Griotte - Verified Compartmentalisation via Capabilities

This directory contains the Rocq mechanisation accompanying the submission "Griotte: Verified Compartmentalisation via Capabilities". It provides a model of a capability machine based on CHERIoT, a minimal implementation of the CHERIoT's RTOS switcher's, and principle to reason about interactions between known and unknown compartments through the switcher.

It also provides a binary (relational) logical relation, used to prove confidentiality properties: two runs of the same known code, which differ only in some secret data, cannot be distinguished by unknown compartments, in the sense that one run halts if and only if the other one does.

Building the proofs

With Docker

Build the Docker image.

$ docker build -t griotte:griotte .

Run the loaded image in a container.

$ docker run -it --hostname griotte --rm griotte:griotte

It will open a container with a shell, at /home/rocq/griotte, under the rocq user. The directory contains the source of the artifact and all the dependencies to build it.

rocq@griotte:~/griotte$ make

Without Docker

Installing the dependencies

Clone this repository

git clone --recursive git@github.com:logsem/griotte.git

If you forgot --recursive

git submodule update --init

With Nix.

For only building the proofs:

nix build

For interactive proving in Emacs, we recommend to install direnv, create a file .envrc as follow:

#!/usr/bin/env bash

use flake . --impure

and to allow direnv in the directory direnv allow. It sets up the environment to contain Rocq and all the dependencies.

With opam.

You need to have opam >= 2.0 installed.

The development is known to compile with Rocq 9.1.1 and Iris 4.5.0. To install those, two options:

• Option 1: create a fresh local opam switch with everything needed:

   opam switch create -y --deps-only --repositories=default,rocq-released=https://rocq-prover.org/opam/released . 4.14.0
   eval $(opam env)

• Option 2 (manual installation):

    opam switch create griotte-test 4.14.0
    # Add the rocq-released repo (skip if you already have it)
    opam repo add rocq-released https://rocq-prover.org/opam/released
    opam update
    # Install dependencies (skip if already installed)
    opam install dune.3.21.0
    opam install rocq-core.9.1.1 rocq-stdlib.9.0.0 rocq-stdpp.1.13.0 rocq-stdpp-bitvector.1.13.0 rocq-iris.4.5.0 rocq-equations.1.3.1+9.1

Troubleshooting

For Option 1, if the invocation fails at some point, either remove the _opam directory and re-run the command (this will redo everything), or do eval $(opam env) and then opam install -y --deps-only . (this will continue from where it failed).

Building

dune build --display short -jN  # replace N with the number of CPU cores of your machine

We recommend that you have 16Gb of RAM+swap. Please be aware that the development takes around 1 to 2 hours to compile.

Checking for admits

The command make check-admitted will grep for 'admit\|Admitted\|ADMITTED' in the Rocq files.

Organisation

The organisation of the theories/ folder is as follows.

Operational semantics opsem/

• registers.v: Defines registers.

• addresses.v: Defines memory addresses.

• otypes.v: Defines otypes.

• machine_base.v: Contains the syntax (permissions, capability, instructions, ...) of the capability machine.

• machine_parameters.v: Defines a number of "settings" for the machine, that parameterize the whole development (e.g. the specific encoding scheme for instructions, etc.).

• machine_parameters_instance.v: Defines a concrete instance of the typeclass MachineParameters.

• griotte_lang.v: Defines the operational semantics of the machine, and the embedding of the capability machine language into Iris.

Program logic program_logic/

• rules_base.v: Contains some of the core resource algebras for the program logic, namely the definition for points to predicates with permissions. It also contains the Hoare triple rules for the fail cases.

• rules.v: Imports all the Hoare triple rules for each instruction. These rules are separated into separate files (located in the rules/ folder).

Proofmode proofmode/

• solve_addr.v, solve_addr_extra.v, solve_pure.v define tactics for reasoning about address arithmetic, and (extensible) pure goals related to the machine.

• memory_region.v: Auxiliary definitions to reason about consecutive range of addresses and memory words.

• proofmode.v and proofmode_instr_rules.v define tactics for automatically finding the right WP rule to apply while proving the specification of known code.

Model of the Kripke worlds model/

The internal model is not supposed to be used by the user of Griotte.

• sts.v: The definition of stsCollection (named sts_full_world in the implementation), and associated lemmas. In particular: private and public future world relations (all these definitions are parameterised by the standard states and two relations over them transitions. These are instantiated in world_std_sts.v).

