Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance

Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson and 5 others

CHERI is a hardware scheme that replaces raw pointers with unforgeable capabilities carrying bounds the chip checks on every access, turning most memory-safety bugs in C into safe crashes — and there is a whole dialect, CHERI C, that existing code recompiles into; but nobody had ever written down precisely what CHERI C means, so its two compilers risk quietly disagreeing; this work from Cambridge, Edinburgh, and SRI gives CHERI C its first rigorous semantics — in prose, as an executable model that runs test programs, and mechanised in the Coq proof assistant — and confronts the thorny truth that C's undefined behaviour and compiler optimisations make it impossible to state, at the source level, the very security guarantee CHERI was built to provide.

The argument in one glance

Problem

CHERI C promises memory safety for legacy C, but nobody wrote down what it means

Memory-safety bugs remain the leading source of security vulnerabilities, and the vast C and C++ codebases we all depend on are riddled with them. CHERI is a hardware scheme that turns raw pointers into unforgeable capabilities the chip bounds-checks on every access, and CHERI C is a dialect that existing code simply recompiles into to gain that protection — Arm and Microsoft are evaluating it for mass adoption. Yet what CHERI C actually means has only ever been defined by its compilers, not written down.
What people did

Let the compilers define the language

In practice, CHERI C is whatever its implementations do — the CHERI versions of Clang/LLVM and, more recently, GCC. Programmers port code by trial and experience, and the compiler teams build up a shared but informal understanding of what the dialect permits. For a research prototype this is workable, and it is how the language was refined in the first place.
Why it fell short

Without a written definition, implementations drift and guarantees blur

Defining a language by its implementations is dangerous. Clang and GCC can quietly diverge from each other and from what programmers expect, breaking portability across the several CHERI architectures. Programmers cannot know precisely what is permitted; verification has no foundation; and — most subtly — it becomes unclear what security CHERI C really guarantees, because capabilities interact in tricky ways with two deep features of C: undefined behaviour and pointer provenance, both of which compilers exploit when they optimise.
This paper's idea

Give CHERI C a rigorous, mechanised semantics — and face the hard truth in it

This work writes down what CHERI C is, in three complementary forms: prose for accessibility, an executable model (extending a trusted ISO C semantics) that runs test programs as an oracle, and a mechanisation in the Coq proof assistant that nails every detail and grounds future proofs. Along the way it decides the subtle cases where capabilities, undefined behaviour, and provenance collide — and confronts head-on that these interactions make it impossible to state CHERI C's intended security guarantee at the source level, giving instead a precise account of what well-defined code can rely on.

Why this problem is worth solving

To see why pinning down the meaning is both valuable and hard, it helps to understand what a capability is.

A conventional processor represents a pointer as a plain machine word — a virtual address — and the only protection is the coarse-grained memory management unit. CHERI replaces this with a capability: a wider value (128 bits plus one out-of-band tag bit on Arm’s Morello) that packs the address together with the bounds of the memory it is allowed to reach, a set of permissions, and other metadata. The hardware checks, on every access, that the address lies within the bounds and that the right permission is present, faulting otherwise. Crucially, capabilities are unforgeable: the extra tag bit, which ordinary memory writes cannot set, marks a value as a genuine capability, and legitimate operations can only shrink a capability’s bounds, never grow them. CHERI C compiles every C pointer to a capability, so an out-of-bounds access that would silently corrupt memory on a normal machine instead trips a hardware check and fail-stops. This is why recompiling existing C with a CHERI compiler deterministically mitigates a large fraction of memory-safety vulnerabilities, with only a fraction of a percent of source changes — a rare path to hardening enormous legacy codebases without rewriting them.

The reason a precise semantics is genuinely difficult, not just tedious, is that two subtle features of C fight against a clean story.

ISO C is defined around undefined behaviour: an out-of-bounds access, a signed overflow, a data race, and many other things are declared to have no defined meaning, and if any possible execution of a program hits undefined behaviour, the whole program is deemed to have it — the compiler may then do anything. This is not a temporal notion: the compiler need not behave sensibly up to the offending point, but may transform the entire program on the assumption that undefined behaviour never happens. That assumption powers aggressive optimisation. A second feature is pointer provenance: to justify reordering memory accesses, compilers track which allocation each pointer came from, assuming pointers of different origin never alias, and the in-progress ISO provenance model bakes this into the abstract machine. Both features mean the compiler reasons about the program in ways that move, delete, and rewrite code based on assumptions the programmer must uphold. Any semantics of CHERI C must reconcile the hardware’s concrete capability checks with these abstract, optimisation-licensing notions — and that reconciliation is where the deep questions live.

