VerifiedOS is a design and implementation in progress for an end-to-end formally verified computer. It combines an in-order CHERI-enabled RV64IMV-inspired system-on-chip with a seL4-inspired multikernel OS. The intended proof chain connects the abstract specification, source, binary and ISA to the modeled hardware.
Engineering effort is treated as free and trust as the scarce resource, so security comes ahead of performance and ahead of compatibility with existing hardware and software.
The first release targets a general-purpose laptop. The release scope defers the browser, handset and server ensemble. The design prefers open standards wherever its guarantees permit; the compute and graphics compatibility plan records the proposed OpenCL, SPIR-V and HIP surfaces and assesses Vulkan and Vulkan SC frontends over shared native execution.
The project plan records completed artifacts, remaining work, priorities and milestones.
Contents
✨ Design highlights
- Bespoke seL4-inspired multikernel
- Deterministic where a guarantee needs it, elastic where the desktop does
- Fixed-latency on-die memory with end-to-end ECC
- One die is one machine, and a server is several
- CHERI in place of the usual protection hardware
- Temporal safety and no uninitialized reads
- No speculative or out-of-order execution
- No simultaneous multithreading (SMT)
- Verified cores and qualified devices
- On-die OpenTitan-class root of trust
- The device holder owns the root
- The device builds its own software
- Memory planned before boot, with elastic pools for the desktop
🧱 Bug classes removed by construction
- RISC-V and microarchitectural omissions
- CHERI capability tags, bounds, and monotonicity
- CHERIoT-lineage compartments, sentries, and lifetime
- Static time partitioning
- Mon CHÉRI property, re-homed without a second tag plane
- CHERI-TAL and binary admission
- Verified OS, I/O, storage, and supply-chain construction
- Faults the machine detects rather than prevents
- Obligations discharged elsewhere
- The proof artifacts themselves
- What this inventory does not claim
⚖️ License
One minimal capability kernel runs per core; other services run in confined compartments. The kernel design takes seL4's endpoints and non-interference goal, with a static object graph and CHERI capabilities replacing its dynamic object machinery.
The fixed tier reserves time and memory for trusted services and deadlines. Desktop applications launch, close and share resources inside a fixed elastic-domain envelope; its contract defines dispatch, bounded yields and the isolation boundary.
On-die SRAM and denser gain-cell memory provide two fixed latency classes, with CHERI tags, ECC and revocation checks on both. The memory profile owns the placement and timing rules; bulk capacity depends on qualifying a physical part.
A machine occupies one die. A later server ensemble adds whole machines with separate memory and trust roots, connected by scheduled authenticated messages. Its contract states the scaling limits and qualification gates.
Pointers carry hardware-checked bounds and permissions. The ISA profile's exclusions record the resulting removal of address translation and parallel protection mechanisms.
CHERI-TAL admission adds lifetime and initialization checks to CHERI's spatial bounds. Revocation and reclamation prevent stale authority surviving reuse; zeroization prevents prior-tenant disclosure.
Cores issue in order with static-only prediction. The microarchitectural absence contract specifies how the missing speculative and history-dependent structures are audited.
Each core has one hardware thread. The absence contract also requires evidence that no second thread context exists.
Scalar, vector and matrix core classes share one ISA and capability model. Graphics, software inference and device control run on those cores. An optional immutable inference module has a separate device contract and remains qualification work.
The root of trust handles measured boot, key custody and attestation on a scalar CHERI core.
The holder controls the generation-signing root set, including removal of the vendor's key. That contract distinguishes generation admission from immutable firmware roots, production debug restrictions and the rollback floor.
A resident certifying toolchain lets the holder build and prove software locally. Its output follows the same admission rules as any producer's: native code enters a successor generation; Wasm app bundles run as interpreted data in the current session.
Fixed-tier storage is assigned before boot. Within its fixed envelope, the desktop uses runtime allocation from reserved pools, with verified chunk isolation and safe reuse. The pool contract owns exhaustion, fragmentation and quarantine costs. Ordinary apps share one pool; an app declared isolated, such as a credential manager, gets a domain, label and pool of its own.
This inventory describes the guarantees targeted by the full specified stack. Implementation and proofs remain incomplete. Each row labels how the design addresses a bug class. Native binary guarantees cover native apps and interpreter hosts. Interpreted guests have arena confinement and the stated guest-semantic limits; their linear memory does not inherit native object-level safety.
Four modes target prevention:
- 🕳️ Absent: the bug's enabling mechanism is deleted.
- 🛡️ Enforced: the CHERI hardware checks every access.
- ✋ Rejected: a mechanical check refuses the artifact before it installs or ships: CHERI-TAL admission for a binary, the proof gate for a proof artifact.
- ✅ Proved: the shipped artifact must carry a machine-checked theorem and pass the proof-artifact gates. The crown-jewel inventory records which specifications and theorems exist today.
Three modes describe detection or remaining obligations:
- 🔔 Detected: a fault within the detector's coverage is corrected or causes a fail-stop response.
- 🤝 Transferred: the named party must meet the obligation; naming that party does not discharge it.
- 🚩 Residual: the obligation remains open in the specification's residual-risks section.
| Potential bug or attack class | Construction | Mode |
|---|---|---|
| Transient-execution attacks, from Spectre and Meltdown to microarchitectural data sampling | No speculative execution, transient state, reorder buffer, or reservation stations exist | 🕳️ Absent |
| Cross-thread SMT leakage and sibling-thread state corruption | One hardware thread per core; there is no second thread context | 🕳️ Absent |
| Poisoning or aliasing of any dynamic predictor state | Prediction is static-only; BHT/PHT, BTB, and RAS state do not exist | 🕳️ Absent |
| Cache timing and cache-eviction side channels | Two fixed-speed memory classes replace caches, eliminating hit/miss and eviction timing. Composition fixes each address's memory class. Admitted secret-typed code rejects secret-dependent SRAM bank selection | 🕳️ Absent ✋ Rejected |
| Cache-coherence protocol and stale-cache bugs | With no cached copies there is no coherence protocol to get wrong and no stale line to serve | 🕳️ Absent |
| Address-translation and paging bugs | Virtual memory, the MMU, page tables, TLBs, walk caches, and the shootdown protocol are deleted | 🕳️ Absent |
| Privilege-ring confusion and S/U transition bugs | Machine mode is the only mode; privileged operations require an unforgeable CHERI permission on PCC | 🕳️ Absent 🛡️ Enforced |
| Configuration gaps and inconsistent views across parallel protection hardware | PMP, IOMMU, and IOPMP are deleted; one capability model governs CPU and DMA access | 🕳️ Absent |
| LR/SC livelock and spurious-failure retry loops | Zalrsc is excluded, and admitted code has no such retry loop |
🕳️ Absent ✋ Rejected |
| CAS retry and capability-sized ABA machinery | Zacas is excluded, so no compare-and-swap exists to retry or to hand a recycled value |
🕳️ Absent |
| Self-modifying-code and instruction-stream synchronization bugs | Runtime emission into executable memory, writable executable memory, fence.i, and writable-to-executable promotion are absent; same-session Wasm apps are interpreted data |
🕳️ Absent |
| DRAM read-disturbance bit flips on the fast class | An SRAM latch gives Rowhammer and RowPress no leaking capacitor or refresh cycle to disturb; SRAM's far weaker disturb modes are detected faults below | 🕳️ Absent |
| Read-disturbance on the bulk class | The capacitorless gain cell's disturb behaviour must be measured before qualification. Cell margin, ECC and fixed refresh address the measured faults; an uncorrectable event stops the machine. No access-reactive counter is used | 🔔 Detected 🚩 Residual |
| Reactive refresh machinery: activation counters, alerts, and back-off | The bulk class is topped up on a schedule fixed when the image is composed, so nothing counts accesses and nothing reacts to them | 🕳️ Absent |
| Memory-bus probing and DIMM or module interposition | On-die memory has no external memory bus, module, or die-to-die link to probe; an ensemble link joins two whole machines and carries scheduled frames, never a load or store, so it is not a memory bus either | 🕳️ Absent |
| Cold-boot remanence | Both memory classes and key storage need construction-specific power-loss qualification. Completed zeroization and authority discharge do not establish erasure after abrupt loss; the physical residuals remain explicit | 🚩 Residual |
| History-dependent prefetch channels | Prefetchers are absent | 🕳️ Absent |
| DVFS and reactive power-control channels | Frequency control and activity-driven control loops are absent | 🕳️ Absent |
| Refresh-timing channels | DRAM refresh and PRAC activity do not exist to observe | 🕳️ Absent |
| Interconnect and quality-of-service contention channels | The admission proof emits a static time-division fabric schedule; best-effort arbitration does not exist. The NoC model is unauthored, so this absence is structural, not yet proved | 🕳️ Absent 🚩 Residual |
| Contention between high-assurance memory islands | A high-assurance island takes a whole SRAM macro or tier and hosts one domain, sharing no path, arbiter, or revocation array with any peer; the unauthored-model residual above applies | 🕳️ Absent 🚩 Residual |
| Contention between low-sensitivity islands sharing an SRAM macro, or domains sharing an island | Static arbitration assigns island slots and, within a shared island, core sub-slots. Macro periphery, power delivery and thermal mass remain shared, as do bank ports and the atomic stage within an island. The unauthored-model residual above applies | 🚩 Residual |
| Variable latency on a secret operand | Every secret-reachable operation is fixed-latency (integer divide, the vector FPU including subnormals, atomics), and misaligned accesses trap rather than split | 🛡️ Enforced |
Variable-latency vfdiv/vfsqrt reached by a secret |
The one exception to fixed latency is flow-rejected: no admitted crypto kernel uses either instruction | ✋ Rejected |
| Secret-dependent address timing across SRAM banks | The flow discipline rejects a secret-labeled address, scalar or vector element, in admitted secret-typed code, and the non-work-conserving schedule confines the term to the issuing partition's own slot; no constant-time claim is made outside that code | ✋ Rejected |
The timing rows cover architectural timing. The crypto core's masked datapath addresses power and near-field electromagnetic leakage under a separate probing model; its limits appear in CHERI-TAL and binary admission.
The microarchitectural absence contract lists structures the audit must not find. The frozen ISA profile defines the architecture.
| Potential bug or attack class | Construction | Mode |
|---|---|---|
| Buffer overflows and out-of-bounds access, down to sub-object fields | Tagged capabilities enforce pointer bounds. The fixed-tier memory plan makes every narrowing exact; installation rejects bounds that would round. Desktop allocations use a composition-fixed size-class table that also permits exact narrowing | 🛡️ Enforced ✋ Rejected |
| Pointer and device-address forgery | Integers and raw bit patterns cannot create a valid tagged capability; authority must derive from an existing capability | 🛡️ Enforced |
| Pointer-provenance violations | Capability validity records derivation in hardware; the admitted ISA exposes no integer-to-capability escape | 🛡️ Enforced 🕳️ Absent |
| Permission escalation and confused derivation | Bounds and permissions only narrow; derivation cannot add authority | 🛡️ Enforced |
| Corruption reaching across any isolation boundary | Each object, compartment, and kernel partition is reachable only through bounded capabilities rooted in the static distribution | 🛡️ Enforced |
| Unsafe-language or compiler-emitted code bypassing spatial checks | Capability checks apply to emitted machine accesses regardless of source language | 🛡️ Enforced |
| DMA bypassing spatial or revocation checks | Device transfers carry explicit capability operands, checked like CPU accesses. Each fabric grant rechecks a live transfer window against the revocation bitmap. The fabric proof remains a recorded residual | 🛡️ Enforced 🚩 Residual |
| Writable-code injection and executable-data promotion | Store and execute cannot coexist in a capability's permission encoding. Only the measured-boot loader writes executable memory in either class, before any core is released. Runtime-written regions never become executable | 🕳️ Absent 🛡️ Enforced ✅ Proved |
| Corrupted pointers accidentally becoming live authority | A modified capability loses its validity tag or fails its bounds and permission checks | 🛡️ Enforced |
| Potential bug or attack class | Construction | Mode |
|---|---|---|
| Ambient authority and authority acquired by name | A compartment can name only capabilities in its manifest; no global namespace or ambient device access exists | 🕳️ Absent 🛡️ Enforced |
setuid-style privilege escalation |
There is no uid/gid identity to assume and no fork() to inherit it through; authority is only what the manifest delegates |
🕳️ Absent |
Path traversal and ../ escape |
A path is only an app-local alias for a manifest capability; no runtime mount/bind, global directory, or path-based capability lookup can reach outside the manifest |
🕳️ Absent |
| TOCTOU races through filename and link re-resolution | The capability is the object, and no symlink indirection exists, leaving no re-resolution window between check and use | 🕳️ Absent |
Shell injection and system()-style string-to-process execution |
There is no text shell, fork()/exec(), or PATH lookup to turn composed text into an action; run this command asks the service manager to start a capability-delegated compartment |
🕳️ Absent |
| Environment-variable injection | No environment block exists to inherit or poison | 🕳️ Absent |
| Argument injection between composed commands | The command interpreter pipes typed values between typed-signature commands, never byte streams for each stage to reparse | 🕳️ Absent |
| Dispatch hijack, handler registration to content sniffing | The handler/translator graph is finite, signed, and fixed at composition; no runtime act can add a handler or reroute a format to one | 🕳️ Absent |
| Malicious or compromised dependencies corrupting their caller or reaching unrelated resources | Attacker-facing and over-authorized libraries are separate least-authority compartments in the static graph | 🛡️ Enforced ✅ Proved |
| Escape from an embedded script engine into its host | The platform's Wasm interpreter must prove soundness and guest confinement against pinned semantics. Even an adversarial module can affect its host and peers only through declared imports and exports. Apps supplying another engine retain the obligation below | ✅ Proved 🤝 Transferred |
| Forged entry points and calls into the middle of a component | Sealed forward-edge sentries constrain entry to declared sites | 🛡️ Enforced |
| Forged or replayed return addresses | Sealed backward-edge sentries constrain return sites | 🛡️ Enforced |
| Unprivileged code accessing system registers or switch machinery | Access-system-register authority is a permission on PCC, held only by the kernel | 🛡️ Enforced |
| Stale capabilities surviving object reuse | Linear lifetime typing, revocation epochs, a budgeted sweep, quarantine, and the per-load filter over the loading island's own revocation array invalidate the old tenant before reuse; a device-held copy dies at its window's next fabric grant, and the desktop pool reuses a chunk only after the same sweep | 🛡️ Enforced ✋ Rejected ✅ Proved |
| Heap-allocator corruption, double allocation, and cross-app heap grooming on the desktop | The verified pool service provides disjoint, exactly bounded chunks, zeroed before handoff and swept for revocation before reuse. CHERI confines an app's heap damage to its own chunks. Pool capabilities cannot leave the domain | ✅ Proved 🛡️ Enforced |
| Runtime creation of unreviewed protection domains or authority edges | Compartments, imports, exports, shared windows, and schedule slots are fixed and checked at composition or package admission; launching a desktop app activates a context the composition already placed | 🕳️ Absent ✋ Rejected |
| Kernel memory exhaustion and allocation-failure paths | The kernel neither allocates after boot nor exposes an allocation primitive; the composition-time memory plan places every kernel object | 🕳️ Absent |
| Out-of-memory kills and cross-compartment memory pressure | Fixed-tier compartments exhaust only their own allotments; there is no shared kernel heap or reclaim policy. Desktop pool exhaustion follows a declared sequence within its domain, hibernating background apps and preserving the focused app. No global reserve, victim scan or kill daemon exists. Pressure between apps in one domain remains a residual | 🕳️ Absent 🚩 Residual |
| Permission-dialog spoofing and confused consent delegation | Only the trusted powerbox narrows and grants device authority. A root-of-trust latch assigns prompt rendering and touch input to the trusted-path agent and lights the hardware indicator. Apps and the compositor cannot draw, overlay or authorize the prompt | 🛡️ Enforced ✅ Proved |
| A declassification grant wider than the object it named | The non-interference theorem models a powerbox grant as a delimited release, CHERI-bounded to the object consent named, never a general high-to-low conduit. Whether the user named the right object is transferred below | ✅ Proved 🛡️ Enforced |
| A declassification an attacker can drive | Robust declassification quantifies over every compromised-component strategy: whether, what, and to whom the powerbox releases depends only on the unforgeable consent act and verified powerbox logic | ✅ Proved |
| An inter-level edge that outlives the act that created it | First-class revocation bounds the grant's lifetime, making an overlong edge a revocation failure rather than a policy exception | ✅ Proved 🛡️ Enforced |
A compartment receives a fixed-table slot or whole core at composition; no runtime action can enlarge that share. This bounds interference, not availability under fault, a separately recorded residual. Each desktop elastic domain is one such tenant: inside one, apps share its slots by a proved proportional share rather than by fixed slots, and the rows below say where that changes the claim.
| Potential bug or attack class | Construction | Mode |
|---|---|---|
| CPU starvation and scheduling denial of service by a hostile or runaway compartment | Each core runs a table-driven cyclic executive of fixed, time-triggered slots: no priorities, no run queue, and no runtime decision over the table. Inside a desktop elastic domain a runaway app receives only its proved proportional share and cannot touch another tenant's slot | 🕳️ Absent ✅ Proved |
| Priority inversion and priority-inheritance chains | There are no priorities to invert, so no inheritance chain can form; the desktop's dispatch uses weights and virtual deadlines rather than priorities, and no call blocks | 🕳️ Absent |
| Kernel lock contention | There is no shared mutable kernel data, no kernel locks, and no kernel threads; the kernel runs on the caller's budget | 🕳️ Absent |
| Interrupt storms and interrupt-driven preemption of an unrelated partition | Interrupt arrival is latched pending state read by ordinary loads in the owner's own slot; the slot-boundary timer is the machine's only asynchronous trap | 🕳️ Absent |
| Termination and progress channels between partitions | The frame is non-work-conserving across labels: a partition that idles, diverges, or faults burns its slot without moving any boundary, so peers observe the schedule, never its progress. A compartment can read its own slot width, and apps sharing a desktop elastic domain share a label and can observe one another's activity through their own timing and the pool; both are recorded residuals. An app declared isolated runs in a domain and label of its own, outside the others' view | 🕳️ Absent 🚩 Residual |
| A desktop app's time or memory spilling into the fixed tier or another tenant | Each elastic domain's envelope of slots, cores and pool is fixed at composition; no app's runtime choice moves another tenant's slot or byte, the boundary timer never cuts an app mid-reaction, and no capability derived from the pool can leave the domain | 🕳️ Absent 🛡️ Enforced |
| Slot overruns spilling into another partition's time | An interval-arithmetic admission proof fits every slot budget within the major frame, and overrun restarts the offender | 🕳️ Absent ✅ Proved |
| Forced revocation sweeps spilling into another partition's time | Grant churn sweeps only the granter's footprint, within fixed slots that cannot grow | 🕳️ Absent ✅ Proved |
| Cross-machine back-pressure, flow-control stalls, and contention over an ensemble link | The link's slot tables are an output of the admission artifact beside the fabric schedule: non-work-conserving, no arbitration, no retry, no flow control, so a peer can fill its own slots and never move this machine's frame; the unauthored isolation-model residual applies | 🕳️ Absent 🚩 Residual |
VerifiedOS adopts Mon CHÉRI's Write-before-Read guarantee without its runtime metadata plane: CHERI-TAL checks definite initialization statically, while eager zeroization prevents prior-tenant disclosure.
| Potential bug class | Construction | Mode |
|---|---|---|
| Reads of any uninitialized location, representation padding included | A load type-checks only where the slot's initialization attribute is set on every incoming control-flow path | ✋ Rejected |
| Disclosure of a prior tenant's data through unwritten memory | Allocation eagerly zeroizes the slot before it enters its new live range | 🕳️ Absent |
| Treating device-filled memory as initialized before DMA completion | The verified HAL consumes exclusive CPU ownership and returns initialized ownership only on completion | ✋ Rejected ✅ Proved |
| Partial or ambiguous initialization across an IPC boundary | Typed IDL messages and copy-once parsers write fixed destinations whole and carry initialization state explicitly | ✋ Rejected ✅ Proved |
| Potential bug class | Construction | Mode |
|---|---|---|
| Use-after-free and dangling pointers | Linear lifetime typing tracks every allocation through the typed binary, so no capability to freed memory survives to be dereferenced | ✋ Rejected |
| Double use or double free of linear authority | Linear and affine capabilities deny duplication, so an authority cannot be spent twice | ✋ Rejected |
| Data races across threads, compartments, or devices | Live writable authority excludes every overlapping alias; shared synchronization cells must have explicit atomic types | ✋ Rejected ✅ Proved |
| Type confusion and ABI mismatch | Type and ABI conformance are checked on the final binary | ✋ Rejected |
| Malformed control flow and calls to undeclared callees | Both halves of CFI and the manifest callee set are checked on the final binary | ✋ Rejected |
| Implicit integer wrap | An unannotated operation cannot silently trap, because no exception or unwinding path exists, and cannot silently wrap: modular and saturating arithmetic survive only as explicitly named operations | ✋ Rejected |
| Overflow or underflow over static bounds | Range side conditions ride on the arithmetic rules: the on-device checker decides them over closed numerals, and a bound that depends on a runtime value enters as a declared premise the checker reads as given and a release-time proof term discharges | ✋ Rejected ✅ Proved |
| Overflow in code admitted at Tier 2 | Tier 2 scopes the range obligation out, a recorded residual; in-range but wrong remains functional correctness at every tier | 🚩 Residual |
| Silently dropped security-bearing verdicts | Relevance typing denies weakening an integrity, freshness, admission, or transaction verdict, so a binary cannot eliminate one without examining it | ✋ Rejected ✅ Proved |
| A wrong response to an examined verdict | The grade bounds the drop, never the response: proceeding after an examined failure remains functional correctness, a recorded residual | 🚩 Residual |
| Ambient mutable state escaping the authority graph | The image is inspected for hidden mutable state (globals, lazy statics, thread-locals, singletons) and capabilities outside its declared initial set | ✋ Rejected |
| Secret-dependent timing in admitted code | The constant-time type discipline rejects secret taint at branches, addresses, and variable-latency operations; unstructured residuals carry a relational proof over the leakage model | ✋ Rejected ✅ Proved |
| Nonce and initialization-vector reuse | A linear nonce is consumed by sealing and cannot be duplicated, stored, or reached twice, even across a restored checkpoint or a re-derived key | ✋ Rejected |
| Secret residue in scalar registers and compiler-introduced spill slots | A must-erase grade, checked on the final binary, lets no secret-typed value or spilled copy of one be dropped by anything but an erasing operation | ✋ Rejected |
| Power and near-field electromagnetic analysis of the crypto core | The secret-handling datapath is masked, and its d-probing and composition theorems are verified on the artifact against a stated probing model; the model is an axiom about the silicon, its faithfulness the recorded residual | ✅ Proved 🚩 Residual |
| Secret residue in the frames of a compartment that returns | Restart erases the compartment's whole footprint before any reuse | 🕳️ Absent |
| Secret-dependent traps and the restart they cause | Constant-time typing makes trap choice a function of public inputs, and restart consumes only the offender's slots | ✋ Rejected 🕳️ Absent |
| A crash record disclosing more than its labeled fault class | The sentinel receives only a fault label from a closed enumeration. Proving that the record reveals no more than that class remains open | 🕳️ Absent 🚩 Residual |
| Unit, dimension, and clock-domain confusion in quantity arithmetic | Quantities carry a phantom dimension decided by type equality and erased before code generation, so cycles cannot stand in for microseconds or bytes for elements | ✋ Rejected |
| Unbounded or slot-overrunning execution | Syntax-directed WCET costs and loop-bound proofs must fit the static cyclic-executive slot; a desktop app instead proves a bounded interval between compiler-inserted yield points, which needs no loop bound | ✋ Rejected ✅ Proved |
| Stack exhaustion and unbounded recursion | The enumerated callee set proves call-graph acyclicity and recursion depth, so worst-case stack use is static; unbounded depth is refused | ✋ Rejected |
| Stack-clash writes into adjacent objects | A bounds-checked stack capability makes overrun fault rather than reach a neighboring object, with no guard page to bypass | 🛡️ Enforced |
| Compiler-created memory-safety regressions | Safety is checked from the final machine code and its derivation; compiler pedigree is not an admission input | ✋ Rejected |
| Compiler or build-farm output that does not implement its included source | Every package carries its exact content-addressed source closure and a theorem from that closure through assembly, linking, and the final image, which the proof kernel checks on the device at install beside the type check | ✋ Rejected ✅ Proved |
| Potential bug, fault, or attack class | Construction | Mode |
|---|---|---|
| Parser bugs, from unchecked lengths to recursive-input exhaustion | Every attacker-facing format uses a schema-bounded, non-recursive, verified Narcissus parser | 🕳️ Absent ✅ Proved |
| Representation-padding leaks in encoded output | Copy-once serialization emits only bytes the schema defines, so no stale padding reaches the wire | ✅ Proved |
| Non-canonical encodings parting byte identity from value identity | Every descriptor used for signing, hashing, addressing, or equality carries a machine-checked canonicity theorem: decode is injective, and re-encoding a decoded input reproduces its bytes; without the theorem, a format cannot serve an identity role | ✅ Proved ✋ Rejected |
Query injection, the SQL-shaped class |
A query supplies a namespace capability and a typed bounded predicate, never command text; even a maximally permissive predicate returns only capabilities derivable from the one supplied | 🕳️ Absent 🛡️ Enforced |
| Configuration injection and text-configuration parsing divergence | Trusted components parse no runtime text configuration; each generation compiles configuration to typed signed objects | 🕳️ Absent |
| Authority smuggling through IPC payloads | Ring payloads cannot store capabilities, on the die or across an ensemble link; they carry only indices into a pre-delegated per-session table, an ensemble-link frame naming the receiving machine's table and nothing on the sending one | 🛡️ Enforced ✅ Proved |
| Ring protocol violations, publication race to peer mutation | One canonical bounded SPSC ring library, linear ownership transfer, explicit atomics, and Ztso fences define the only transitions |
✋ Rejected ✅ Proved |
| DMA time-of-check/time-of-use races over a live buffer | Submission consumes the CPU's exclusive capability and returns it only after device completion | ✋ Rejected ✅ Proved |
| Deadlock and livelock in shared filesystem operations | RefFS-style linearizability and MoLi definite-release proofs are prerequisites to temporal admission | ✅ Proved |
| Torn writes and inconsistent crash recovery | The log and filesystem carry crash-refinement proofs | ✅ Proved |
| Process-resume state corruption | Recovery reconstructs from measured boot rather than resuming execution state, so no saved execution image exists to corrupt | 🕳️ Absent |
| Offline storage tampering and ciphertext substitution | Authenticate-then-return AEAD and the Merkle structure reject unauthenticated data before any byte is returned | 🛡️ Enforced ✅ Proved |
| Silent storage corruption and bit rot | Patrol reads scrub decay and read-disturb, rewriting pages approaching the correction limit; corruption that outruns the scrub fails authentication rather than returning silently | 🔔 Detected |
| Unauthorized rollback of system generations | Signed roots, monotonic counters, and an anti-rollback floor constrain which generation may boot | 🛡️ Enforced ✅ Proved |
| Replaying spent or revoked state through a restored backup | A backup carries only rollbackable typed regions, sealed under a key only the holder can reproduce; keys, credentials, grants and freshness-protected state never leave the device, so a restore re-derives authority and brings back no spent token, attempt counter or revoked grant. A backup sits outside the duress erase, a recorded residual | 🕳️ Absent 🚩 Residual |
| Reopening test, debug, or manufacturing access | A fixed acyclic lifecycle over one-way OTP fuses has no such transition: leaving test disables every debug and manufacturing interface at once, and nothing reopens them | 🕳️ Absent 🛡️ Enforced |
| RMA returning a production device to a debuggable state with its secrets intact | Production's one outgoing edge is an authenticated, terminal RMA transition, preceded by crypto-erase, with no return path | 🛡️ Enforced 🕳️ Absent |
| Engineering-key acceptance outside the factory | Lifecycle state enters the measured chain before ROM verifies any payload, making every transition attested, while state-diversified verification roots leave no engineering key acceptable in production | 🛡️ Enforced |
| Executable-loading and dynamic-linking bugs | There is no on-device ELF loader, dynamic linker, relocation pass, or executable-format parser; a small verified content-addressed image reader and capability-wiring table replace them | 🕳️ Absent ✅ Proved |
| Malicious or compromised supply-chain output bypassing platform safety | Admission re-checks the final artifact's types and proofs with no trust in its build pedigree, the correspondence theorem above ties it to its included source closure, and source-level malicious dependencies remain least-authority contained | ✋ Rejected ✅ Proved 🛡️ Enforced |
| Protocol downgrade and negotiation confusion | Each protocol has one composition-fixed configuration, ciphersuite, and version, with no capability-driven fallback; downgrade generations are absent from silicon | 🕳️ Absent |
| Ensemble-link interposition, peer substitution, or frame replay | Mutually attested peers use an authenticated encrypted session with identities and composition fixed at ensemble composition. Keys stay in the crypto core. Failed or mismatched attestation refuses the link; each machine runs its own generation. An unauthenticated or replayed session frame stops the link. The session model remains a residual | ✅ Proved 🚩 Residual |
| Link and radio state-machine flaws | A Lustre control plane refines a formal model of the standard's state machine, making unmodeled states, transitions, and timers unreachable | ✅ Proved |
| Model unfaithfulness and composed session security | Each reference model is curated from its protocol's machine-checked symbolic security analysis, so the machine the sequencer provably runs is the one whose session security that analysis checks; what remains recorded is the model's faithfulness to the prose standard, the primitives' symbolic abstraction, and the imported analyses standing as evidence outside the trust base | 🚩 Residual |
| Firmware bugs in auxiliary processors, baseband to management engine | Those programmable foreign computers are absent; fixed-function matter is driven by attested host software | 🕳️ Absent |
These faults can occur. The design detects, corrects or contains them within the stated coverage.
| Potential bug or fault class | Construction | Mode |
|---|---|---|
| Single-event and multi-cell upsets | Every array from the register file to main memory is ECC-corrected, and interleaving separates adjacent-cell strikes | 🔔 Detected |
| A bit flip forging or destroying capability authority | The validity-tag plane carries stronger DECTED (double-error-correct, triple-error-detect) correction, because a flipped tag changes authority rather than data | 🔔 Detected |
| Latent errors accumulating past the correction distance | Background scrubbing finds and repairs errors while they are still correctable | 🔔 Detected |
| An uncorrectable error | The access fails stop rather than returning a value | 🔔 Detected |
| SRAM disturb and half-select upsets | The same end-to-end ECC corrects these operationally induced flips, the far weaker analogs of the deleted DRAM disturbance classes | 🔔 Detected |
| A dead or degraded noise source weakening the one entropy root | Independent sources spanning at least two physical mechanisms are health-tested at startup and continuously after; failure is fail-stop, never a degraded draw. A failure the tests miss remains a recorded residual | 🔔 Detected 🚩 Residual |
| Physical fault injection, glitching to laser to EM | Supply, clock, timing-margin and light sensors trigger fail-stop on excursions. ECC corrects stored-state faults; tag and bounds checks trap capability corruption; the multikernel confines live-kernel faults for restart; watchdogs handle wedged cores. Undetected datapath corruption remains a residual | 🔔 Detected 🚩 Residual |
| A fault the layered detectors miss | Coverage beyond the stated single-fault model is evidence rather than theorem, and consumer-grade transient datapath strikes are unclaimed; both are recorded residuals | 🚩 Residual |
| Skipped critical instructions under an injected fault | The certifying compiler maintains control-flow signatures over boot verification, credential comparison, and lifecycle transitions; acceptance requires a comparison-derived token that fall-through or truncation cannot produce, and its absence under every fault in the protected-sequence single-fault model is a theorem | 🔔 Detected ✅ Proved |
| A fault-corrupted detector that cannot report itself | The sentinel is a detection-only lockstepped pair whose divergence latches fail-stop to the root of trust, with no third replicated core and no voting | 🔔 Detected |
| A partition alive but wedged, or a runaway holding its core | Watchdogs occupy failure domains disjoint from the cores, clock tree, and scheduler: the sentinel monitor restarts, revokes, or rolls back first, and the root of trust's always-on timer on an independent slow clock is the last resort. Only its reset responds within a slot, a recorded limit | 🔔 Detected 🚩 Residual |
| Reset loops hardening into permanent denial of service | Boot counting breaks a reset loop into minimal recovery, bounding downtime rather than permitting it | 🔔 Detected |
| An uncorrectable ensemble-link session frame | Fixed-latency forward error correction corrects what it is built for at a constant cost, and a frame whose authentication tag then fails stops the link rather than delivering a guess; the machine keeps running and the link is re-established at a scheduled instant | 🔔 Detected |
Each row names who must meet an obligation outside the platform.
| Class the platform does not close | Where the obligation goes, and what the platform still contributes | Mode |
|---|---|---|
| Injection into an app-supplied interpreter, including browser JavaScript | The compartment author. Apps using their own engine instead of the platform's verified Wasm interpreter must handle guest injection themselves. Browser JavaScript is also contained without a verification claim. In either case, manifest capabilities limit damage to the app's authority | 🤝 Transferred |
| Upset rates and component reliability beyond what the die's own correction covers | The deployment. The platform mandates correction at every point; the deployment selects the radiation-hardening grade, the one source-rate lever an enclosure cannot supply | 🤝 Transferred |
| The user granting the authority they meant to grant | The human. The attested, unspoofable powerbox makes the grant mechanism trustworthy and CHERI-bounded, but no proof can establish that the user named the right object; the abuse-resistance half of that ceiling is booked open | 🤝 Transferred 🚩 Residual |
Every Proved claim must pass the checks below. They guard against undeclared assumptions, vacuous theorems and specifications too weak to reject a bad implementation.
| Potential bug class | Construction | Mode |
|---|---|---|
| A shipped theorem resting on more than its declared assumptions | The proof term enumerates each theorem's axioms and assumptions for exact comparison with the requirements-register declaration; any extra or missing member fails the build | ✋ Rejected |
| A vacuous theorem: an impossible premise or an empty quantified domain | The build rejects quantified records without constructed witnesses and reports witnesses beside constants. Review must still establish that each witness satisfies the theorem's hypotheses. General vacuity is undecidable; the remaining obligation is a recorded residual | ✋ Rejected 🚩 Residual |
| A specification so weak that anything refines it | Every refinement and policy claim carries an instance its specification rejects. Review judges whether that instance meaningfully tests the specification; no build check decides this. That judgment remains a recorded residual | ✅ Proved 🚩 Residual |
This inventory does not claim to eliminate memory leaks, incorrect app intent, specification errors, cryptographic hardness failures, denial of service, social-engineering mistakes, analog or physical attacks, or every protocol flaw. Canonicity covers this platform's encodings. Agreement with an independent peer additionally requires that peer's grammar, interpretation, and implementation correspondence. A cooperating peer can supply artifacts for a bounded equivalence proof; without them, parser differentials remain untrusted evidence and a recorded residual.
The transferred rows count limits owned elsewhere. The specification's residual-risks section and critique.md record those limits and open proof work.
This inventory summarizes named archetypes; it is not the coverage claim, because such a list can never be complete. The register-computed coverage matrix, spanning every boundary and property, makes that claim.
The documentation index groups the companions by subject: languages, hardware, assurance, implementation, performance, and background.
Original documentation is CC BY 4.0; original code and proofs are Apache 2.0. The modified Sail model retains its BSD two-clause license. The licensing map owns path-specific terms and exceptions; THIRD-PARTY.md records upstream components.