PaperlayerView exact revision on arXiv

Source-linked AI summary

Griotte: Verified Compartmentalisation via Capabilities

June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal

arXiv:2609.01110v1cs.PLcs.CR

TL;DR

CHERIoT’s compartment model raises formalisation and assurance questions because isolation depends jointly on hardware capabilities and the switcher. The paper answers them with faithful Griotte models, a continuation-based logical relation, verified switcher specifications, and modular case studies demonstrating the resulting security properties.

  • Problem

    The paper asks how to formalise CHERIoT compartmentalisation and assure the switcher’s security role alongside the capability machine.

  • Method

    The authors develop Griotte and Griotte OS, faithful idealised CHERIoT models with a continuation-based logical relation and specifications for cross-compartment switcher calls.

  • Results

    The paper proves the stated properties in Griotte, verifies that the switcher implementation meets its specifications, and proves representative compartment case studies correct.

  • Takeaways & Limitations

    The results provide a formal foundation for CHERIoT’s compartment model by composing individual compartment specifications with capability and switcher reasoning.

  • Takeaways & Limitations

    The case-study assurance assumes the concrete code of known compartments while treating unknown compartments as potentially adversarial, with imports and exports known.

Abstract

from arXiv · show

CHERIoT is a novel hardware-software co-design that leverages hardware capabilities to define a notion of compartment, in a minimalistic capability-based OS, CHERIoT RTOS. By default, compartments are isolated to limit damage in case of bugs or malicious behaviour. To allow cross-compartment communication, the OS provides a privileged component, called the switcher. The switcher provides an interface for cross-compartment calls, while enforcing isolation between compartments and guaranteeing stack safety. Together with hardware capabilities, the switcher is critical to enforce the security guarantees of the CHERIoT compartment model. The design of CHERIoT raises two questions: First, how can one formalise the informal notion of compartmentalisation that CHERIoT compartments are designed to provide? And second, given that the safety properties of CHERIoT hinge on the complementary roles of the capability machine and of the switcher, does the design of CHERIoT enforce the desired security properties? In this paper, we introduce Griotte and Griotte OS, idealised but faithful versions of the CHERIoT machine and the CHERIoT RTOS, which we use to answer these two questions: First, we formally capture the aforementioned security guarantees in the form of a continuation-based logical relation which captures the combined behaviour of the switcher and of the capability machine. And second, we define a specification for the Griotte switcher that enforces those guarantees, and prove that the implementation meets the specification. We demonstrate Griotte on a range of key scenarios illustrating different aspects of CHERIoT, including integrity of the local state in the presence of memory sharing with unknown code. Our approach is modular: we verify compartments individually, and then compose their specifications. Together, our contributions give a solid formal foundation to the design of CHERIoT.

1 Introduction

CHERIoT uses hardware capabilities and a privileged switcher to isolate compartments while enabling controlled cross-compartment calls. The paper formalises these guarantees and verifies them in faithful idealised models of CHERIoT.

  • CHERIoT compartments default to their own code and private memory, while imports, exports, and the switcher enable controlled communication.Cross-compartment calls can share explicitly provided capabilities.
  • The switcher enforces least privilege by replacing the caller’s root code, data, and stack capabilities with those of the called compartment.This is intended to limit buggy or malicious compartments to explicitly granted access.
  • The design leaves open how compartmentalisation should be formalised and whether the switcher and capability machine provide the required assurance.
  • Griotte and Griotte OS are idealised but faithful CHERIoT models used to characterise stack safety, no-capture, IMUD, and extended capability safety.The paper proves these properties in Griotte and illustrates them with case studies.
  • The paper develops a program logic, continuation-based logical relation, switcher specifications and proof, assumptions, and end-to-end case studies.The contributions include support for deep local and deep immutable capabilities.

2 Technical Overview

