ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC

Franz Brauße; Fedor Shmarov; Rafael Menezes; Mikhail R. Gadelha; Konstantin Korovin; Giles Reger; Lucas Cordeiro

ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC

Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas Cordeiro

Igalia

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In this paper we present ESBMC-CHERI – first bounded model checker capable of formally verifying C programs for CHERI-enabled platforms. CHERI provides run-time protection for the memory unsafe programming languages such as C/C++ at the hardware level. At the same time, it introduces new semantics to C programs, making some safe C programs cause hardware exceptions on CHERI-extended platforms. Hence, it is crucial to detect memory safety violations and compatibility issues ahead of compilation. However, there are no verification tools currently available for reasoning over CHERI-C programs. We demonstrate the work undertaken towards implementing support for CHERI-C in our state-of-the-art bounded model checker ESBMC and the plans for future work and extensive evaluation of ESBMC-CHERI. The ESBMC-CHERI demonstration and the source code are available at https://github.com/esbmc/esbmc/tree/cheri-clang.

Original language	English
Title of host publication	ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)
Publication status	Accepted/In press - 27 May 2022

Embargoed Document

esbmc-cheri
Accepted author manuscript, 457 KB
Embargo ends: 1/01/32

Cite this

@inproceedings{87b7e1bda4e54e78bd8352a82e73ebf3,

title = "ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC",

abstract = "In this paper we present ESBMC-CHERI – first bounded model checker capable of formally verifying C programs for CHERI-enabled platforms. CHERI provides run-time protection for the memory unsafe programming languages such as C/C++ at the hardware level. At the same time, it introduces new semantics to C programs, making some safe C programs cause hardware exceptions on CHERI-extended platforms. Hence, it is crucial to detect memory safety violations and compatibility issues ahead of compilation. However, there are no verification tools currently available for reasoning over CHERI-C programs. We demonstrate the work undertaken towards implementing support for CHERI-C in our state-of-the-art bounded model checker ESBMC and the plans for future work and extensive evaluation of ESBMC-CHERI. The ESBMC-CHERI demonstration and the source code are available at https://github.com/esbmc/esbmc/tree/cheri-clang.",

author = "Franz Brau{\ss}e and Fedor Shmarov and Rafael Menezes and Gadelha, {Mikhail R.} and Konstantin Korovin and Giles Reger and Lucas Cordeiro",

year = "2022",

month = may,

day = "27",

language = "English",

booktitle = "ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)",

}

TY - GEN

T1 - ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC

AU - Brauße, Franz

AU - Shmarov, Fedor

AU - Menezes, Rafael

AU - Gadelha, Mikhail R.

AU - Korovin, Konstantin

AU - Reger, Giles

AU - Cordeiro, Lucas

PY - 2022/5/27

Y1 - 2022/5/27

N2 - In this paper we present ESBMC-CHERI – first bounded model checker capable of formally verifying C programs for CHERI-enabled platforms. CHERI provides run-time protection for the memory unsafe programming languages such as C/C++ at the hardware level. At the same time, it introduces new semantics to C programs, making some safe C programs cause hardware exceptions on CHERI-extended platforms. Hence, it is crucial to detect memory safety violations and compatibility issues ahead of compilation. However, there are no verification tools currently available for reasoning over CHERI-C programs. We demonstrate the work undertaken towards implementing support for CHERI-C in our state-of-the-art bounded model checker ESBMC and the plans for future work and extensive evaluation of ESBMC-CHERI. The ESBMC-CHERI demonstration and the source code are available at https://github.com/esbmc/esbmc/tree/cheri-clang.

AB - In this paper we present ESBMC-CHERI – first bounded model checker capable of formally verifying C programs for CHERI-enabled platforms. CHERI provides run-time protection for the memory unsafe programming languages such as C/C++ at the hardware level. At the same time, it introduces new semantics to C programs, making some safe C programs cause hardware exceptions on CHERI-extended platforms. Hence, it is crucial to detect memory safety violations and compatibility issues ahead of compilation. However, there are no verification tools currently available for reasoning over CHERI-C programs. We demonstrate the work undertaken towards implementing support for CHERI-C in our state-of-the-art bounded model checker ESBMC and the plans for future work and extensive evaluation of ESBMC-CHERI. The ESBMC-CHERI demonstration and the source code are available at https://github.com/esbmc/esbmc/tree/cheri-clang.

M3 - Conference contribution

BT - ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)

ER -

ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC

Abstract

Embargoed Document

Fingerprint

Cite this