What people did before, and where it broke

Define CHERI C by its implementations. Treat the CHERI Clang and GCC compilers as the de facto specification, refining the language by porting code. Where it broke. Implementations can silently diverge from each other and from programmer expectations, with no reference to resolve disputes and no basis for portability or verification.
Rely on the hardware’s deterministic trapping as the guarantee. Assume that because the chip bounds-checks every access, an out-of-bounds access always fail-stops. Where it broke. Compiler optimisations, permitted to assume undefined-behaviour-freedom, can delete the very access that would have trapped, so the hardware guarantee does not survive to the compiled program.
Reuse ISO C’s existing memory semantics as-is. Take the standard C abstract machine and provenance model unchanged. Where it broke. It has no notion of capabilities, tags, bounds compression, or the CHERI-specific behaviours around integer-pointer conversions and representability, so it cannot describe what CHERI C actually does.
Build an abstract formal memory model (prior CHERI-C formalisation). Model CHERI C memory abstractly and prove properties of it. Where it broke. Being abstract, it left out non-representability, pointer-to-integer conversion, capability derivation in arithmetic, and the optimisation interactions — the very cases where the semantics is contentious.
The gap. No existing account combined an accessible, executable, and machine-checked definition that engaged with the real, messy interactions of capabilities, undefined behaviour, and provenance, or was honest about what security guarantee those interactions actually permit. Producing one is exactly what a language heading for mass adoption needs.

How the CHERI C semantics is built

Pinning down what CHERI C means, in three forms, and facing the hard cases

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Replace an implementation-defined language with a rigorous, machine-checked definition. The core contribution is to stop letting the compilers be the specification and instead write down what CHERI C means, precisely enough to be executed and mechanised. This matters because a language defined only by its implementations has no ground truth: Clang and GCC can drift apart, programmers cannot know what is guaranteed, and verification has nothing to stand on. By giving the language a single rigorous semantics — expressed in prose for people, as an executable model for testing, and in a proof assistant for proving — the work turns a folk understanding into an object everyone can check against, which is exactly how the test suite could catch real bugs in both compilers. Replacing informal, error-prone reasoning about a system with a rigorous, sound, machine-checkable definition that others can build proofs upon is the same discipline the quantum-program verification work covered elsewhere on this site follows, exchanging hand-waving for a formal logic whose soundness can be trusted.

Confront that a guarantee true of the hardware need not survive the compiler. The paper’s deepest insight is a disappointment turned into clarity. One would love to define CHERI C so that any out-of-bounds access is guaranteed to trap — a clean, strong security property. But because such an access is undefined behaviour in C, the optimiser is allowed to assume it never happens and simply delete the access, so the trap that the hardware would have produced never occurs in the compiled program, and whether it does can hinge on unrelated code. A source-level semantics therefore cannot promise the fail-stop safety CHERI provides; it must keep undefined behaviour and state instead what well-defined code can rely on. Grappling with whether a property stated at one level still holds after a program is transformed, rather than assuming it does, is the same problem the scheduling-language work covered elsewhere on this site centers on, where a handle on the code must be carefully tracked to stay meaningful through each transformation the compiler applies.

Track capabilities and provenance as two complementary mechanisms, not one. A tempting simplification is that CHERI’s runtime capability checks make the compiler’s provenance analysis redundant — both, after all, are about which memory a pointer may legitimately reach. The paper shows they are complementary and neither subsumes the other: capability bounds can over-approximate an allocation, two pointers with the same bounds can have different provenance (a freed object and a fresh one reusing its address), and without a revocation mechanism a runtime check cannot tell a live allocation from a dead one, which provenance can. So the semantics keeps both, each doing a job the other cannot. Recognizing that two mechanisms operating at different times, one at runtime and one at compile time, are each necessary for a different case rather than collapsing them into one is the same judgement the CXL memory work covered elsewhere on this site makes, keeping a strict mechanism for the data that needs it and a looser one for the data that does not, because no single mechanism serves both.

Following the “does it trap?” question through the semantics

Whether an out-of-bounds write is guaranteed to fail-stop

Tracing one seemingly-simple guarantee shows why the semantics is subtle.

Step 1 of 5

The appealing dream

It would be wonderful to define CHERI C so that every out-of-bounds access is caught by the hardware and the program fail-stops safely — a clean, strong security guarantee you could write straight into the semantics and that programmers could rely on absolutely.

This is the intuition most people have about what CHERI buys you.

Why it works

