Logic and Examples
The Cerise logics use a combination of program logic and logical relations to reason about interactions between trusted, known, well-behaved code and untrusted, unknown, arbitrary code. The program logics are connected to the operational semantics of the machine via an adequacy theorem, which translates a program logic statement into a statement about the operational semantics.
Cerise consists of a family of projects aiming at verifying different extensions of the vanilla Cerise machine, presented in the Cerise journal paper. This pages presents a list of case studies verified by the Cerise logics. For each examples, we give a link to the corresponding proofs, and a link to an implementation in the interpreter (for a specific adversary).
Cerise capability machine
The original Cerise paper shows how to verify programs that call and are called by untrusted code. Capability bounds and permissions limit access to memory, while sentries let untrusted callers invoke code without exposing its private state.
Sub-buffer sharing
A program restricts a capability’s bounds before sharing a buffer with untrusted code. The adjacent secret lies outside those bounds, so the untrusted code cannot overwrite it.
Paper, §§2.3 and 6.1 · Rocq adequacy proof · Run sub-buffer sharing
Encapsulated counter
A sentry exposes an increment operation while hiding the counter’s private buffer. Untrusted callers can invoke it repeatedly, but the counter remains non-negative.
Paper context, §§2.4 and 6.2 · Rocq adequacy proof · Run the counter
Read-only sharing and local-state encapsulation
A program allocates a buffer and gives untrusted code read-only access. The calling convention protects the saved writable capability, so the buffer’s contents remain unchanged after the call.
Compact local-state variant
Fuller read-only-sharing variant
Dynamic software sealing
A software library creates pairs of seal and unseal functions, hiding values behind unforgeable keys. Keys can be shared with untrusted code; recovering a hidden value requires the matching unseal function.
Interval object
An interval library orders two integer bounds and uses dynamic software sealing to protect their representation. Untrusted clients can create intervals and read their bounds, but cannot change them or make the lower bound exceed the upper bound.
Paper, §§8.1 and 8.3 · Rocq adequacy proof · Run the interval object
Uninitialised and directed capabilities for secure and efficient calling conventions
This variant adds local and uninitialised capabilities for secure stack-based calls. Reused stack memory must be overwritten before it can be read, reducing costly stack clearing to just the current frame on return.
Very Awkward Example (VAE)
A closure sets its private buffer to 0, calls untrusted code, sets it to 1, and calls again. The final check sees 1 even if the untrusted code calls the closure recursively.
Paper, §6.8 · Rocq adequacy proof · Run Very Awkward Example (VAE)
Directed capabilities build on uninitialised capabilities by restricting where stack capabilities can be stored. This prevents access to returned stack frames and makes secure calls possible without any stack clearing.
Downward local-state encapsulation
A closure leaves a pointer to its private buffer on the stack when it returns, without clearing its frame. Directed capabilities prevent callers from recovering that pointer, so the buffer remains unchanged across repeated calls.
Paper, §4.3.1 · Rocq adequacy proof · Run downward local-state encapsulation
Stack object
A function shares an incoming stack object and a newly allocated one with untrusted code. Checking that the incoming object is fully readable and contains only integers prevents it from exposing write access to private stack data.
Cerisier: capability machine with trusted execution enclaves
Cerisier adds enclave creation, exclusive-memory checks, and local attestation to Cerise. These features let clients identify enclave code and establish trust in its results, even when untrusted code creates and invokes the enclave.
Secure outsourced computation
A client delegates a computation to an adversary, which can create and run an enclave. Checking the enclave’s identity and attested result ensures that any result the client accepts equals the expected value, 42.
Mutual attestation
Two enclaves authenticate each other’s results using MAGE, hashing their code separately from their shared identity table. Each enclave can verify the other’s identity and result without a circular dependency between their full identities.
Trusted sensor readout
A reader enclave exclusively owns a modeled sensor, and a transformer enclave attests the reader before doubling its reading. Attesting the transformer lets a client verify that it receives the expected processed reading, 42.
Griotte: compartmentalisation in a capability machine
Griotte adds CHERIoT-style compartments, deep permissions, and a verified switcher for calls between compartments. Together, they let mutually distrustful components share memory and call each other while protecting private memory and stack state. See the Rocq development for the proofs.
Multi-user key-value store
A shared key-value store uses sealed user keys to keep users’ entries separate. A client can store a value, call an adversary that also uses the store, and read back the same value because the adversary lacks its user key.
Mutually distrustful compartments
A client shares a different buffer with each of two untrusted compartments. Because those compartments cannot communicate, each can modify only its own shared buffer, even after the other has been called.
Paper, §§2.1.1 and 8.1 · Rocq code · Run mutually distrustful compartments
Deep immutability
A compartment shares a deeply read-only capability to a buffer containing a writable pointer. Following that pointer also yields read-only access, so the untrusted recipient cannot change the data reached indirectly.
Deep locality
A compartment lends access through a deep-local capability, which makes nested pointers local too. Together with the switcher’s stack clearing, this prevents an adversary from retaining access and changing the data during a later call.
Calling convention: WBCF and stack safety
These examples adapt the Very Awkward Example, stack object, and downward local-state encapsulation from the earlier papers on uninitialised and directed capabilities to Griotte’s calling convention. The switcher enforces well-bracketed control flow (WBCF): calls return in the proper nested order. It also protects private stack data during calls and prevents access to it after return.