Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part I
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part I
复制标题
系统构建和分析的工具和算法 - 第 29 届国际会议，TACAS 2023，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2023，法国巴黎，2023 年 4 月 22-27 日，会议记录，部分
DOI：
10.1007/978-3-031-30823-9_28
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Park S
中科院分区：
文献类型：
--
作者：
Park S
CHERI-C通过添加硬件功能扩展了C编程语言，在保持效率的同时确保一定程度的内存安全。功能还可以用于更高级别的安全措施，如软件划分，必须正确使用以实现所需的安全保证。由于扩展改变了C语言的语义，因此需要新的理论和工具来推理CHERI-C代码并验证其正确性。在这项工作中，我们提出了一个正式的内存模型，提供了CHERI-C程序的内存语义。我们提出了一个广义的理论，具有丰富的性质，适合验证和潜在的其他类型的分析。我们的理论是由Isabelle/HOL形式化，也产生了内存模型的OCaml可执行实例的支持。验证和提取的代码，然后使用实例化的parametricGillian程序分析框架，我们可以执行CHERI-C程序的具体执行。该工具可以运行一个CHERI-C测试套件，证明我们的工具的正确性，并捕捉CHERI硬件可能错过的一类很好的安全违规。
CHERI-C extends the C programming language by addinghardware capabilities, ensuring a certain degree of memory safety while remaining efficient. Capabilities can also be employed for higher-level security measures, such as software compartmentalization, that have to be used correctly to achieve the desired security guarantees. As the extension changes the semantics of C, new theories and tooling are required to reason about CHERI-C code and verify correctness. In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs. We present a generalised theory with rich properties suitable for verification and potentially other types of analyses. Our theory is backed by an Isabelle/HOL formalisation that also generates an OCaml executable instance of the memory model. The verified and extracted code is then used to instantiate the parametricGillianprogram analysis framework, with which we can perform concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss.