Trabalho em anais de eventoOpen Access
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC
BRAUßE, FRANZ; SHMAROV, FEDOR; MENEZES, RAFAEL; GADELHA, MIKHAIL R.; KOROVIN, KONSTANTIN; REGER, GILES; CORDEIRO, LUCAS C
Resumo
Resumo
This paper presents ESBMC-CHERI -- the 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 current verification tools 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.
Autoria
Autores do grupo (1)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
CHERIbounded model checkingC program verificationmemory safetyformal verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento