pith. sign in

arxiv: 2604.13638 · v2 · submitted 2026-04-15 · 💻 cs.PL

Cerisier: A Program Logic for Attestation in a Capability Machine

June Rousseau , Denis Carnier , Thomas Van Strydonck , Steven Keuchel , Dominique Devriese , Lars Birkedal This is my paper

Pith reviewed 2026-05-10 12:10 UTC · model grok-4.3

classification 💻 cs.PL
keywords program logicattestationcapability machinesIris separation logicenclavestrusted computingformal verificationCHERI-TrEE
0
0 comments X

The pith

Cerisier is the first program logic for modular reasoning about trusted, untrusted, and attested code on capability machines.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Cerisier supplies a program logic that lets developers prove security properties across systems that mix trusted enclaves, untrusted components, and attestation steps. The logic tracks how trust changes after attestation succeeds and supplies a single universal contract that handles both capability safety and attestation for any untrusted code. It is built as an extension of the Cerise capability machine logic and is fully mechanized in Iris and Rocq. This matters because attestation is security-critical yet hard to reason about modularly, and prior techniques could not handle the combination of trusted, untrusted, and attested code in one framework. The paper shows the approach works by verifying three concrete applications: secure outsourced computation, mutual attestation, and a trusted sensor model.

Core claim

Cerisier is the first program logic for modular reasoning about trusted, untrusted and attested code, fully mechanized in the Iris separation logic and the Rocq Prover. It formalizes the CHERI-TrEE proposal to extend capability machines with enclave primitives as an extension to the Cerise machine and logic. The logic includes a universal contract for untrusted code that captures both capability safety and local enclave attestation; the contract is expressed via a logical relation that defines the authority of capabilities. End-to-end properties are proved for secure outsourced computation, mutual attestation, and a modeled trusted sensor component.

What carries the argument

The universal contract for untrusted code, expressed as a logical relation that defines the authority of capabilities and thereby captures both capability safety and the effects of local enclave attestation.

If this is right

  • Developers can prove end-to-end security properties for secure outsourced computation that uses attestation.
  • Mutual attestation protocols between distrusting components can be verified modularly.
  • Properties of modeled trusted sensor components that rely on attestation can be established without inspecting every line of untrusted client code.
  • Reasoning about how trust evolves after successful attestation becomes possible inside a single modular framework.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same logical-relation style could be adapted to other enclave hardware extensions beyond CHERI-TrEE.
  • Larger systems that combine remote attestation with local enclave use might become verifiable by extending the contract.
  • The mechanized proofs could serve as a starting point for verifying real-world trusted-execution environments that expose similar primitives.

Load-bearing premise

The formalization of CHERI-TrEE enclave primitives as an extension to Cerise accurately reflects the intended hardware behavior, and the universal contract adequately encodes both capability safety and local enclave attestation.

What would settle it

A concrete program using the CHERI-TrEE primitives that satisfies the universal contract yet violates one of the claimed end-to-end security properties in secure outsourced computation, mutual attestation, or the trusted sensor example.

Figures

Figures reproduced from arXiv: 2604.13638 by Denis Carnier, Dominique Devriese, June Rousseau, Lars Birkedal, Steven Keuchel, Thomas Van Strydonck.