A single agreed definition stops implementations from drifting apart. When a language is defined only by its compilers, Clang and GCC can quietly disagree and confuse programmers → but writing one rigorous semantics gives them all a common reference to conform to → so the test suite could check the compilers against it and surface real bugs in each.
Three complementary forms serve three different needs. A single form cannot be readable, runnable, and provable at once → but pairing prose with an executable model and a Coq mechanisation makes the definition accessible, testable as an oracle, and a foundation for machine-checked proof → so each audience, from porters to verifiers, gets a form it can use.
Building on trusted foundations keeps the huge C semantics manageable. Defining a C dialect from scratch would be enormous and error-prone → but extending an already-validated ISO C semantics and its provenance model means only the capability-specific parts are new → so the effort focuses on what CHERI changes and the interactions with existing C features are checked systematically.
Facing the optimisation problem honestly is more useful than a false guarantee. It is tempting to promise that every out-of-bounds access traps → but optimisations can delete the access, so the semantics instead keeps undefined behaviour and states what well-defined code can rely on → so the definition stays sound and the real open question, the precise security guarantee, is named rather than hidden.
Ghost state makes the semantics precise without over-constraining compilers. Directly overwriting a capability clears its tag in hardware, but an optimiser may remove the overwrite → but recording the event in abstract-machine ghost state and making later use of the capability undefined permits both the trap and its elimination → so optimisations stay sound while the abstract machine still bounds what programs may do.

What it costs (trade-offs and scope)

It cannot state CHERI C’s security guarantee. The paper’s central, honest finding: because undefined behaviour lets optimisations delete the very accesses that would trap, no source-level semantics can promise the fail-stop safety CHERI is built for; it gives a positive semantics of what well-defined code can rely on and flags the exact guarantee as open work.
It covers spatial safety, and its concrete model is one architecture. CHERI C targets spatial safety; temporal safety is not universally guaranteed and remains active research, and the Coq model fixes the implementation-defined details to Arm Morello.
Several claims are argued, not proved. The mechanisation gives a foundation for proofs but does not itself prove the deep properties — for instance, that capability bounds make a provenance check redundant is stated as a belief, not a theorem.
The hardest cases are under-tested. Testing exactly where optimisations interact with undefined behaviour — the cases the semantics most needs to get right — is acknowledged as difficult and left for future work; the 94-test suite mainly exercises the main design choices.
Some decisions trade portability for future-proofing and are provisional. Making representability implementation-defined admits more architectures but makes portable CHERI C harder to write, and several choices are noted as needing revisiting with more experience.
Ghost state is abstract, not real. The ghost-state bits exist only in the abstract machine to license or forbid optimisations; hardware does not carry them, so the semantics bounds behaviour precisely-but-loosely rather than predicting it exactly.
Validation is by testing and expert discussion, not exhaustive. The suite is small and was not executed on the embedded CHERIoT target, whose applicability rests on discussion with its designers.

The evaluation

Ways of defining CHERI C

Property	Compilers only	Prior formal model
How CHERI C is defined		An abstract memory model
Runs test programs as an oracle	No	Via a separate checker
Undefined-behaviour and optimisation interactions	Implicit, unclear	Not addressed
Covers intptr_t, non-representability, provenance	Whatever the compilers do
Proves properties	No	Yes

Ways of pinning down CHERI C. This work gives the first rigorous, comprehensive definition in three complementary forms — prose, an executable model extending the Cerberus ISO C semantics and PNVI-ae-udi provenance model, and a Coq mechanisation of the memory object model — engaging directly with capabilities, undefined behaviour, and provenance. A 94-test suite run on CHERI Clang and GCC found them mostly compliant with no principal disagreements, and surfaced several real implementation bugs.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This work is a careful, important foundation-laying effort: it gives CHERI C — a memory-safe dialect of C heading toward mass adoption via Arm and Microsoft — its first rigorous definition, in three complementary forms (readable prose, an executable model atop a trusted ISO C semantics that runs as a test oracle, and a Coq mechanisation for future proof), and it validates that against the real Clang and GCC compilers, finding no principal disagreements and several implementation bugs. Its most valuable contribution is intellectual honesty. It shows that C’s undefined behaviour and compiler optimisations make it impossible to state, at the source level, the fail-stop security guarantee CHERI is meant to provide — optimisations can delete the very accesses that would trap — so it gives a positive semantics of what well-defined code can rely on and names the true security property as open. It covers spatial (not temporal) safety, fixes its concrete model to one architecture, argues rather than proves its deeper claims, under-tests the hardest optimisation cases, and leaves several choices provisional. The durable idea is that a memory-safety mechanism is only as trustworthy as the source-language guarantee you can actually state and prove about it — and getting there requires confronting, not glossing over, how the compiler transforms the code beneath you.

