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

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-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 languageEnglish
Title of host publicationACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)
Publication statusAccepted/In press - 27 May 2022

Fingerprint

Dive into the research topics of 'ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC'. Together they form a unique fingerprint.

Cite this