PanSigna: the architecture of a Typed Policy Reactor Monitor-Compiler — a capability-secured reference monitor that compiles typed, default-deny policies down a multi-level IR to CHERI, seL4, WASM, and inline enforcement targets.

Architecture dossier · v0 · 2026-07-08
for review by the CHERI Alliance & seL4 Foundation

PanSigna

A Typed Policy Reactor Monitor-Compiler

One reference monitor for a whole machine — where authority is a typed, default-deny policy that is not interpreted at each call but compiled, once, down a multi-level IR into whatever can enforce it fastest: a CHERI capability, an seL4 kernel object, a WASM import table, or a residual inline guard. The decision is proved equal to the policy; the enforcement runs at the speed of the silicon.

The one door — complete mediation invoke(cap, method, path, body, grant) → identity · policy · resolve · transport · audit // grant = None ⇒ deny
Provably securecomplete mediation · default-deny · ocap
Performantcompile, don't interpret
Governablepolicy bound to types · inherited
Interoperableone IR · four backends
§1

The name is the specification

Five words, each a load-bearing claim. Read together they describe the whole machine: typed authority, expressed as policy, driven by a reactor, mediated by a monitor, delivered by a compiler.

Typed
rides the type spine

Every subject and object is a typed thing. Policy binds to a type, not an instance, via a governs edge — authored once, inherited by every member down the subTypeOf DAG.

Policy
author the allow, never the deny

Deny is the floor, not a rule you write. Authority is a positive allow-policy — a content-addressed blob of verifiable bytecode. Composition is kernel-fixed deny-overrides; a broken policy fails closed.

Reactor
events are the source of truth

State is a durable append-only log of posts (CQRS). Reactions — themselves things — project the log into the typed store and recompile affected policy. Nothing mutates in place; everything is a reaction to an event.

Monitor
one door, complete mediation

The store is reachable only through invoke. Every edge — API, VFS, bus, runner — is a pure client with zero direct authority. A compile-time guard fails the build if a perimeter module reaches the core.

Compiler
lower policy to the metal

The novel core. A policy is lowered — like an SSA IR through a backend — from an abstract typed dialect to the strongest enforcement primitive each target offers, then proved equivalent to its source.

§2

The proof surface

Security is not a feeling; it is a set of named guarantees, each with a mechanism, a citation, and an honest status — what is machine-proved, what is designed-for, what is assumed of a dependency. Nothing here is claimed proved that isn't.

