CHERI-C extends the C programming language by adding hardware 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 parametric Gillian program 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.

翻译：CHERI-C通过添加硬件能力扩展了C编程语言，在保持高效的同时确保一定程度的内存安全性。这些能力还可用于更高级别的安全措施（如软件隔离），这些措施必须被正确使用才能实现所需的安全保障。由于该扩展改变了C语言的语义，因此需要新的理论和工具来推理CHERI-C代码并验证其正确性。本文提出了一种形式化内存模型，为CHERI-C程序提供了内存语义。我们提出了一种具有丰富属性的广义理论，适用于验证及其他类型的分析。该理论基于Isabelle/HOL形式化，并可生成OCaml可执行内存模型实例。随后，利用验证并提取的代码实例化参数化Gillian程序分析框架，从而实现对CHERI-C程序的具体执行。该工具能够运行CHERI-C测试套件，验证其正确性，并捕获CHERI硬件可能遗漏的一类安全违规行为。