Bastion is an OS architecture for safeguarded AI where what an agent may do is expressed as a "capability signature". This is an Dijkstra monad whose commands are the only effects the agent can reach, with the indexed monad providing the modular reasoning principles required. This system requires a robust policy enforcer in the runtime system that sits inside the real application and dynamically prevents commands from running that the policy doesn't permit.
A long, long time ago I built something just like this in the Statecall Policy Language to let a programmer write a protocol automaton (e.g. for SSH or DNS) once and compile it to both Promela (so that SPIN could model-check safety properties expressed in LTL), and to OCaml as a safety monitor linked into the running application that raised an exception the moment the program deviates from its model.
The idea here is that a single spec that can be checked is used both for reasoning and also to embed in the real application code, so that the model and the code don't drift apart. The cost of carrying a monitor back then in an SSH server was a tiny ~2 of throughput, and it could be made negligible these days.
This project aims to apply that idea to modern day proof-oriented programming. We'll do the static reasoning in Leana 4 rather than Promela, and gthe a Dijkstra monad rather than LTL formulae. For the applications, we'll use OxCaml running inside Eio.
1 Specifications that can cross OS layers
The specifications we want to express aren't confined to just one library. Consider a policy over a pipeline of a filesystem, a JSON parser and a network socket:
the agent may read files below
/data; it may send to the network only values derived from thepublicsubtree of a parsed document; and no raw file bytes should ever cross the socket.
While multiple separate effect vocabularies are involved here, the property itself is a relation between them. Each layer contributes its own capability signature and its own specification monad; e.g. the filesystem's can borrow from an existing formal account of POSIX behaviour such as SibylFS, while the JSON parser is a pure relation between bytes and values.
The composite policy can be assembled from them via monad transformers (details TBD!). Working out what a realistic information flow property looks like here is the first chunk of the project.
1.1 Proof-producing extraction
While the specification is written in Lean 4, it should be a DSL that can compile it into multiple artefacts:
- proof obligations that can be discharged statically
- a residual automaton in OxCaml for obligations that must be dynamically checked
- a Lean proof that the second refines the first.
Every trace the automaton accepts should satisfy the predicate transformer, and every trace that violates it should be rejected.
Deciding where to cut between the static and dynamic halves will involve some difficult design choices, and so we'll ground this in a few practical interfaces such as a filesystem, a JSON parser, and a network interface.
2 Implementing the automaton in Eio
As a stretch goal, we'll embed this in OxCaml! OCaml 5 effect handlers are a much better interception point than anything that was available to me in 2005 in OCaml 3!
Each IO operation performed by an Eio fibre passes through a handler, so we could embed an automaton that can be ticked on each operation by the scheduler itself. OxCaml then earns its place on the fast path as it can be used to unbox and stack-allocate it so that a state transition is fast.
Another good stretch goal would be to hand the specification writing to an LLM. Agents are now plausible at producing mechanised Lean.
3 Prerequisites
Lean 4 and/or OCaml, or the appetite to learn both quickly. You will need interest in systems programming as well for the performance aspects.
4 Background Reading
- Modularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads, see the slides and Cyrus Omar's talk video, and why a sandbox that is just a shell wrapper isn't sufficient.
- Dijkstra monads for free, Ahman et al, POPL 2017, and Dijkstra monads for all, Maillard et al, ICFP 2019.
- Securing Verified IO Programs Against Unverified Code in Fstar, Andrici et al, POPL 2024.
- Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language and SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions for the historical work I did and Creating High-Performance, Statically Type-Safe Network Applications for the SSH/DNS server it was exercised on.
- Eio 1.0 – Effects-based IO for OCaml 5 and Effectively tackling the awkward squad for the Eio enforcement substrate, and An io_uring IO implementation for Lean for a sibling project that puts Lean underneath the IO stack.