Figure 1
Figure 1. Figure 1: Interaction scenario for the secure outsourced computation (SOC) example. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Simplified pseudocode of Secure Outsourced Computation (SOC) using CHERI-TrEE primi [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The base Cerise capability machine’s words, state, and instructions. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Excerpt of the operational semantics for of a single instruction. The complete operational [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Syntax of the Cerisier program logic. U K (a) Scenario 1: pass￾ing control to untrusted code U K (b) Scenario 2: being called by untrusted code (possibly many times) [PITH_FULL_IMAGE:figures/full_fig_p006_6.png] view at source ↗
Figure 4
Figure 4. Figure 4: Two scenarios: a trusted component (K) interacts with an un￾trusted context (U). For reasoning, we start from the Cerise program logic [18], formalized and mechanized in Iris [26] and Rocq. It supports modular reasoning about systems combining both trusted and adversarial code. The syntax of the program logic is presented in [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 7
Figure 7. Figure 7: WP rule for a valid load. Changes between the pre- and postcondition are marked in orange. E (𝑤) ≜    pc Z⇒ 𝑤 ∗ © ­ « (𝑟,𝑤 ∗𝑟 ) ∈regs 𝑟 Z⇒ 𝑤𝑟 ∗ V (𝑤𝑟) ª ® ¬    ⇝ • V (𝑤) ≜    V (𝑧) ≜ True for 𝑧 ∈ Z V (o, −, −, −) ≜ True V (e, 𝑏, 𝑒, 𝑎) ≜ ⊲ □ E (rx, 𝑏, 𝑒, 𝑎) V (rw/rwx, 𝑏, 𝑒, −) ≜ ∗𝑎∈ [𝑏,𝑒 ) ∃𝑤 . 𝑎 ↦→ 𝑤 ∗ V (𝑤) 𝑎 V (ro/rx, 𝑏, 𝑒, −) ≜ ∗𝑎∈ [𝑏,𝑒 ) ∃𝑃 . ∃𝑤 . 𝑎 … view at source ↗
Figure 8
Figure 8. Figure 8: Logical relation defining “safe to share” ( [PITH_FULL_IMAGE:figures/full_fig_p007_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Excerpt of the operational semantics with capability sealing extensions, extending Figure [PITH_FULL_IMAGE:figures/full_fig_p008_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Excerpt of the operational semantics with revocation-related extensions, extending Figure [PITH_FULL_IMAGE:figures/full_fig_p010_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: WP rule for a valid case of the isunique instruction with distinct PC, source, and destination registers. The postcondition asserts that either the sweep was unsuccessful, writing 0 to the destination register, or it was successful and we increment the version number of the capability and all addresses within its bounds. operation: the revocation affects the global state, whereas separation logics like Ir… view at source ↗
Figure 12
Figure 12. Figure 12: Excerpt of the operational semantics containing secure hashing extensions and assumptions, [PITH_FULL_IMAGE:figures/full_fig_p011_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Excerpt of the operational semantics with attestation-related extensions, extending Figure [PITH_FULL_IMAGE:figures/full_fig_p012_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Representation of the effects in memory of the [PITH_FULL_IMAGE:figures/full_fig_p012_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: SOC using Cerisier primitives, adapted from Figure [PITH_FULL_IMAGE:figures/full_fig_p014_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Rules for the new enclave instructions. The “ [PITH_FULL_IMAGE:figures/full_fig_p015_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Global invariant I parameterised by user-provided map M of enclaves of interest (custom enclaves). custom_enclaves_contract(M) ≜ ∀𝐼 ∈ dom(M), data, 𝑏, 𝑒, 𝑣, 𝑝′ , 𝑏′ , 𝑒′ , 𝑎′ , 𝑣′ , 𝑜. © ­ ­ ­ ­ ­ ­ ­ « ⌈𝑏 = M (𝐼).addr⌉ ∗ ⌈tidx = tidx_of_otype(𝑜)⌉ ∗ (1) 𝑏 ↦→𝑣 (𝑝 ′ , 𝑏′ , 𝑒′ , 𝑎′ )𝑣 ′ ∗ [𝑏 + 1, 𝑒) ↦→𝑣 M (𝐼).code ∗ (2) 𝑏 ′ ↦→𝑣 ′ [su, 𝑜, 𝑜 + 2, 𝑜] ∗ [𝑏 ′ + 1, 𝑒′ ) ↦→𝑣 ′ data ∗ (3) seal_pred (o,M (I).Penc) ∗ … view at source ↗
Figure 18
Figure 18. Figure 18: Contract of custom enclaves, parameterised by user-provided map [PITH_FULL_IMAGE:figures/full_fig_p016_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Operational semantics: execution of a single instruction. [PITH_FULL_IMAGE:figures/full_fig_p026_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: Execution of a single instruction for sealing, unsealing and enclaves. [PITH_FULL_IMAGE:figures/full_fig_p027_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: Operational semantics helper [PITH_FULL_IMAGE:figures/full_fig_p027_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Lattice of permission. We have 𝑝1 ≼ 𝑝2 if there is a path going up from 𝑝1 to 𝑝2 in the diagram [PITH_FULL_IMAGE:figures/full_fig_p028_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: Full Cerisier code of the SOC client [PITH_FULL_IMAGE:figures/full_fig_p029_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: Full Cerisier code of the SOC enclave [PITH_FULL_IMAGE:figures/full_fig_p030_24.png] view at source ↗
Figure 25
Figure 25. Figure 25: Full Cerisier code of a possible adversary for the SOC example [PITH_FULL_IMAGE:figures/full_fig_p031_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: Cerisier pseudocode of the Mutual Attestation client [PITH_FULL_IMAGE:figures/full_fig_p032_26.png] view at source ↗
Figure 27
Figure 27. Figure 27: Cerisier pseudocode of the Mutual Attestation Enclave A [PITH_FULL_IMAGE:figures/full_fig_p033_27.png] view at source ↗
Figure 28
Figure 28. Figure 28: Cerisier pseudocode of the Mutual Attestation Enclave B [PITH_FULL_IMAGE:figures/full_fig_p034_28.png] view at source ↗
Figure 29
Figure 29. Figure 29: Full Cerisier code of the trusted sensor readout client [PITH_FULL_IMAGE:figures/full_fig_p035_29.png] view at source ↗
Figure 30
Figure 30. Figure 30: Full Cerisier code of the sensor enclave [PITH_FULL_IMAGE:figures/full_fig_p036_30.png] view at source ↗
Figure 31
Figure 31. Figure 31: Full Cerisier code of the transformer enclave [PITH_FULL_IMAGE:figures/full_fig_p037_31.png] view at source ↗
Figure 32
Figure 32. Figure 32: Definition of the enclaves resources [PITH_FULL_IMAGE:figures/full_fig_p039_32.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The paper presents Cerisier, the first program logic for modular reasoning about trusted, untrusted, and attested code on capability machines. It extends the Cerise logic and machine with CHERI-TrEE enclave primitives for local attestation, defines a universal contract for untrusted code via logical relations on capabilities that is intended to capture both capability safety and attestation-derived trust evolution, and mechanizes the entire development in Iris and Rocq. End-to-end properties are proved for three applications: secure outsourced computation, mutual attestation, and a modeled trusted sensor.

Significance. If the universal contract correctly propagates attestation authority without over- or under-approximation, the work would be a significant step forward for verified trusted computing, enabling compositional proofs over mixed codebases where prior logics could not. The full mechanization in Rocq, including the logical-relation definition and the three application proofs, is a clear strength that provides concrete evidence of internal consistency.

major comments (2)
  1. [§3.2] §3.2 (Universal Contract): The logical relation is stated independently of the enclave primitives and is claimed to simultaneously enforce capability safety and track local attestation. However, no explicit lemma is given showing that a successful attestation step updates the client's view of the enclave's authority in the relation (e.g., via a preservation or simulation result under the CHERI-TrEE call instruction). Without this, it is unclear whether the end-to-end properties proved for the three applications actually transfer to executions that use the modeled primitives.
  2. [§4] §4 (CHERI-TrEE Extension): The formalization of the enclave primitives as an extension to Cerise is load-bearing for the adequacy claim, yet the paper provides only an informal correspondence argument rather than a simulation or refinement relation between the extended machine semantics and the proposed CHERI-TrEE hardware behavior. This leaves open whether the mechanized proofs validate the intended hardware model or merely an over-approximation thereof.
minor comments (3)
  1. [§5–7] The three application proofs in §5–7 would benefit from a short table summarizing which parts of the universal contract are exercised by each example, to make the modularity claim easier to assess.
  2. [§3] Notation for the logical relation (e.g., the authority predicates) is introduced in §3 but used with slight variations in the application sections; a single consolidated definition or reference would improve readability.
  3. [§1] The introduction cites the original CHERI-TrEE proposal but does not include a direct pointer to its formal semantics or any prior mechanization attempts; adding this would help situate the contribution.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback on Cerisier. We address the two major comments point by point below, providing clarifications on the logical relation and machine extension while committing to targeted revisions that strengthen the manuscript without altering its core contributions.

read point-by-point responses

  1. Referee: [§3.2] §3.2 (Universal Contract): The logical relation is stated independently of the enclave primitives and is claimed to simultaneously enforce capability safety and track local attestation. However, no explicit lemma is given showing that a successful attestation step updates the client's view of the enclave's authority in the relation (e.g., via a preservation or simulation result under the CHERI-TrEE call instruction). Without this, it is unclear whether the end-to-end properties proved for the three applications actually transfer to executions that use the modeled primitives.

    Authors: The universal contract is intentionally defined independently of specific primitives to support modular reasoning over arbitrary capabilities. Attestation authority is captured directly in the logical relation: successful attestation produces capabilities whose authority reflects the enclave's attested identity and permissions. The three application proofs in §5 compose the universal contract with the modeled CHERI-TrEE instructions and establish the end-to-end properties post-attestation. To address the request for an explicit connection, we will add a lemma in the revised §3.2 showing preservation of the relation under the attestation call, including how the client's authority view is updated. This will make the transfer to the application proofs fully explicit. revision: yes

  2. Referee: [§4] §4 (CHERI-TrEE Extension): The formalization of the enclave primitives as an extension to Cerise is load-bearing for the adequacy claim, yet the paper provides only an informal correspondence argument rather than a simulation or refinement relation between the extended machine semantics and the proposed CHERI-TrEE hardware behavior. This leaves open whether the mechanized proofs validate the intended hardware model or merely an over-approximation thereof.

    Authors: The mechanized model extends Cerise precisely with the enclave instructions and semantics as specified in the CHERI-TrEE design proposal. Adequacy of the program logic holds with respect to this model. A full simulation or refinement to hardware-level semantics would require a separate formalization of the CHERI-TrEE hardware, which is not available in the literature and lies outside the paper's scope. In the revision we will expand §4 with a detailed informal correspondence, including an explicit mapping of each modeled primitive to the proposal's specification, to clarify that the model is not an over-approximation of the intended behavior. revision: partial

Circularity Check

0 steps flagged

No circularity: mechanized logical relations and independent universal contract

full rationale

The derivation defines Cerisier via Iris logical relations for capability authority (extending Cerise), states a universal contract for untrusted code that independently captures capability safety plus attestation tracking, and then proves end-to-end properties for three applications. All steps are machine-checked in Rocq; the contract is not defined in terms of the application theorems, no parameters are fitted to data, and no self-citation chain is load-bearing for the central claims. The mechanization supplies external verifiability, keeping the chain self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based solely on the abstract, no free parameters are mentioned. The work relies on standard Iris separation logic axioms and the domain assumption that the CHERI-TrEE proposal can be faithfully modeled as an extension to Cerise. No new invented entities are introduced.

axioms (1)
  • domain assumption The CHERI-TrEE enclave primitives can be faithfully formalized as an extension to the Cerise capability machine.
    The paper states it formalizes a recent proposal as an extension to Cerise.

pith-pipeline@v0.9.0 · 5524 in / 1305 out tokens · 51853 ms · 2026-05-10T12:10:03.696033+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages · 1 internal anchor

  1. [1]

    Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters

    Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2021. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. Cerisier: A Program Logic for Attestation in a Capability Machine 23 In34th IEEE Computer Security Foundations Symposium, CSF 2021,...

    work page doi:10.1109/csf51468.2021.00048 2021

  2. [2]

    Maicc: A lightweight many-core architecture with in-cache computing for multi-dnn parallel inference,

    Saar Amar, David Chisnall, Tony Chen, Nathaniel Wesley Filardo, Ben Laurie, Kunyan Liu, Robert Norton, Simon W. Moore, Yucong Tao, Robert N. M. Watson, and Hongyan Xia. 2023. CHERIoT: Complete Memory Safety for Embedded Devices. InProceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture(Toronto, ON, Canada)(MICRO ’23). Associat...

    work page doi:10.1145/3613424 2023

  3. [3]

    2022.Arm Architecture Reference Manual Supplement Morello for A-Profile Architecture

    ARM Ltd. 2022.Arm Architecture Reference Manual Supplement Morello for A-Profile Architecture. ARM Ltd. https: //documentation-service.arm.com/static/61e577e1b691546d37bd38a0?token= Document number DDI0606

    work page 2022

  4. [4]

    Manuel Barbosa, Bernardo Portela, Guillaume Scerri, and Bogdan Warinschi. 2016. Foundations of Hardware-Based Attested Computation and Application to SGX. InIEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016. IEEE, 245–260. doi:10.1109/EUROSP.2016.28

    work page doi:10.1109/eurosp.2016.28 2016

  5. [5]

    Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter Sewell. 2022. Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. InProgramming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European...

    work page doi:10.1007/978-3-030-99336-8_7 2022

  6. [6]

    Marton Bognar, Jo Van Bulck, and Frank Piessens. 2022. Mind the Gap: Studying the Insecurity of Provably Secure Embedded Trusted Execution Architectures. In43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 1638–1655. doi:10.1109/SP46214.2022.9833735

    work page doi:10.1109/sp46214.2022.9833735 2022

  7. [7]

    Marton Bognar, Job Noorman, and Frank Piessens. 2023. Proteus: An Extensible RISC-V Core for Hardware Extensions. InRISC-V Summit Europe ’23

    work page 2023

  8. [8]

    Ferdinand Brasser, Brahim El Mahjoub, Ahmad-Reza Sadeghi, Christian Wachsmann, and Patrick Koeberl. 2015. TyTAN: tiny trust anchor for tiny devices. InProceedings of the 52nd Annual Design Automation Conference, San Francisco, CA, USA, June 7-11, 2015. ACM, 34:1–34:6. doi:10.1145/2744769.2744922

    work page doi:10.1145/2744769.2744922 2015

  9. [9]

    Carter, Stephen W

    Nicholas P. Carter, Stephen W. Keckler, and William J. Dally. 1994. Hardware Support for Fast Capability-based Addressing. InInternational Conference on Architectural Support for Programming Languages and Operating Systems. ACM, 319–327. doi:10.1145/195473.195579

    work page doi:10.1145/195473.195579 1994

  10. [10]

    Guoxing Chen and Yinqian Zhang. 2022. MAGE: Mutual Attestation for a Group of Enclaves without Trusted Third Parties. In31st USENIX Security Symposium, USENIX Security 2022, Boston, MA, USA, August 10-12, 2022, Kevin R. B. Butler and Kurt Thomas (Eds.). USENIX Association, 4095–4110. https://www.usenix.org/conference/usenixsecurity22/ presentation/chen-guoxing

    work page 2022

  11. [11]

    2016.Intel SGX Explained

    Victor Costan and Srinivas Devadas. 2016.Intel SGX Explained. Technical Report 086. https://eprint.iacr.org/2016/086

    work page 2016

  12. [12]

    and Van Horn, Earl C

    Jack B. Dennis and Earl C. Van Horn. 1966. Programming semantics for multiprogrammed computations.Commun. ACM9, 3 (1966), 143–155. doi:10.1145/365230.365252

    work page doi:10.1145/365230.365252 1966

  13. [13]

    Dominique Devriese, Lars Birkedal, and Frank Piessens. 2016. Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. InIEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016. IEEE, 147–162. doi:10.1109/EUROSP.2016.22

    work page doi:10.1109/eurosp.2016.22 2016

  14. [14]

    2021.CheriOS: Designing an Untrusted Single-Address-Space Capability Operating System Utilising Capability Hardware and a Minimal Hypervisor

    Lawrence Esswood. 2021.CheriOS: Designing an Untrusted Single-Address-Space Capability Operating System Utilising Capability Hardware and a Minimal Hypervisor. Ph. D. Dissertation. University of Cambridge. https://www.repository. cam.ac.uk/handle/1810/326715

    work page 2021

  15. [15]

    Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software. InSymposium on Operating Systems Principles (SOSP ’17). ACM, 287–305. doi:10.1145/3132747.3132782

    work page doi:10.1145/3132747.3132782 2017

  16. [16]

    Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey D. Son, Timo...

    work page doi:10.1109/sp40000.2020.00098 2020

  17. [17]

    Gutstein, Jonathan Woodruff, Jessica Clarke, Peter Rugg, Brooks Davis, Mark Johnston, Robert Norton, David Chisnall, Simon W

    Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Jessica Clarke, Peter Rugg, Brooks Davis, Mark Johnston, Robert Norton, David Chisnall, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson. 2024. Cornucopia Reloaded: Load Barriers for CHERI Heap Temporal Safety. InProceedings of the 29th ACM International Conference on Architectural S...

    work page doi:10.1145/3620665.3640416 2024

  18. [18]

    Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. 2024. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.J. ACM 24 June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal 71, 1 (Feb. 2024), 1–59. do...

    work page doi:10.1145/3623510 2024

  19. [19]

    Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal. 2021. Efficient and Provable Local Capability Revocation Using Uninitialized Capabilities.Proceedings of the ACM on Programming Languages5, POPL (Jan. 2021), 6:1–6:30. doi:10.1145/3434287

    work page doi:10.1145/3434287 2021

  20. [20]

    Aïna Linn Georges, Alix Trieu, and Lars Birkedal. 2022. Le Temps Des Cerises: Efficient Temporal Stack Safety on Capability Machines Using Directed Capabilities.Proceedings of the ACM on Programming Languages6, OOPSLA1 (April 2022), 74:1–74:30. doi:10.1145/3527318

    work page doi:10.1145/3527318 2022

  21. [21]

    Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, and Peter Sewell. 2025. Morello- Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture.Proc. ACM Program. Lang.9, PLDI (June 2025), 226:1961–226:1983. doi:10.1145/3729329

    work page doi:10.1145/3729329 2025

  22. [22]

    Morley Mao, and Henry X

    Shengtuo Hu, Qi Alfred Chen, Jiwon Joung, Can Carlak, Yiheng Feng, Z. Morley Mao, and Henry X. Liu. 2020. CVShield: Guarding Sensor Data in Connected Vehicle with Trusted Execution Environment. InProceedings of the Second ACM Workshop on Automotive and Aerial Vehicle Security (AutoSec ’20). Association for Computing Machinery, 1–4. doi:10.1145/3375706.3380552

    work page doi:10.1145/3375706.3380552 2020

  23. [23]

    Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2011. Separation Logic in the Presence of Garbage Collection. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. IEEE, Toronto, ON, Canada, 247–256. doi:10.1109/ LICS.2011.46 http://ieeexplore.ieee.org/document/5970244/

    work page arXiv 2011

  24. [24]

    Sander Huyghebaert, Steven Keuchel, Coen De Roover, and Dominique Devriese. 2023. Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts. InProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, CCS 2023, Copenhagen, Denmark, November 26-30, 2023, Weizhi Meng, Christian Damsgaard Jensen, Cas Crem...

    work page doi:10.1145/3576915.3616602 2023

  25. [25]

    Moore, Alex Bradbury, Hongyan Xia, Robert N.M

    Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon W. Moore, Alex Bradbury, Hongyan Xia, Robert N.M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A. Theodore Markettos. 2017. Efficient Tagged Memory. In2017 IEEE Internationa...

    work page doi:10.1109/iccd.2017.112 2017

  26. [26]

    Ralf Jung, Robbert Krebbers, Jacques-henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic.Journal of Functional Programming28 (2018), e20. doi:10.1017/S0956796818000151

    work page doi:10.1017/s0956796818000151 2018

  27. [27]

    Xiaoguo Li, Bowen Zhao, Guomin Yang, Tao Xiang, Jian Weng, and Robert H. Deng. 2023. A Survey of Secure Computation Using Trusted Execution Environments. arXiv:2302.12150 doi:10.48550/ARXIV.2302.12150

    work page doi:10.48550/arxiv.2302.12150 2023

  28. [28]

    Maene, J

    P. Maene, J. Götzfried, R. de Clercq, T. Müller, F. Freiling, and I. Verbauwhede. 2018. Hardware-Based Trusted Computing Architectures for Isolation and Attestation.IEEE Trans. Comput.67, 3 (March 2018), 361–374. doi:10.1109/ TC.2017.2647955

    work page arXiv 2018

  29. [29]

    Morris, Jr

    James H. Morris, Jr. 1973. Protection in Programming Languages.Commun. ACM16, 1 (Jan. 1973), 15–21. doi:10.1145/ 361932.361937

    work page arXiv 1973

  30. [30]

    Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. 2020. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. In2020 IEE...

    work page doi:10.1109/sp40000.2020.00055 2020

  31. [31]

    Job Noorman, Jo Van Bulck, Jan Tobias Mühlberg, Frank Piessens, Pieter Maene, Bart Preneel, Ingrid Verbauwhede, Johannes Götzfried, Tilo Müller, and Felix Freiling. 2017. Sancus 2.0: A Low-Cost Security Architecture for IoT Devices. ACM Transactions on Privacy and Security20, 3 (July 2017), 7:1–7:33. doi:10.1145/3079763

    work page doi:10.1145/3079763 2017

  32. [32]

    Ivan De Oliveira Nunes, Karim Eldefrawy, Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. 2019. VRASED: A Verified Hardware/Software Co-Design for Remote Attestation. In28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019, Nadia Heninger and Patrick Traynor (Eds.). USENIX Association, 1429–1446. https:/...

    work page 2019

  33. [33]

    Andrew M. Pitts. 2010. Step-Indexed Biorthogonality: a Tutorial Example. InModelling, Controlling and Reasoning About State, 29.08. - 03.09.2010 (Dagstuhl Seminar Proceedings, Vol. 10351), Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany. http://drops.dagstuhl.de/ opus/volltexte/...

    work page 2010

  34. [34]

    June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal. 2026. Cerisier: A Program Logic for Attestation in a Capability Machine. arXiv:2604.13638 doi:10.48550/arXiv.2604.13638

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2604.13638 2026

  35. [35]

    June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal. 2026. Cerisier - Code repository. https://github.com/logsem/cerisier

    work page 2026

  36. [36]

    June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal. 2026. Cerisier: A Program Logic for Attestation in a Capability Machine (Artifact). doi:10.5281/zenodo.19062990 Cerisier: A Program Logic for Attestation in a Capability Machine 25

    work page doi:10.5281/zenodo.19062990 2026

  37. [37]

    Muhammad Usama Sardar, Saidgani Musaev, and Christof Fetzer. 2021. Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification.IEEE Access9 (2021). doi:10.1109/ACCESS.2021.3087421

    work page doi:10.1109/access.2021.3087421 2021

  38. [38]

    Carlton Shepherd, Raja Naeem Akram, and Konstantinos Markantonakis. 2017. Establishing Mutually Trusted Channels for Remote Sensing Devices with Trusted Execution Environments. InARES (ARES ’17). Association for Computing Machinery, 1–10. doi:10.1145/3098954.3098971

    work page doi:10.1145/3098954.3098971 2017

  39. [39]

    Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2021. StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities.Journal of Functional Programming31 (2021), e9. doi:10.1017/ S095679682100006X

    work page 2021

  40. [41]

    Eijiro Sumii and Benjamin C. Pierce. 2003. Logical relations for encryption.Journal of Computer Security11, 4 (2003), 521–554. doi:10.3233/JCS-2003-11403

    work page doi:10.3233/jcs-2003-11403 2003

  41. [42]

    Thomas Van Strydonck, Aïna Linn Georges, Armaël Gueneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese. 2022. Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines. InIEEE Computer Security Foundations Symposium (CSF). 80–95. doi:10.1109/CSF54842.2022.9919645

    work page doi:10.1109/csf54842.2022.9919645 2022

  42. [43]

    Thomas Van Strydonck, Job Noorman, Jennifer Jackson, Leonardo Alves Dias, Robin Vanderstraeten, David Oswald, Frank Piessens, and Dominique Devriese. 2023. CHERI-TrEE: Flexible Enclaves on Capability Machines. In2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P). IEEE, Delft, Netherlands, 1143–1159. doi:10.1109/ EuroSP57164.2023.00070 http...

    work page arXiv 2023

  43. [44]

    Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, Graeme Barnes, David Chisnall, Jessica Clarke, Brooks Davis, Lee Eisen, Nathaniel Wesley Filardo, Franz A. Fuchs, Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan N...

    work page doi:10.48456/tr-987 2023

  44. [45]

    Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav H. Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert M. Norton, Michael Roe, Stacey D. Son, and Munraj Vadera. 2015. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compart- mentalization. In2015 IEE...

    work page doi:10.1109/sp.2015.9 2015

  45. [46]

    Hasini Witharana, Hansika Weerasena, and Prabhat Mishra. 2024. Formal Verification of Virtualization-Based Trusted Execution Environments.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems43, 11 (Nov. 2024), 4262–4273. doi:10.1109/TCAD.2024.3443008

    work page doi:10.1109/tcad.2024.3443008 2024

  46. [47]

    Sara Zain, Jannik Mähn, Stefan Köpsell, and Sebastian Ertel. 2025. Formally-Verified Security against Forgery of Remote Attestation Using SSProve. arXiv:2502.17653 [cs] doi:10.48550/arXiv.2502.17653 26 June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal A Operational Semantics 𝑖 J𝑖K(𝜎) Conditions fail ...

    work page doi:10.48550/arxiv.2502.17653 2025