ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC
复制标题
ESBMC-CHERI：利用 ESBMC 验证 CHERI 平台的 C 程序
DOI：
10.1145/3533767.3543289
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Brauße F
中科院分区：
文献类型：
--
作者：
Brauße F
本文介绍了ESBMC-CHERI -第一个有界模型检查器能够正式验证C程序的CHERI使能平台。CHERI在硬件级为C/C++等内存不安全的编程语言提供运行时保护。同时，它为C程序引入了新的语义，使得一些安全的C程序在CHERI扩展平台上产生硬件异常。因此，在编译之前检测内存安全违规和兼容性问题至关重要。然而，有没有目前的验证工具，推理CHERI-C程序。我们展示了在我们最先进的有界模型检查器ESBMC中实现对CHERI-C的支持所做的工作，以及ESBMC-CHERI未来工作和广泛评估的计划。ESBMC-CHERI演示和源代码可以在https://github.com/esbmc/esbmc/tree/cheri-clang上获得。
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.
登录
查看更多内容
CHERI Concentrate：实用的压缩功能
影响因子：
3.7
作者：
Woodruff J
通讯作者：
Woodruff J
影响因子：
1.8
作者：
Armstrong, Alasdair;Bauereiss, Thomas;Sewell, Peter
通讯作者：
Sewell, Peter
使用基于 SMT 的上下文边界模型检查来验证 CUDA 程序
DOI：
10.1145/2851613.2851830
发表时间：
2016
期刊：
Proceedings of the 31st Annual ACM Symposium on Applied Computing
影响因子：
--
作者：
P. A. Pereira;Higo F. Albuquerque;Hendrio Marques;I. D. Silva;C. Carvalho;L. Cordeiro;Vanessa Santos;R. Ferreira
通讯作者：
R. Ferreira
基于Qt跨平台框架的C++程序有界模型检查
DOI：
--
发表时间：
2017
期刊：
Software testing, verification & reliability
影响因子：
--
作者：
Felipe R. Monteiro;Mário A. P. Garcia;L. Cordeiro;Eddie Filho
通讯作者：
Eddie Filho
探索 C 语义和指针起源
DOI：
--
发表时间：
2019
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Kayvan Memarian;Victor B. F. Gomes;Brooks Davis;Stephen Kell;Alexander Richardson;R. Watson;Peter Sewell
通讯作者：
Peter Sewell