GuaranteeMechanismRests onStatus
Complete mediation Store reachable only via invoke; perimeter has no store/exec/bus handle; build.rs denies at compile time. Lampson '74 design-enforced
Fail-safe defaults Base on permission: default allow = false. No allow matches ⇒ denied. No ambient authority — owner is a token, not a branch. Saltzer & Schroeder '75 design-enforced
Attenuation is a ceiling Grants are attenuable ocap tokens; a delegate can only narrow, never widen. Offline-verifiable (Ed25519 + caveats). Miller '06 · Biscuit dep-assured
Policy semantics are sound Authorizer & validator proved in Lean (default-deny, deny-overrides, order-independent) — of the model; the Rust engine is differential-tested against it. PanSigna mandates schema-validated policies so Cedar's skip-on-error can't drop a forbid. Cedar / Lean (cedar-spec) model-proved
Compiler preserves meaning Each lowering emits a witness; a validator checks compiled enforcement ≡ source policy per artifact (translation validation), plus differential fuzzing. Pnueli '98 · Alive2 design-target
Spatial + referential safety Capability bounds & permissions enforced in hardware; unforgeable, monotonic, tagged. CHERI · Morello hw-enforced
Isolation of the TCB Enforcement primitives distributed as kernel capabilities on a formally verified microkernel. seL4 (Klein '09) kernel-proved
Integrity of policy artifacts Policies are sha256-addressed blobs; the hash is the integrity check. Compile-per-hash, cache is correctness-free. Venti · Nix · git design-enforced
§3

Compile, don't interpret

Every policy engine in production pays a tax on the hot path: it interprets a rule set on each request. PanSigna's thesis is that a reference monitor is a compiler target — the policy is fixed long before the call, so the decision can be lowered ahead of time into a primitive the substrate enforces for free.

The interpreted monitor — everyone else Decision cost paid per call

Request arrives → marshal context → evaluate rule tree in a policy VM → return allow/deny. Predictable overhead on every access; the engine is on the critical path forever, and its correctness is re-litigated at runtime.

The compiled monitor — PanSigna Decision cost paid once, at compile

Policy compiled per sha256 into a CHERI capability set / seL4 CNode / WASM import table. At call time the substrate is the check — a bounds test in silicon, a cap lookup in the kernel. Zero policy-VM on the hot path.

Where the performance lives

Ahead-of-time lowering. The residual — what genuinely can't be pushed into hardware or kernel — is the only thing evaluated at runtime, and it is emitted as a monomorphized guard, not a rule walk.

Content-addressed compilation. Identical policy compiles once; the artifact caches by hash with no invalidation problem, because immutable blobs make caching correctness-free.

The MLIR discipline, everywhere

Design lives in the IR, not the language. Concrete syntax — Rust, C, Nix — is interface only, chosen for pragmatism and never at the cost of performance: monomorphized generics over dynamic dispatch on hot paths, bulk operations over per-item allocation.

The compiler is structured as progressive lowering through dialects — Lattner's "one IR, many backends," applied to authority instead of arithmetic.

§4

The lowering pipeline

The heart of the machine, read top-to-bottom exactly as it compiles. A typed policy descends through three dialects and two passes, then fans out to the four enforcement targets — each receiving the strongest primitive it can offer — and every emission is checked against its source.

Dialect L2
Policy · high
Typed Policy Dialect
What a human authors and a proof tool reads: allow-rules over entity types, bound by governs edges, in a language with mechanized semantics.
// author the allow, by type — inherited by every instance permit(principal is Agent, action == invoke, resource is Content) when { resource.trust >= principal.clearance && grant.scope.covers(resource) };
↓pass — resolve & inherit: bind each rule to its type; expand down the subTypeOf DAG; normalize to canonical allow-set
Dialect L1
Authorization IR · mid
Authorization IR  — SSA, deny-overrides
Target-independent, fully typed, single-assignment. Deny is explicit as the meet; the artifact is now a pure decision function ready to specialize.
%r0 = allow guard=[trust≥clr, scope⊇res] ; from L2 %d = deny ⊤ ; the floor %out= meet(%d, %r0) ; deny-overrides
↓pass — partial-evaluate & assign: specialize against the thing-graph & available substrate; route each residual to the strongest target that can hold it
Dialect L0
Target ISA · low
CHERI
hardware-enforced

Spatial rules become capability bounds + permissions — unforgeable, checked every access by the ISA.

→ sealed cap, perms mask
seL4
kernel-enforced

Structural authority becomes a CNode / capDL distribution — policy-as-kernel-objects, model-verified.

→ cap slots · capDL '10
WASM
sandbox-enforced

Custom ops run in a sandbox; the compiled import table is the grant — absent import, absent authority.

→ component imports
Inline
software residual

Whatever can't be pushed lower: a monomorphized guard compiled into the invoke path. The honest fallback.

→ predicate · IRM '04
⊨ Translation validation. check( ⟦L0 emission⟧ ≡ ⟦L2 source⟧ ) per artifact — every lowering carries a witness the validator confirms, so a miscompiled policy is caught before it is ever installed. Backed by differential fuzzing across the four targets.

What is actually new here

Not "compiling policy." Each level is proven prior art: inlined reference monitors (Erlingsson & Schneider '04) for the residual, OPA's compile-to-WASM as industrial precedent, eBPF LSM/KRSI for kernel-compiled policy, seL4 capDL for policy-as-kernel-objects, and Micro-Policies/PUMP ('15) for hardware tag enforcement adjacent to CHERI.

The contribution is preserving one typed, default-deny, deny-overrides semantics across all four heterogeneous targets at once — and proving each lowering equal to that single source. Standing on named shoulders; the new step is the join.

§5

Dependency choices

Every load-bearing part is a deliberate pick over a named alternative, weighted for provability first, then performance, then ecosystem fit. Each carries its honest trade and a lane: production reality today, or research we advance.

CategoryPolicy front-end & semantics
Cedar
over OPA/Rego
The only widely-used policy language with a mechanized (Lean) semantics and a verification-guided Rust implementation — decisive for a provability-first monitor. Typed schemas and entity types map directly onto the type spine. production
Trade Cedar's model is authorization, not arbitrary Datalog — we adopt its discipline and lose Rego's anything-goes flexibility, which for a monitor is a feature.
CategoryCompiler core & IR
Rust-native SSA IR
MLIR discipline, not melior
Progressive lowering through dialects is the proven shape for "one source, many backends" — but PanSigna's value is custom dialects with verified rewrites, exactly what melior can't express (new dialects still need C++ TableGen behind an alpha C API). So we take MLIR's method and build the IR in Rust (pliron-class base), keeping MLIR-compatible textual syntax. research
Trade we forfeit MLIR's mature pass manager and upstream lowerings, and take on a pre-1.0 IR core to own — bought back as a cargo-only build (clean flake, plausibly self-hostable on CHERI-seL4) and a Lean semantics that binds to the SSA calculus, not a C++ artifact. Precedent: NVIDIA's cuda-oxide (2026), lean-mlir.
CategoryGrants & capability tokens
Biscuit
Eclipse · v3.3 · over macaroons
Attenuation as a first-class ceiling (appended blocks only add checks), offline Ed25519 chain verification, and Datalog caveats that express as policy — a near-exact fit for Miller-style ocap grants. Macaroons lack offline public-key verification; zcap-ld has no Rust. production
Trade Biscuit's Datalog is a second policy language: the monitor must maintain a verified compilation from the typed IR into token checks or granted authority drifts — and verifying tokens pulls a Datalog evaluator into the TCB. UCAN 1.0 kept on watch as a convergence target.
CategoryEnforcement substrates
CHERI · seL4
the two proved floors
Hardware referential safety and a formally verified kernel are the two strongest enforcement primitives in existence — and the reason this project belongs to this audience. Policy lowers into them. production
Trade CHERI×hypervisor semantics are still draft (v1.0 excludes the hyp chapter) — an area PanSigna's substrate work feeds back into the spec.
Wasmtime
for custom ops
The default runner for agent-authored code: content-addressed, portable, sandboxed. Solid on aarch64-darwin and riscv64-linux today. production off-CHERI · research on purecap
Trade a WASM runtime on CHERI-purecap is research-grade, not production — presented honestly as a forward lane, not a shipped claim.
CategoryEvent log & substrate
NATS JetStream
CNCF · async-nats
The durable, replayable post log that is the CQRS source of truth; the reactor projects it into the typed store. We cite the Dec 2025 Jepsen 2.12.1 analysis openly and pin its lessons: sync_interval: always on the source-of-truth stream, R=3, server ≥2.14.x. production
Trade durability-always costs write latency and a running broker is infrastructure — bought back as an auditable, rebuildable store that is a pure projection of an append-only log. With this audience, citing the adversarial result and engineering around it beats omitting it.
Nix
the reproducibility spine
Every artifact — toolchain, policy blob, substrate image — is content-addressed and reproducible. The build graph is the supply-chain proof the Alliance already values. production
Trade a learning curve for contributors, repaid in bit-for-bit reproducibility and a hermetic CI story.
§6

The repository, as governed structure

The layout enacts the reference monitor: a small trusted core that alone touches authority, a ring of perimeter edges that are pure invoke clients, and a compile-time guard that fails the build if the ring ever reaches past it. You can read the security property off the directory tree.

pansigna/ ├─ flake.nix # the reproducibility spine — one command ├─ build.rs # DEFAULT-DENY GUARD · perimeter→core = build fail │ ├─ core/ # ── the TCB · only code with authority ── │ ├─ invoke.rs # THE ONE DOOR: id·policy·resolve·transport·audit │ ├─ monitor.rs # reference monitor · complete mediation │ ├─ store/ # things · edges · content(sha256) · posts │ └─ grant/ # mint · verify (Biscuit) · attenuate=ceiling │ ├─ compiler/ # ── the Monitor-Compiler ── │ ├─ dialect/ │ │ ├─ policy_l2.rs # typed policy dialect (Cedar-grounded) │ │ ├─ authz_l1.rs # SSA authorization IR · deny-overrides │ │ └─ target_l0.rs # per-substrate primitives │ ├─ passes/ # resolve·inherit · partial-eval · assign │ ├─ lower/ # cheri · sel4 · wasm · inline backends │ └─ verify/ # translation validation · differential fuzz │ ├─ reactor/ # reactions · projector(posts→things) · recompile │ ├─ perimeter/ # ── edges · pure invoke clients · NO authority ── │ ├─ api/ vfs/ mcp/ run/ # each a thin shim over the door │ ├─ proofs/ # Lean semantics · IR↔policy equivalence lemmas └─ policies/ # content-addressed allow-policy blobs, by type
Core — the TCB. The only modules that hold a store, exec, or bus handle. Kept small on purpose: the smaller the trusted base, the smaller the surface to prove.
Compiler & spine. The lowering pipeline, the reactor, the Nix flake — the machinery that turns typed policy into enforced authority, reproducibly.
Perimeter — the edges. API, filesystem projection, MCP, op-runners. Every one is a client of invoke and nothing more; they can request authority, never hold it.
The guard. build.rs statically forbids any perimeter module from importing core authority. Violating the reference-monitor property is a compile error, not a code-review note.
§7

Honest ledger

What is real, what is designed, what is research — stated plainly, because this audience can tell the difference and respects the distinction.

◉ Rests on proved ground
  • seL4 functional correctness (Klein et al.)
  • CHERI hardware capability safety
  • Cedar's Lean-mechanized authorizer
  • Content-addressing integrity (Nix/git)
◒ Designed, to be built & shown
  • The L2→L1→L0 lowering pipeline
  • Translation validation per artifact
  • The build.rs default-deny guard
  • Reactor projection + recompile loop
○ Research lane, named as such
  • WASM runtime on CHERI-purecap
  • CHERI×hypervisor policy semantics
  • Real-MLIR vs native-IR decision
  • End-to-end proof chain composition

Provenance. Every dependency claim here was source-verified against upstream repositories and papers on 2026-07-08 (Cedar's Lean theorems in cedar-spec; Biscuit v3.3 / Eclipse; wasmtime riscv64 Tier 3 & the absent purecap path; NATS 2.14.x + the Dec 2025 Jepsen analysis; the six prior-art shoulders). Where a claim softened — Cedar's proofs cover the model not the crate; melior can't hold custom dialects; WASM-on-CHERI is research-only — it is marked here, not dropped. This is an architecture proposal for discussion: its purpose is to be refuted or ratified by the people who built the ground it stands on.