The technical overview shows how capability safety and switcher correctness jointly establish isolation, no-capture, and integrity in representative compartment examples. The proof approach combines program logic, logical relations, and continuation reasoning for cross-compartment calls.

  • Griotte case studies rely on both capability safety and correct switcher behavior to verify compartmentalisation properties.The examples cover IMUD and no-capture as simplified CHERIoT use cases.
  • Isolation of Multiple Untrusted Domains.: B cannot alter c after receiving access only to b, because capability rules prevent reaching c through pointer arithmetic or buffer overflow.The shared capability covers only [b,b+1).
  • Isolation of Multiple Untrusted Domains.: C observes b unchanged at 42 because K never shares b with C and B cannot transfer b’s capability without communicating with C.The example also depends on known imports and exports and switcher isolation.
  • No-Capture.: Deep local capabilities downgrade loaded capabilities to local, and clearing the callee’s stack prevents B from retaining access to i after returning.The second call therefore tests that B cannot capture i.
  • How We Prove It: The proof method uses a program logic for known code and a logical relation capturing capability safety for arbitrary unknown code.Arguments shared with adversaries must be shown safe to share.
  • How We Prove It: A continuation relation models logical stacks, worlds, compartment names, safe switcher returns, and linear framing across cross-compartment calls.This supports reasoning about return control flow and preserved resources.

U K U’

Griotte’s proof structure tracks call-stack evolution, technical logical-relation goals, framing, and world transitions around known, unknown, and switcher code. The paper also presents these ingredients as a general structure for hardware-software-enforced isolation.

  • Call stack: The logical call stack records frames such as s, k, and k′, with each pushed frame creating an obligation discharged when the switcher returns.
  • Technical Proof Goal: Entry into code requires an EEntryPoint goal, while switcher return requires an EK goal for safely executing from the prior logical call stack.
  • Framing: Framing preserves separation-logic resources not used by the switcher specification after return.
  • Worlds: Kripke worlds distinguish permissive private transitions in known code from constraining public transitions in unknown code and switcher transitions.Switcher transitions are shown to be public.
  • The proposed structure combines logical relations, continuation relations, universal contracts, precise and loose cross-domain specifications, and world or domain parameters.The authors believe it can generalise beyond CHERIoT to OS and hypervisor isolation.

3 Design of the Griotte Machine and the Griotte OS

Griotte extends the Cerise capability machine with CHERIoT-specific permissions and privilege levels, then builds an OS whose switcher manages compartment communication and shared-stack safety.

  • Griotte Machine: Griotte extends Cerise with deep locality, deep immutability, privileged execution, and corresponding special-register instructions.These features include lg, dl, lm, dro, xsr, readSR, and writeSR.
  • Griotte Machine: Capabilities combine permissions, locality, authority bounds, and current addresses to control memory access.Successful access requires the current address to fall within the capability’s bounds and the permission to authorize the action.
  • Griotte Machine: Deep capabilities propagate restrictions to loaded words, enabling inherited deep locality and deep immutability.This addresses limitations of shallow capabilities, whose reachable capabilities can retain broader locality or write authority.
  • Griotte OS: A compartment contains code, data, and sealed or sentry capability structures, while machine state comprises registers, memory, and execution state.Griotte distinguishes general and special registers; the switcher uses the privileged mtdc register for its trusted stack.
  • Griotte OS: Griotte provides hardware memory-safety primitives as the foundation for a lightweight compartment model modeled after CHERIoT RTOS.The OS uses these primitives to support compartment execution and protected cross-compartment calls.
  • The Switcher: The switcher enforces cross-compartment isolation by validating, saving, restricting, and restoring the shared compartments’ stack capability.It excludes the caller’s used frame from the callee’s bounds and zeroes the callee’s frame to prevent stack-frame access and capability leakage.

4 Program Logic

The Griotte program logic supports modular reasoning about programs running on the capability machine. Built on Iris separation logic, it specifies executions while preserving logical invariants.

  • Program Logic: Griotte’s program logic adapts earlier capability-machine reasoning with rules for Griotte’s additional instructions.The paper presents useful notation rather than explaining the full logic in detail.
  • Program Logic: The logic is built on Iris separation logic using points-to predicates for memory, registers, special registers, and complete register files.Register-file assertions combine individual register points-to predicates with separating conjunction.
  • Program Logic: The specification form {P} ⇝• states that executions starting from P preserve logical invariants and may diverge, halt, or stop safely with an error.The specification characterizes safe execution without requiring termination.

5 Logical Relation

