A Formal CHERI-C Semantics for Verification

TL;DR

This paper introduces a formal memory semantics for CHERI-C, enabling verification and analysis of capability-based security features through a formal model and tool support.

Contribution

It provides a formal, verified memory model for CHERI-C, integrated with the Gillian analysis framework for concrete execution and safety verification.

Findings

Successfully formalized CHERI-C semantics in Isabelle/HOL

Generated executable memory model in OCaml for analysis

Detected safety violations in CHERI hardware through testing

Abstract

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.