一句话：提出首个面向 CHERI 平台 C 程序的有界模型检测器 ESBMC-CHERI，可形式验证内存安全与兼容性问题。
本文介绍 ESBMC-CHERI，这是首个能够对 CHERI 平台 C 程序进行形式验证的有界模型检测器。CHERI 在硬件层为 C/C++ 等内存不安全语言提供运行时保护，但改变了 C 程序语义，使部分原本安全的程序在 CHERI 扩展平台上触发硬件异常。因此，在编译前检测内存安全违规与兼容性问题至关重要，而此前缺乏面向 CHERI-C 的验证工具。作者在 ESBMC 中实现了对 CHERI-C 的支持，使其可进行有界模型检测，并报告了实现进展、未来工作与评估计划。工具与源码已公开。
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.
@inproceedings{paperbot7420,
title = {ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC},
author = {Franz Brauße and Fedor Shmarov and Rafael Menezes and Mikhail R. Gadelha and Konstantin Korovin and Giles Reger and Lucas C. Cordeiro},
booktitle = {ISSTA},
year = {2022},
doi = {10.1145/3533767.3543289}
}