• world_std_sts.v: Definitions of the standard world and the standard invariant states. Also contains lemmas about standard transitions.

• sts_multiple_updates.v: Auxiliary definitions to reason about multiple updates to a world.

• world_std_revocation.v: Definitions and lemmas to revoke (and restore) the world (setting Temporary invariants to a Revoked state).

• world_ghost_resources.v: Defines the ghost resources needed to interpret the world.

• region_invariants.v: Definitions for standard resources, and the shared resources map sharedResources (named region in the implementation). Contains some lemmas for "opening" and "closing" the map, akin to opening and closing invariants.

• region_invariants_revocation.v: Lemmas for revoking standard resources in the world interpretation.

• region_invariants_allocation.v: Lemmas for allocating a range of standard resources.

• model_interp_stack.v: Definitions and lemmas specific to reasoning about the stack region.

Interface of Kripke World for the user model/

• world_ghost_theory.v: Ghost theory of world interpretation. Clean interface with the model to ease the proofs for the user.

• world_interp_allocation_compartments.v: Lemmas for allocating standard resources for adversary compartments.

• world_interp_stack.v: Extension of the ghost theory of world interpretation, specific to stack region.

Logical relation and FTLR logrel/

• call_stack: Definitions of the logical call-stack resources.

• seal_store.v: Definitions of the resources for sealing predicates.

• logrel.v: The definition of the unary logical relation.

• world_interp_stack.v: A collections of lemmas related to world manipulation in presence of safe-to-share.

• ftlr/monotone.v: Proof of the monotonicity of the value relation with regards to public future worlds, and private future worlds for non local words.

• fundamental.v: Contains Fundamental Theorem of Logical Relations. 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.

• stack_world_resources.v: Definition of resources to have a clean interface with manipulation of the world, for stack region.

Switcher switcher/

• switcher.v: Code of the Griotte switcher.

• clear_registers{,_spec}.v and clear_stack{_spec}.v: Code and specifications of registers and stack clearing, used by the switcher.

• switcher_preamble.v: Definition of the switcher's invariant and sealing predicate for the export table's otype.

• switcher_helpers.v: Helpers lemmas to prove the switcher specifications.

• interp_switcher_{call,return}.v: Proof that the switcher's sentries are safe to execute

• switcher_spec_{call,return}.v: Specification and proofs of the switcher's sentries for known code, invoking unknown code.

Case studies case_studies

• switcher_adequacy.v: Proof of validity of the adversaries exported cross-compartment sealed entry points.

• adequacy_helpers.v: Helper lemmas for adequacy theorems.

• compartment_layout.v: Definition of regular compartment's memory layout, switcher's memory layout, and assert library memory layout.

