一句话：首次严格全面地定义 CHERI C 语义，涵盖能力、来源与未定义行为，并给出可执行及 Coq 机器化形式。
内存安全漏洞长期困扰传统架构与 C 代码库。CHERI 用不可伪造的硬件能力替代机器字指针，以极小修改提升现有 C 代码安全性，已有 MIPS/RISC-V 原型并在 Arm Morello 与 Microsoft CHERIoT 中评估，但 CHERI C 的精确语义仍属开放问题。本文首次尝试严格而全面地定义 CHERI C 语义，讨论能力、指针来源与未定义行为等关键设计问题，并以散文、基于 Cerberus C 语义的可执行语义以及 Coq 机器化语义三种互补形式加以澄清。该工作为 CHERI C 代码移植、编译器实现及未来语义与验证奠定基础。
Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C codebase chronically prone to exploitable errors. The CHERI research project has shown how one can provide radically improved security for that existing codebase with minimal modification, using unforgeable hardware capabilities in place of machine-word pointers in CHERI dialects of C, implemented as adaptions of Clang/LLVM and GCC. CHERI was first prototyped as extensions of MIPS and RISC-V; it is currently being evaluated by Arm and others with the Arm Morello experimental architecture, processor, and platform, to explore its potential for mass-market adoption, and by Microsoft in their CHERIoT design for embedded cores. There is thus considerable practical experience with CHERI C implementation and use, but exactly what CHERI C's semantics is (or should be) remains an open question. In this paper, we present the first attempt to rigorously and comprehensively define CHERI C semantics, discuss key semantics design questions relating to capabilities, provenance, and undefined behaviour, and clarify them with semantics in multiple complementary forms: in prose, as an executable semantics adapting the Cerberus C semantics, and mechanised in Coq. This establishes a solid foundation for CHERI C, for those porting code to it, for compiler implementers, and for future semantics and verification.
@inproceedings{ZalivaMA0DRC0SW24,
title = {Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance},
author = {Vadim Zaliva and Kayvan Memarian and Ricardo Almeida and Jessica Clarke and Brooks Davis and Alexander Richardson and David Chisnall and Brian Campbell and Ian Stark and Robert N. M. Watson and Peter Sewell},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3617232.3624859}
}