Griotte: Verified Compartmentalisation via Capabilities
Listen
Radio episode about this paper
Transcript
Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.
Tom: Next we'll be talking about the paper "Griotte: Verified Compartmentalisation via Capabilities".
Jane: The paper was written by June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod and Lars Birkedal from Aarhus University and Jane Street, United Kingdom (Jane Street).
Tom: Stay tuned as we take you through the paper and discuss its implications.
Jane: We also have Lu with us today — senior AI researcher at Tsinghua.
Tom: We also have Meng with us today — lead engineer at a mysterious AI startup.
Jane: We also have Lalam with us today — the in-house Large Language Model.
Tom: Alright, let's get started.
Title and Core Concept: Tom: We’re diving into a really interesting paper today, "Griotte: Verified Compartmentalisation via Capabilities," which is putting a major focus on how we can structure untrusted code safely. It sounds like the authors, June Rousseau and Aïna Linn Georges among the team, are building this system to isolate components that might fail or even maliciously behave.
Jane: That's right; they aren't just talking about physical separation, but logical separation using hardware capabilities. Think of it as creating a secure container for every piece of software you run.
Lu: The title itself suggests a profound shift in how we view computation, moving away from monolithic trust toward this concept of compartmentalization, which is quite powerful conceptually.
Meng: For us who work with complex systems, the implications are huge; we could be running different AI models or data processing streams on the same hardware without one affecting the other's integrity.
Lalam: It certainly feels like a highly structured approach to building software that has inherent boundaries, giving us a strong starting point for future AI applications.
Tom: We’re seeing this design not just as an isolation tool but as a foundational model for how computation itself should be constrained, and it sets the stage perfectly for our next discussion on the paper's mechanics.
Summary of Mechanism: Tom: The core idea of Griotte is really about managing communication between these isolated compartments using a mechanism they call "the Switcher," which dictates how we prove this safety. It’s not just about physical separation; it’s about a sophisticated control flow managed by that central component.
Jane: The paper shows us that this isn't just about hardware enforcement; it's also about software design, specifically the concept of "no-capture," which is key to ensuring security.
Lu: No-capture is fascinating because it means the Switcher actively manages the state of memory between calls, preventing any temporary data from one compartment from being used or retained by another, which is a massive win for security.
Meng: That stack clearing mechanism is critical for practical safety because it prevents subtle bugs or malicious side effects from surviving a cross-compartment function return.
Lalam: It ensures that even when running dynamic code, the system maintains a consistently clean state, which leads to much more reliable and trustworthy software behavior overall.
Tom: So, we’ve got a clear picture of the architecture: we have isolation enforced by the Switcher, and no-capture ensures that all temporary state is wiped clean upon return. This leads us naturally into how they prove this system mathematically sound.
Improvements and Formal Methods: Tom: The paper moves into how they rigorously prove that this whole system is secure, using formal methods like a continuation-based logical relation and separation logic. They aren't just testing; they are proving it mathematically.
Jane: This formal verification of concepts like "Isolation of Multiple Untrusted Domains" gives us a level of certainty that goes far beyond what typical debugging cycles can achieve.
Lu: The ability to model the entire system using this continuation-based logical relation is such a huge achievement in computer science, it provides a detailed roadmap for future system design.
Meng: This allows us to design safety specifications *before* writing code, guaranteeing that we meet those requirements from an absolute standpoint.
Lalam: It suggests that the very concept of security in software development is changing because we are defining trust mathematically rather than relying on heuristic checks.
Tom: As we wrap up this discussion on verification, it's clear the path toward rigorous proof is a major part of this work, and let's look at how all these advanced features tie into real-world application and future research.
Conclusion: Tom: We’ve seen that "Griotte: Verified Compartmentalisation via Capabilities" provides a robust, formally verified framework for running untrusted code in isolated domains, which is really exciting.
Jane: It seems like the combination of hardware capabilities and this rigorous logical modeling is giving us a powerful tool to ensure reliability in complex systems.
Lu: I think the biggest implication is that this opens the door for AI applications where we can isolate parts of an agent’s reasoning even further than before, making them more trustworthy.
Meng: I'm particularly interested in how this could apply to edge computing devices where resource constraints force us into highly optimized, verified code.
Lalam: This work provides a structural foundation for software that is inherently secure, ensuring that trust is baked directly into the design of a truly robust system.
Tom: So, we’ve been discussing "Griotte: Verified Compartmentalisation via Capabilities," and I hope this has given listeners a real sense of the power and precision behind this work.
Lu: It’s thrilling to think about the possibilities when you can formally prove that such a complex control flow is safe, just imagine is possible!
Meng: I'm eager to see how these verifiable structures translate into actual deployment at scale, since that's where the real engineering impact lies.
Lalam: The path toward more trustworthy software has definitely been clarified by this research.
June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal
Aarhus University · Jane Street, United Kingdom (Jane Street)
cs.PL, cs.CR
Submitted: 2026-09-01
Updated: 2026-09-01
Code: https://github.com/CHERIoT-Platform/cheriot-demos
License: http://creativecommons.org/licenses/by/4.0/
Importance score: 80/100
The gist: The paper details the formal verification of compartmentalization within the Griotte OS using a capability-based security model.
Key concepts
- Compartmentalisation
- A method of logically separating software components to isolate them. Instead of physical separation, it creates secure containers for code, ensuring that if one piece fails or behaves maliciously, it does not compromise the others.
- Switcher
- The central component in the Griotte architecture that manages communication between isolated compartments. It dictates how safety is proven and controls the sophisticated flow of execution between different software components.
- No-capture
- A key security concept ensuring that temporary data (state) from one isolated compartment cannot be used or retained by another when a function returns. This mechanism wipes clean the state for reliable, trustworthy behavior.
- Formal Methods
- The rigorous mathematical process used to prove that the entire system is secure. The paper uses techniques like continuation-based logical relation and separation logic to guarantee safety beyond typical debugging.
Terminology
Summary
The paper details the formal verification of compartmentalization within the Griotte OS using a capability-based security model. It establishes rigorous mathematical guarantees for interactions between known and unknown code by proving that cross-compartment entry points are safe to execute, even when transitioning into private future worlds, thereby ensuring robust isolation and verifiable system integrity.
Cross-Compartment Entry Point Safety (Corollary J.1)
The fundamental result of the paper is Corollary J.1, which states that if a compartment’s Process Capability (PCC) and its associated Data Capability (CGP) are both safe to share in a world W,
then any exported cross-compartment entry points are safe to execute in any private future world W'. This safety is formalized by the transition:
switcher inv W' priv W. E EntryPoint(W)(C) to
This theorem provides the core mechanism for proving that controlled interactions at compartment boundaries maintain system safety.
Proof Foundation via FTLR and Register Safety
Theorem J.1 is proven by applying the FTLR (Theorem 5.1). The proof hinges on demonstrating that all machine registers contain safe to share words.
This conclusion is reached through three key observations:
-
The compartment stack capability (
csp) and the arguments (ca0–canargs) are safe to share, guaranteed by the precondition of E EntryPoint. -
For
cra, the return-to-switcher sentry capability is always safe to share, citing Theorem 6.3. -
All other registers are shown to contain zero, making them
trivially safe to share.
Compartment Safety Allocation (Lemma J.2)
To establish the necessary precondition—that PCC and CGP are safe to share—the authors utilize Lemma J.2 (Compartment safety allocation). This lemma describes how a world W can transition to W', which extends the world with the compartment’s memory regions:
let W':= W [bpcc, epcc) [bcgp, ecgp):= Permanent
The lemma requires that code regions contain only instructions, data contains either instructions or capabilities pointing within the data region, and crucially, it assumes that if the PCC and the CGP capabilities of the compartment are safe in the world W', then we can prove that the imports are safe to share in W'.
Handling Import Table Capabilities
A critical challenge addressed is proving that the import table is safe to share, as it may contain capabilities that point outside the compartment.
The paper distinguishes three types of entries within this import table:
-
Cross-compartment switcher call entry points, which rely on Theorem 6.3.
-
Cross-compartment entry points targeting known code, requiring proof that the target is a valid entry point and that
the function is safe to execute.
-
Cross-compartment entry points targeting another adversary compartment, which must all be labeled by the same logical compartment name, resulting in safety similar to a self-importing cross-compartment entry point.
Improvements for AI systems
The primary value derived from this paper lies in its rigorous formal treatment of secure state transitions and capability management across trust boundaries. Current AI systems, particularly those relying on complex, multi-stage inference pipelines or interacting with untrusted external environments (e.g., APIs, physical actuators), lack the formal guarantees provided by the PCC/CGP capability model and the compartmentalization structure.
I propose improvements in three highly specific areas: Verifiable AI Pipelines, Capability-Based Trust Modeling for LLMs, and Formalized Runtime Monitoring.
Improvement: Implement a formal framework, inspired by the EEntryPoint and E K transitions, to model the execution flow of multi-stage AI reasoning pipelines. This moves beyond simple input/output validation to guarantee that the state passed between functional modules (the compartments
) is structurally sound and adheres to predefined safety invariants.
Mechanism:
-
State Contracts: Every module boundary must be defined by a formal contract specifying the exact set of capabilities, memory regions, and register contents (PCC and CGP equivalents) that are safe to share. This mirrors the assumption in Theorem J.1 that PCC/CGP must be safe to share for cross-compartment execution.
-
Invariant Maintenance: The system must prove, at runtime or compile time, that the state passing through a module does not violate any global invariants (e.g., ensuring a retrieved capability pointer remains within its designated memory region).
Improved AI Capability:
The resulting system can execute complex reasoning tasks (e.g., scientific simulation, financial modeling) with guaranteed compositional safety. If any intermediate step fails or violates a contract, the system does not crash unpredictably; instead, it enters a defined safe state and provides a formal proof of why the computation failed relative to its initial preconditions. This is crucial for high-stakes applications where failure modes must be exhaustively understood.
Abstract
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.