• macros/* : Specifications for some useful macros

For each examples <name>:

• name.v: contains the code, the initial data, the import table and export table of the known compartment.
• name_spec{_*}.v contains the specifications of the example.
• name_spec{_*}_closure.v contains the specifications of the example, when an entry point for known code is involved.
• name_adequacy.v contains the end-to-end theorem of the example.
• name_concrete.v contains a concrete implementation of the adequacy with a concrete instance of the machine and a concrete adversary.

The case studies are:

• cmdc/: Canonically Mutually Distrustful Compartmentalisation example.

• counter/: Counter compartment incrementing an internal counter.

• dle/: Example using the deep locality (DL) permission.

• droe/: Example using the deep immutability (DRO) permission.

• lse_downward/: Example showing that the switcher protects against dangling pointers.

• vae/: Very Awkward Example. Shows that the switcher's defines a Well Bracketed calling convention.

• stack_object/: Example showing that the switcher can support stack objects, but requires additional checks.

Binary model

The binary model relates two runs of the machine: the implementation run, described by the usual resources (↦ᵣ, ↦ₛᵣ, ↦ₐ), and the specification run, described by a ghost copy of the machine state (↣ᵣ, ↣ₛᵣ, ↣ₐ, and ⤇ e for its current expression). Both runs execute the same code; the logical relation relates pairs of words, and is diagonal except for sealed words, whose payloads may differ. Each directory mirrors its unary counterpart, and files carry a _binary suffix.

Specification side program_logic_binary/

• spec_instance_binary.v: Ghost state of the specification run, its points-to predicates, the invariant spec_ctx tying it to an actual execution, and the generic lemmas to step the specification run.

• memory_region_binary.v: Specification counterparts of the region points-to and codefrag.

• rules_binary/: Rules stepping the specification run, one file per instruction, and the determinism lemma of each instruction.

Proofmode proofmode_binary/

• proofmode_binary.v and proofmode_instr_rules_binary.v define the tactics iInstr_spec/iGo_spec, to step the specification run, and iInstr_lockstep/iGo_lockstep, to step both runs at once.

• register_tactics_binary.v: Specification counterparts of the register-map tactics.

Model of the Kripke worlds model_binary/

Copies of the files of model/ whose definitions involve words, where the shared resources hold a pair of words: one in the implementation memory and one in the specification memory. The other files of model/ are reused unchanged.

Logical relation and FTLR logrel_binary/

• call_stack_binary.v: Call stack of the specification run. The logical relation relates the two call stacks frame by frame.

• seal_store_binary.v: Sealing predicates over pairs of words.

• logrel_binary.v: The definition of the binary logical relation.

• monotone_binary.v, stack_world_resources_binary.v, wp_rules_interp_binary.v: Binary counterparts of the corresponding unary files.

• ftlr_binary/fundamental_binary.v: Contains the binary Fundamental Theorem of Logical Relations. Each case (one for each instruction) is proved in a separate file of ftlr_binary/.

Switcher switcher_binary/

• switcher_preamble_binary.v: The switcher's invariant, holding the switcher's state of both runs.

• clear_registers_spec_binary.v, clear_stack_spec_binary.v, switcher_macros_spec_binary.v: Specifications of the macros used by the switcher.

• interp_switcher_{call,return}_binary.v (and the interp_switcher_call_* files): Proof that the switcher's sentries are in the binary logical relation.

• switcher_spec_{call,return}_binary.v (and the switcher_spec_call_* files): Specification and proofs of the switcher's sentries for known code, invoking unknown code.

• switcher_adequacy_binary.v: Proof of validity of the adversaries exported cross-compartment sealed entry points.

Case studies case_studies_binary/

• adequacy_helpers_binary.v: Helper lemmas for the end-to-end theorems, in particular binary_adequacy, which turns a proof in the binary logical relation into "if the first run halts, then the second run halts".

• fetch_spec_binary.v, switcher_spec_call_diag_binary.v: Specifications of macros used by the examples.

Each example follows the structure of the unary case studies (name_binary.v, name_spec{_*}_binary.v, name_adequacy_binary.v, name_concrete_binary.v). Its end-to-end theorem states that, for two initial memories that differ only in the secret, the first run halts if and only if the second run halts.

The case studies are:

• confidential_stack/: A known compartment keeps a secret in its stack frame, and leaves a stale copy of it above its stack pointer, before calling an unknown compartment.

• confidential_stack_callee/: An unknown compartment calls a known compartment, which stores a secret in its stack frame before returning.

• confidential_cmdc/: Confidentiality variant of the CMDC example: each of two unknown compartments never learns the secret of the other one.

• confidential_write_only/: A known compartment shares with an unknown compartment a write-only capability to a secret.

Assumptions theories/assumptions.v

The file assumptions.v prints the assumptions of the FTLR, and then of each end-to-end theorems of the case studies, for the unary and the binary models.

Uncomment the file to check the assumptions. Be aware that it can be long to execute (10-15 minutes).

The only axiom our theorems depend on is functional, which is well-known to be compatible with Rocq's internal theory.

FunctionalExtensionality.functional_extensionality_dep :
  forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
  (forall x : A, f x = g x) -> f = g

Moreover, our theorem make the following assumptions:

• The typeclass MachineParameters from theories/opsem/machine_parameters.v, which defines well-formed encode/decode functions for instructions and permissions.
• The typeclass memory_layout from the respective *_adequacy.v* files, which defines the memory layout in the initial state of the machine.

Differences with the paper

Some definitions have different names from the paper.

name in paper => name in mechanisation

In the operational semantics:

name in paper	name in mechanisation
Running	Instr Executable
Halted	Instr Halted
Failed	Instr Failed

For technical reasons (so that Iris considers a single instruction as an atomic step), the execution mode is interweaved with the "Instr Next" mode, which reduces to a value. The Seq _ context can then return and continue to the next instruction. The full expression for an executing program is Seq (Instr Executable).

In the model:

name in paper	name in mechanisation
stsCollection	full_sts_world
sharedResources	region
stsRes	world_interp
public transition	std_rel_pub
private transition	std_rel_priv