Opportunity Map/CHERI ECOSYSTEM · A PUBLIC POLICY ONTOLOGY
CHERI enforces policy at the metal — and across the stack. One public ontology, from users to registers.
CHERI is one of the few substrates whose policy story runs continuously from the user's request down to the register set. Sealing and otype put authority into hardware; above the substrate, four ecosystem enforcers already retype the same authority at every height — cheriot-audit's Rego over compartment graphs, Cedar at tool-call interposition, eBPF in the kernel, XDP2 at the datapath.
The opportunity is a public policy ontology: one shared language of authority whose lowering emits into all four enforcers, so a policy written for a user surface reaches the register that carries it — losslessly, and only once.
◐ community proposalconfidence ~85%16 components surveyed2 unfilled ecosystem gaps
One ontology → users, kernel, datapath, silicon
The proposed artifact is a lowering compiler over a public policy ontology. One shared language of authority; the ecosystem's four existing enforcers as its targets.
01 — THE INVENTORY
Adopt · Borrow · Propose
Every component in the CHERI policy landscape falls in exactly one category. Does the ecosystem already ship it? Does academia already prove it? Or is it a coordination gap no vendor and no theorem has closed? The rule: adopt what enforces, borrow what theorizes, propose only what no one else covers.
🔩
ADOPT
enforcement — the ecosystem already ships this
CHERI sealing / otype 95%
The substrate already types authority. Every proposal on this page rests on it.
VeriCHERI monotonicity 90%
Tags clear, never set — mechanically proven. A free axiom the ecosystem shares.
Sail model + Verilator Ibex 90%
The maintained gold model. Any reimplementation is duplicated effort.
MLIR infrastructure 90%
The dialect substrate. Build a CHERI-policy dialect in it, not against it.
LLVM / CHERIoT toolchain 85%
The recommended CHERI microcontroller profile. The ecosystem's compiler is already here.
Rego / OPA + cheriot-audit 85%
Ships today. Operates on the compartment report directly. The build-time enforcer is solved.
Cedar engine 75%
The decidable runtime decision fragment. Reimplementing it recreates OPA badly.
📖
BORROW
semantics — read the theorems, don't reimplement them
Cerise / Cerisier 70%
The logical-relation methodology for what a capability contract guarantees. Read the shape; mechanize only when a barrier demands a machine-checked proof.
TAL / StkTokens 70%
The conceptual parent of typed low-level code. Read for why otype types authority, not data.
⚠ fragile category
BORROW silently expands into a quarter of Coq without discipline. A community tripwire: touch mechanized proof only when a customer or regulator demands one.
🔨
PROPOSE
the artifacts the ecosystem is missing
Typed-attachment primitive 90%
The irreducible base carrying TTL. No enforcer in the stack holds it — the ecosystem must define it.
Temporal / revocation enforcer 85%
CHERI is timeless; policy engines evaluate snapshots. Force-time has no home — a new component must own it.
Lowering compiler 90%
The compiler that emits XDP2, eBPF, otype-discipline, and Cedar decisions from one source. No prior art — the proposal itself.
Unified attachment dialect 90%
The MLIR dialect the lowering emits from — the ecosystem's shared source of policy meaning.
Cedar schema + interposition 80%THIN
Domain glue over an adopted engine. Weeks of integration, not quarters of engineering.
Append-only provenance 80%THIN
The linker already emits section hashes; the ledger over them is a small binding.
02 — THE VERTICAL
Not five tools. One column of proof.
Each layer proves a different claim about authority; none substitutes for another. The unification proposal is that a single dialect descends through all five heights, and each height enforces what its position allows — read top to bottom.
▼ AUTHORITY DESCENDS ▼
Semantics
Cerise universal contracts
What an attachment means and guarantees, phrased as a logical relation. Borrowed as the ecosystem's shared vocabulary.
BORROW → PROPOSE
│
Silicon
Sealing · otype · VeriCHERI
Authority enforced in hardware. Monotonic — authority only shrinks, tags clear and never set.
ADOPT
│
Build-time
Rego over the compartment graph
The static image is audited before deployment. The information barrier is proven here as a graph theorem.
ADOPT
│
Runtime
Cedar decision at the tool call
Per-call decisions at the interposition point. Decidable and analyzable — but stateless of time.
ADOPT
│
Provenance
SBOM hashes seal the ledger
Every section hash bound into an append-only record. Grounds the whole column in evidence.
PROPOSE · thin
one dialect threads all five heights
03 — WHERE THE ECOSYSTEM IS SILENT
Two gaps no vendor and no theorem covers
Everywhere else, an enforcer already ships or a proof already exists. In exactly these two places the market and the physics leave a gap — no procurement path, no citation, no fork of an existing tool closes them. This is where new work — by whoever the community entrusts with it — actually matters.
⚡ THE GAP · 01
Effect-force-time / TTL
Every enforcer in the stack is timeless or snapshot-stateless. CHERI carries no clock; Rego and Cedar evaluate frozen instants. TTL is the one field the ecosystem's policy vocabulary does not represent.
The seam is meaning that no substrate natively carries. It must be defined in the dialect layer, or the stack does not represent it at all.
⚡ THE GAP · 02
The unified lowering
The compiler that reads one annotated schema and emits XDP2, eBPF, otype-discipline, and Cedar decisions is what makes "one grammar of authority, four enforcers" concrete for the CHERI ecosystem.
Definitionally un-procurable — it is the encoding of the primitive itself. This is the artifact the ecosystem is missing, and the coordination opportunity this map exists to name.
04 — THE FORK, RESOLVED
Rego vs Cedar is not a fork — it's a division of phase
The tension in the ecosystem's policy conversation resolves cleanly. Two engines, two phases. Zero policy engines need be authored by anyone taking this proposal on — the lowering compiler emits to both, and each engine keeps operating in the phase it was designed for.
◐ BUILD-TIME
Rego over the compartment report
Least-privilege audit over the static graph. The information barrier is proven before anything ships — native to cheriot-audit, already shipping.
ADOPT · cheriot-audit
│ vs │
◐ RUNTIME
Cedar at the tool call
Per-call decisions at interposition. Only the schema and the glue are proposed; the engine is adopted as-is.
ADOPT engine · PROPOSE schema
Temporal logic belongs to neither — Cedar's entity model can't hold TTL, so it moves to the dialect layer by construction.
05 — THE LEDGER
Full component ledger
Every component in the CHERI policy landscape, its category, the layer it occupies, and the confidence behind the placement. Filter to isolate a category.
ComponentCategoryLayerRationaleConfidence
CHERI sealing / otype
ADOPT
Silicon
The substrate already types authority. Every proposal rests on it.
95%
VeriCHERI monotonicity
ADOPT
Silicon
Tags clear, never set — mechanically proven. A free ecosystem axiom.
90%
Sail model + Verilator Ibex
ADOPT
Emulation
Maintained gold model. Reimplementation is duplicated effort.
90%
MLIR infrastructure
ADOPT
Compiler
The dialect substrate. Build the CHERI-policy dialect in it.
90%
LLVM / CHERIoT toolchain
ADOPT
Compiler
The recommended CHERI MCU profile. The ecosystem's compiler is here.
85%
Rego / OPA + cheriot-audit
ADOPT
Build-time
Ships today; operates on the compartment report natively.
The logical-relation methodology. Mechanize only when a barrier proof is demanded.
70%
TAL / StkTokens
BORROW
Theory
Conceptual parent of typed low-level code. Read, don't port.
70%
Typed-attachment primitive
PROPOSE
Core
Irreducible base carrying TTL. No enforcer holds it — an ecosystem gap.
90%
Temporal / revocation enforcer
PROPOSE
Runtime
Nothing in the stack carries force-time — an ecosystem gap.
85%
Lowering compiler
PROPOSE
Compiler
One dialect → four ecosystem enforcers. No prior art — the coordination artifact.
90%
Unified attachment dialect
PROPOSE
Compiler
The MLIR dialect the lowering emits from — the shared source of meaning.
90%
Cedar schema + interposition
PROPOSE
Runtime · thin
Domain glue over an adopted engine. Weeks of work.
80%
Append-only provenance
PROPOSE
Provenance · thin
Ledger over the linker's existing section hashes.
80%
DESIGN NOTE
⬡ WHERE THE COORDINATION POINT ACTUALLY LIVES
The recurring temptation among capable CHERI implementers is to see the deep problem as more primitives in silicon — richer sealing, deeper capability types, a bespoke capability engine. Substrate work is the beautiful problem, and the leverage feels like it lives there. It does not.
The leverage lives in the compiler and the dialect above the substrate. The substrate is already shared. Every hour spent extending it further is an hour not spent on the lowering that unifies what the substrate already carries with what the four policy surfaces above it already decide. The discipline the ecosystem needs is refusal — decline the deeper substrate build precisely because the substrate is not where the coordination gap is.
Adopt the enforcement. Borrow the theorems. Propose the dialect.
OPEN QUESTIONS · TLDR
Open questions — risks · edges · calls for input
BORROW is the fragile category. "Borrow the Cerise methodology" silently expands into a quarter of Iris/Coq without discipline. Community tripwire: touch mechanized proof only when a customer or regulator demands a machine-checked barrier proof.
otype width vs dialect type-count. An adopted enforcer imposes a hard ceiling on the dialect above it. Whether virtualization closes the mismatch is an open design question.
Cedar and TTL. Cedar's entity model can't hold TTL. If temporal logic must live in the dialect regardless, Cedar's marginal value over the native Rego path narrows — a re-weighing worth doing in the open.
Sequencing of the two gaps. The unified lowering and the temporal enforcer are coupled — force-time is a field the compiler must lower. Neither proposal ships without a decision on the other.
TLDR
ADOPT — the ecosystem already ships CHERI, VeriCHERI, Sail, LLVM, MLIR-infra, Rego, and the Cedar engine.
BORROW — theorems from Cerise and TAL. Reading, not reimplementation.
PROPOSE — the missing artifacts: a typed-attachment primitive, a temporal enforcer, the unified dialect, the lowering compiler, and thin Cedar/provenance glue.
THE GAPS — TTL/force-time and the unified lowering. No vendor sells them; no theorem replaces them. The ecosystem's temptation is to extend the substrate; the leverage is to unify what the substrate and its enforcers already carry.