~/talk

Cerisier: A Program Logic for Attestation in a Capability Machine

on YouTube 16m
Talkat PLDI 2026 · 2026-06-15..06-19· [security]

speakers

name:June Rousseau
links:none on file
name:Denis Carnier
links:none on file
name:Thomas Van Strydonck
links:none on file
name:Steven Keuchel
links:none on file
name:Dominique Devriese
linkedin:dominique-devriese-9905757
name:Lars Birkedal
linkedin:lars-birkedal-71b8954b

resources

video:https://youtu.be/SiZb2vF4Ufk
slides:none on file

summary

Cerisier presents a program logic that formalizes CHERI-TrEE support for enclaves on a capability machine and claims modular, end-to-end proofs for systems mixing trusted, untrusted and attested code. The development is fully mechanized: ~35,000 lines in Iris and the Rocq Prover, with reusable artifacts available. Key technical pieces are a universal contract for untrusted code based on a logical relation, memory-revocation reasoning, symbolic signing predicates, and case studies proving security for secure outsourced computation, mutual attestation, and trusted sensor using Iris+Rocq.

AI-written summary · about

chapters (9)

  1. 0:00Cerisier and attestation intro
  2. 1:04Secure computation outsourcing problem
  3. 3:54Attestation example breakdown
  4. 5:40Verifying enclaves challenges
  5. 7:45Cherry Tree sealing and sweep
  6. 9:54Enclave maps attestation reasoning
  7. 11:39End-to-end proof example
  8. 12:20Complex case studies
  9. 13:03Conclusion and Iris verification

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.