The section defines a logical relation for Griotte that models capability authority, memory invariants, compartment-specific views, and the switcher’s continuation behavior. Its Fundamental Theorem connects safe sharing with safe execution for unknown code.

  • Logical relation: The logical relation combines a program logic with a continuation relation to model unknown code and the switcher’s behavior.The continuation relation supports precise switcher specifications and matches their postcondition.
  • Worlds: A Kripke world tracks memory invariants through public transitions that preserve all invariants and private transitions that preserve only non-revocable invariants.Worlds contain standard state for shared regions and custom state for private regions.
  • Worlds: Griotte’s standard invariant states are Permanent, Temporary, and Revoked, distinguishing persistent sharing, revocable sharing, and locations with no enforced safety guarantee.Permanent states remain safe after private transitions; Temporary states may be revoked by private transitions.
  • Relations: The value relation states when a word is safe to share with a compartment, while the expression relation states when it is safe for that compartment to execute.The value relation also captures the authority held by the word.
  • Fundamental theorem: The FTLR proves that any word safe to share is safe to execute, yielding a universal contract for arbitrary unknown code.The proof shows that instructions preserve safe-to-share register contents and comprises approximately 2500 lines of Rocq.

6 Specification and Proof of the Griotte Switcher

This section specifies the Griotte switcher’s cross-compartment calls and returns, then proves that its implementation satisfies those specifications. The specifications support both known callers and unknown code while preserving stack safety and well-bracketed control flow.

  • Proof: The implementation satisfies the formal specifications for cross-compartment calls and returns.The section presents precise specifications for known code and shareability specifications for unknown code.
  • Switcher invariant: The switcher invariant captures private switcher state, entry-point sealing, and synchronization between the logical call-stack and trusted physical stack.Together, these conditions model that only the switcher can change the logical call-stack.
  • Known-code specification: The call specification requires shareable arguments and entry points, the callee’s stack resources, the current world, and the caller’s continuation relation.The entry point’s shareability combines with the FTLR to provide a specification for unknown code.
  • Known-code specification: The call postcondition returns a public future world, shareable return values, and the callee’s stack resources after temporary adversary access.Stack clearing on return supports safe revocation of the callee’s stack-frame access.
  • Unknown-code interface: The safety theorem states that cross-compartment call and return sentries are safe to share when world transitions at call boundaries are public.This permits unknown code to invoke the switcher under the specified sharing conditions.

7 Adequacy — Putting It All Together

The adequacy results connect loader-final initial states, program-logic specifications, and the universal contract for unknown code. Under these assumptions, assertions remain successful throughout execution.

  • Initial state: A loader-final state specifies compartment initialization, disjoint memory regions, switcher initialization, assertion checking, and initial register contents.Adversarial code and data contain arbitrary integers or capabilities pointing within the data section, while import and export tables are case-study-specific.
  • Result: The end-to-end theorems state that the assertion flag remains 0 at every execution step.Equivalently, none of the assertions fail.
  • Adequacy theorem: The end-to-end adequacy theorem assumes a loader-final state and a program-logic specification for the assertion flag.Under these conditions, the assertions never fail.
  • Proof strategy: The proof combines program-logic reasoning for known code with the FTLR-derived universal contract when unknown code executes.This combination establishes the required assumption of the adequacy theorem.

8 Case Studies

The case studies use Griotte’s program logic, logical relation, and switcher specifications to verify small but challenging CHERIoT examples. They cover compartmentalisation, IMUD, no-capture, deep capabilities, WBCF, dangling-pointer protection, and stack safety.

  • Verification approach: The verification approach combines Griotte’s program logic and logical relation with specifications of the switcher’s cross-compartment calls.The examples are proved correct using the approach introduced earlier, with register-related proof details omitted in the sketch.
  • Compartmentalisation example: Sharing b with compartment B requires allocating a permanent invariant, relinquishing local points-to ownership, and proving that b’s contents satisfy the invariant.Because integers are always safe, the proof can preserve ownership of c across B’s call, supporting the first assertion.
  • Compartmentalisation example: IMUD permits the proof of C’s call to retain control over b while b’s invariant remains open, because B and C are disjoint compartments.The proof allocates a permanent invariant for c and uses the disjointness of the compartments to maintain knowledge that b contains 42 during C’s call.
  • Compartmentalisation example: The proof of the compartmentalisation example establishes that the final assertion holds after C.g by framing b↦42 around the switcher specification.This follows the earlier preservation of b’s invariant and the public future world returned after B.f.
  • Other case studies: The case studies also verify no-capture of deep local capabilities and correctness of examples relying on deep immutability, WBCF, dangling-pointer protection, and stack safety.The authors report additional correct case studies, including adapted integrity examples and the Very Awkward Example, Downward Local-State Encapsulation, and Stack Objects.

