Skip to content
JouleOS Docs

Capability ledger

JouleOS gates every privileged operation through a capability ledger. The defining property is not policy — it is construction: a Capability<T> can only be produced by the kernel’s Ledger::issue. There is no public constructor. A forged capability is unrepresentable in the type system, not merely rejected at runtime.

Eight typed classes

Section titled “Eight typed classes”

Every gated I/O path maps to exactly one class:

Storage · NetworkSend · Inference · SensorAcquire · ActuatorIssue · MemoryRecall · DisplayOutput · CodeGen

A subsystem that wants to touch the network must hold a Capability<NetworkSend>; nothing else will type-check.

Delegation and revocation

Section titled “Delegation and revocation”
  • Intersection delegation — a delegated capability can only narrow. You cannot hand out more than you hold.
  • Constructive revocation — a generation flag invalidates a capability and everything derived from it, atomically.

The TCB boundary is the proof

Section titled “The TCB boundary is the proof”

The kernel trusted computing base is no_std. The JIT (Cranelift) lives outside the TCB and literally cannot link into it — the dependency graph forbids it. So the strongest claim about the kernel isn’t a promise to audit; it’s a fact about what can compile.

The proof is structural. The policy is downstream of it.

These invariants (I1–I20 in THEOREM v0.2) are enforced in the conformance suite. The same object-capability discipline is realized over the wire by the sibling standard JCP.