Reference. Cerisier: A Program Logic for Attestation in a Capability Machine

June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, Lars Birkedal · PLDI · 2026 · security separation-logic · PDF · DOI · pldb
A key feature in trusted computing is attestation, which allows encapsulated components (enclaves) to prove their identity to (local or remote) distrusting components. Reasoning about software that uses the technique requires tracking how trust evolves after successful attestation. This process is security-critical and non-trivial, but no existing formal verification technique supports modular reasoning about attestation of enclaves and their clients, or proving end-to-end properties for systems combining trusted, untrusted and attested code. We contribute Cerisier, the first program logic for modular reasoning about trusted, untrusted and attested code, fully mechanized in the Iris separation logic and the Rocq Prover. We formalize a recent proposal, CHERI-TrEE, to extend capability machines with enclave primitives, as an extension to the Cerise capability machine and program logic. Our program logic comes with a universal contract for untrusted code, which captures both capability safety and local enclave attestation. Like Cerise, this universal contract is phrased in terms of a logical relation defining capabilities’ authority. We demonstrate Cerisier by proving end-to-end properties for three representative applications of trusted computing: secure outsourced computation, mutual attestation and a modeled trusted sensor component.

Cite
Cite as @rousseau-2026-cerisier (helia, typst) · \cite{rousseau-2026-cerisier} (LaTeX)
BibTeX
bibtex · 1 line
@article{rousseau-2026-cerisier, title={Cerisier: A Program Logic for Attestation in a Capability Machine}, volume={10}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3808287}, DOI={10.1145/3808287}, number={PLDI}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Rousseau, June and Carnier, Denis and Van Strydonck, Thomas and Keuchel, Steven and Devriese, Dominique and Birkedal, Lars}, year={2026}, month=June, pages={1004–1028} }
hayagriva YAML (typst)
yaml · 20 lines
rousseau-2026-cerisier:
  type: article
  title: 'Cerisier: A Program Logic for Attestation in a Capability Machine'
  author:
  - Rousseau, June
  - Carnier, Denis
  - Strydonck, Thomas Van
  - Keuchel, Steven
  - Devriese, Dominique
  - Birkedal, Lars
  date: 2026-06
  page-range: 1004-1028
  serial-number:
    doi: 10.1145/3808287
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: PLDI
    volume: 10
Download: rousseau-2026-cerisier.bib · rousseau-2026-cerisier.yml
Cites 47 works (2 here)
With notes (2)

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code georges-2024-ceriseJACM · 2024
A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities , machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. We use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant. The methodology we present underlies recent work of the authors on formal reasoning about capability machines [Georges et al. 2021 ; Skorstengaard et al. 2019a ; Van Strydonck et al. 2022 ], but was left somewhat implicit in those publications. In this paper we present a pedagogical introduction to the methodology, in a simpler setting (no exotic capabilities), and starting from minimal examples. We work our way up to new results about a heap-based calling convention and implementations of sophisticated object-capability patterns of the kind previously studied for high-level languages with object-capabilities, demonstrating that the methodology scales to such reasoning.
DOI

Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018JFP · 2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
PDF · DOI · pldb
External (45)
rousseau-2026-cerisier reference entries/refs/rousseau-2026-cerisier/rousseau-2026-cerisier.hel