9 Related Work

Related work addresses secure calling conventions, capability safety, system isolation, and reasoning about interactions with untrusted code. Griotte differs by integrating a verified switcher with a logical relation that captures unknown-code effects and compartment-specific guarantees.

  • Verifying calling conventions: Cerise work verifies secure calling conventions for capability machines, but does not support deep permissions or multiple untrusted domains in the same way as Griotte.Those calling conventions also do not rely on a privileged compartment like the CHERIoT switcher, motivating Griotte’s continuation relation.
  • Verifying calling conventions: Griotte’s examples show desirable switcher behaviour but do not provide a systematic security characterisation such as an overlay semantics and full-abstraction proof.The cited Cerise work provides that broader systematic treatment for some calling-convention guarantees.
  • Verifying calling conventions: Lau and Vijayaraghavan specify the CHERIoT switcher’s exception path and threads, which Griotte does not cover, but their specification is not integrated with a logical relation for unknown code.This distinguishes their scope from Griotte’s treatment of the switcher together with unknown-code effects.
  • Formal verification at scale: Full-scale CHERI verification has established capability monotonicity and, for Morello, capability safety, but not the combined stack-safety and no-capture guarantees addressed by Griotte.RTL model checking has examined some allocator and switcher properties, but not end-to-end integrity and isolation.
  • Other systems interacting with untrusted code: OS and hypervisor verification proves isolation between processes or virtual machines, whereas related systems do not prove end-to-end examples involving IMUD, no-capture, or stack safety.VMSL reasons about clients interacting through part of Arm’s FF-A ABI, while abstracting the hypervisor rather than verifying it like Griotte’s switcher.

10 Conclusion and Future Work

The paper validates Griotte’s formal model of CHERIoT compartmentalisation and switcher security, while identifying important extensions needed for closer correspondence with CHERIoT RTOS.

  • Conclusion: A continuation-based logical relation captures Griotte’s security properties, and verified switcher specifications match the implementation.The work also proves end-to-end correctness for key use cases involving unknown compartments.
  • Conclusion: The approach validates aspects of CHERIoT and provides a first step toward verifying the CHERIoT RTOS.The authors believe the approach may also apply to non-CHERI systems.
  • Future Work: The idealised machine omits exceptions, although exceptions are a crucial complexity in real-time operating systems and cross-compartment calls.This is identified as future work rather than a property covered by the current model.
  • Future Work: The model assumes a single-core machine and does not implement CHERIoT’s high-water-mark stack-clearing optimisation.Concurrency would complicate both the machinery and correctness statements, while the optimisation is expected to require additional ghost states.

F.2 Deep Immutability

The deep-immutability example shares a deeply immutable capability with an unknown compartment and formally preserves the local value despite that compartment’s access.

  • Example Setup: Deep immutability is the key CHERIoT feature demonstrated by the example.The scenario uses a known compartment K and an adversary compartment B.
  • Example Setup: K stores 42 in i, stores a writable capability to i in pi, then shares a read-only deep-immutable capability to pi with B.The shared capability is constructed with RO_DRO and global locality.
  • Proof: B cannot modify i because the capability it obtains through the deeply immutable pointer lacks write permission.The proof associates a read-only invariant with pi and a value invariant stating that i remains 42.
  • Result: After B returns, the proof recovers i ↦→ 42, establishing the assertion that i == 42.The value invariant is preserved across the cross-compartment call.

F.3 Well Bracketed Control Flow: Very Awkward Example (VAE)