Background

Why real systems increasingly need formal foundations

It helps to see why a paper whose product is a definition, not a faster or cheaper system, belongs at an architecture conference. Hardware and systems are increasingly relied upon for security, and a security mechanism is only as good as the guarantee you can precisely state and check about it — a vague promise of safety invites exactly the gaps attackers exploit, and here the gap is real: a well-known result showed that adding safety checks after the optimiser can let the optimiser delete both the bad access and its check. As mechanisms like CHERI move from research prototypes toward the phones and servers of millions, the informal understanding that sufficed in the lab becomes a liability: implementations diverge, programmers guess, and no one can prove what holds. A rigorous, executable, mechanised semantics is the foundation that lets the rest — portable code, conforming compilers, verified programs — be built with confidence. The virtual-memory research work covered elsewhere on this site makes a kindred bet, that building a faithful, executable model of a hard-to-study system is what unlocks rigorous work on top of it. The broad lesson is that as systems carry more critical weight, the unglamorous act of writing down exactly what they mean becomes essential infrastructure.

If you remember only three things

1. CHERI is a hardware architecture that replaces machine-word pointers with unforgeable capabilities — values carrying an address plus bounds, permissions, and a protecting tag bit, which the chip checks on every access and which code can shrink but never grow — so recompiling legacy C into the CHERI C dialect turns most memory-safety bugs into deterministic safe crashes with a fraction of a percent of source changes; but CHERI C's meaning had only ever been defined by its Clang and GCC implementations, which risk quietly diverging, leaving unclear what is permitted, how it interacts with C's undefined behaviour and pointer provenance, and what security it actually guarantees.
2. This work gives CHERI C its first rigorous, comprehensive semantics in three complementary forms — accessible prose, an executable model extending the well-validated Cerberus ISO C semantics and the PNVI-ae-udi provenance memory model (runnable as a test oracle), and a mechanisation of the memory object model in the Coq proof assistant (a basis for future proof) — and it resolves the subtle design questions where capabilities, undefined behaviour, and provenance collide (out-of-bounds construction and representability, integer-pointer conversions via capability-backed intptr_t, direct overwriting of capability bytes), using per-capability abstract-machine ghost state to keep compiler optimisations sound.
3. The deepest finding is honest and negative: because an out-of-bounds access is undefined behaviour, a compiler optimisation may delete the access that the hardware would have trapped, so no source-level semantics can state the fail-stop security guarantee CHERI is built to provide — the paper therefore gives a positive semantics of what well-defined code can rely on and names the precise security property as open work; validated by a 94-test suite on CHERI Clang and GCC (mostly compliant, no principal disagreements, several real bugs found), it covers spatial not temporal safety, fixes its concrete model to Arm Morello, and argues rather than proves its deeper claims.

Check yourself

Check your understanding

1. What is a CHERI capability, and how does it provide memory safety?
2. Why did CHERI C need a rigorous written semantics at all?
3. What is the paper's central, and somewhat negative, finding about CHERI C's security guarantee?
4. Which statement best reflects the limits of this work?

Sources

The paper is “Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance” by Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell, published at ASPLOS 2024, DOI 10.1145/3617232.3624859. The authors are at the University of Cambridge, the University of Edinburgh, SRI International, and Microsoft; the semantics and examples are open-source.

This explainer is written from the full 16-page text. Everything above comes from the paper’s own sections: the introduction and background on CHERI hardware capabilities (Morello’s 128-plus-1-bit capabilities, tags, bounds compression, permissions, and sealing), on C undefined behaviour and its non-temporal, whole-program nature, and on pointer provenance and the PNVI-ae-udi memory object model; the design-questions section working through the interactions of capabilities, undefined behaviour, and provenance across out-of-bounds access and the impossibility of a trapping guarantee, out-of-bounds construction and representability, pointer-integer conversions with capability-backed (u)intptr_t and the new ptraddr_t, type punning, direct accesses to capability representations handled with per-capability ghost state, pointer equality, capability derivation in binary arithmetic, sub-object bounds, const and permissions, cross-architecture abstraction, and why capability and provenance checks are complementary; the executable-semantics section extending Cerberus with the CHERI C memory object model, the new CHERI undefined behaviours, the ghost-state-augmented memory state, and the bounds-checked load rule, mechanised in Coq and extracted for execution; and the validation section reporting the 94-test suite run across Cerberus, CHERI Clang/LLVM, and CHERI GCC (mostly compliant with no principal disagreements, identifying several real implementation and library bugs), plus the discussion of CHERIoT applicability and the open question of CHERI C’s precise security guarantees.