Cerise: Program verification on a capability machine in presence of untrusted code

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

The complete list of modules in the development can be found in the Table of Contents. We give below an overview of the contents of the formalization.

Operational semantics

• addr_reg: Defines registers and the set of (finite) memory addresses.
• machine_base: Contains the syntax (permissions, capability, instructions, ...) of the capability machine.
• machine_parameters: Defines a number of "settings" for the machine, that parameterize the whole development (e.g. the specific encoding scheme for instructions, etc.).
• cap_lang: Defines the operational semantics of the machine, and the embedding of the capability machine language into Iris.
• machine_run: Defines an executable version of the operational semantics, allowing to use them as an interpreter to run a concrete machine configuration.

Program logic

• region: Auxiliary definitions to reason about consecutive range of addresses and memory words.
• rules.rules_base: Contains some of the core resource algebras for the program logic, namely the definition for points to predicates with permissions.
• rules: Imports all the Hoare triple rules for each instruction. These rules are separated into separate files (located in the rules/ folder).

Logical relation

• logrel: The definition of the logical relation.
• fundamental: Establishes the *fundamental theorem of our logical relation*. Each case (one for each instruction) is proved in a separate file (located in the ftlr/ folder), which are all imported and applied in this file.

Case studies

Building blocks

• examples.macros, examples.macros_new: Some useful macros and their proof (in particular, the crtcls macro used to implement closures).
• examples.malloc: A simple malloc implementation, and its proof.
• examples.assert: Implementation and proof for the assert routine.
• examples.call, examples.callback: A heap based calling convention: the calling convention invokes malloc to dynamically allocate heap space, store the activation record and the locals, and clear all non parameter and continuation registers.
• examples.template_adequacy: Iris adequacy statements specialized to reason about known code interacting with unknown code while maintaining an invariant (over private state).
• examples.template_adequacy_ocpl : Adequacy statement integrating the use of the malloc and assert macro; establishes that assert never fails, by showing as an invariant that the "failure" flag of the assert routine is never raised.

Example programs & libraries

• examples.buffer: Very simple example of a program sharing a statically allocated sub-buffer with an adversary.
• examples.minimal_counter: Simple counter program, only relying on statically allocated memory, sharing an "increment" closure with the adversary.
• examples.lse, examples.lse_adequacy: Example showing how one can reason on capabilities with a RO permission, and in particular obtain than their contents cannot change even after being shared with an adversary. Relies on malloc, assert, and the heap-based calling convention.
• examples.dynamic_sealing, examples.keylist: a library implementing dynamic sealing, with keylist providing its underlying data-structure as an associative list.
• examples.interval, examples.interval_closure: a library of "secure" intervals, using dynamic sealing to provide data abstraction for the concrete representation of intervals.
• examples.interval_client, examples.interval_client_closure, examples.interval_client_adequacy: a client of the interval library, demonstrating the data abstraction properties that it provides.
• examples.adder, examples.adder_adequacy: The simple example detailed in our JFLA article (en/fr). Exposes one closure that enables increasing the value of a reference. The first file proves a separation-logic specification for the system, and the "adequacy" file extracts it into a self-contained statement depending only on the operational semantics.
• examples.counter, examples.counter_preamble, examples.counter_adequacy: A counter module, with an increment, read, and reset closure. Relies on the malloc routine to allocate its memory, and the assert routine to signal failure (which we then prove cannot happen).