The Very Awkward Example shows that correctness under adversarial cross-compartment calls relies on well-bracketed control flow, which the switcher enforces through trusted-stack management.

  • Setup: K.awk resets a, invokes callback f, resets a again, invokes f again, and asserts that a equals 1.The assertion tests whether adversarial control flow can improperly revisit the second call site.
  • Setup: The example connects known compartment K and adversary compartment B through mutually imported entry points and a callback.B invokes K.awk, while K can invoke an entry point supplied by B.
  • Security argument: Without well-bracketed control flow, the adversary could save the return pointer, re-enter K.awk, reset a, and later return to the second call site.That behavior would invalidate the assertion.
  • Security argument: The switcher enforces well-bracketed control flow by storing return pointers in the caller’s protected compartment stack and popping the trusted stack’s top frame.Consequently, the cross-compartment control flow remains properly nested and the assertion does not fail.
  • Verification: The proof uses the custom part of the logical-relation world to track the value of a.The full proof is implemented in Rocq.

F.4 Protection Against Dangling Pointers

These examples show how CHERIoT protects local state from dangling stack pointers and overlapping stack objects, with stack clearing and dynamic checks supplying the required safeguards.

  • Dangling pointers: Temporal stack safety prevents callers from reading the contents of popped stack frames through dangling pointers.The section adapts a capability-machine example where this property is required for correctness.
  • Dangling pointers: In the dangling-pointer example, adversarial code could obtain K.f’s private capability to a through a stale stack pointer and alter a between invocations.The second invocation would then fail its assertion that a remains 2.
  • Dangling pointers: CHERIoT prevents this attack by clearing the callee’s stack during the switcher’s return.The correctness proof follows from the switcher-return specification, which permits unsafe-to-share stack contents to be discarded.
  • Stack objects: Stack objects create a separate risk because an input pointer supplied by the caller can overlap the callee’s private stack variable y.Adversarial components can collaborate by forwarding that pointer to another callback.
  • Stack objects: A dynamic check that in does not overlap y is sufficient to prove that the integrity assertion cannot fail.The paper reports a proof of this result in the Rocq implementation.
  • Entry-point predicates: The VEntryPoint predicate constrains sealed cross-compartment entry points to carry the resources needed to fetch export metadata and safely execute the target.Its guarantees rely on untrusted components lacking the corresponding sealing and unsealing capabilities.

I Switcher Return Specification

The switcher-return specification formalizes how a known callee returns to its caller: it restores the caller’s saved state, clears the callee frame, updates the logical world, and resumes execution safely.

  • Specification: The paper states a specification for returns from known cross-compartment code to a possibly adversarial caller.This specification is identified as Theorem I.1.
  • Specification: The specification’s post-proof state retains the caller’s stack, compartment resources, frame matching, stack-pointer synchronization, and trusted-stack invariant.The formal preconditions and postconditions include shared resources and revoked-resource accounting.
  • Specification: The caller supplies an initial world when invoking the callee, which may update that world by allocating invariants or revoking resources.The current return world therefore supports few guarantees about the callee’s stack frame.
  • Proof: The switcher proves the return by opening its invariant, popping the top call-stack frame, and recovering the caller’s world and compartment.The proof maintains correspondence between the physical trusted stack and the logical call stack.
  • Proof: It restores the caller’s saved registers, zeroes the callee’s stack frame, reinstates temporary addresses in the world, and clears non-return registers before jumping back.These operations expose the resources required by the return specification while preventing unsafe callee-frame contents from persisting.

J Deriving Safety for Cross-Compartment Entry Points

The entry-point safety derivation combines boundary-specific logical preconditions with capability-safety assumptions to show that exported cross-compartment entry points remain safe to execute.

  • Boundary model: Griotte models interactions between known and unknown code only at switcher boundaries with specific machine states.Those states are captured in the preconditions for EEntryPoint and EK.
  • Entry-point safety: If a compartment’s PCC and CGP are safe to share, its exported cross-compartment entry points are safe to execute in any private future world.This is the central entry-point corollary.
  • Entry-point safety: The proof applies the fundamental theorem for logical relations and checks that the relevant registers contain safe-to-share words.The stack capability, arguments, and return-to-switcher sentry receive specific safety justifications.
  • Allocation: Compartment safety allocation establishes safe PCC and CGP capabilities after extending the world with the compartment’s memory region.The assumptions constrain code to instructions and data to instructions or capabilities within the compartment’s data region.
  • Import tables: Import-table safety is handled by distinguishing switcher-call entries, entries targeting known code, and entries targeting adversary compartments with a common logical name.Each class receives a corresponding safety argument.
Loading 2609.01110v1…