Structural, not advisory
Security model
The goal is not to make attacks difficult. It is to make the interesting ones unrepresentable, and to keep the set of things that must be correct small enough to prove.
Source of record: docs/threat-model.md in the Bivdi repository.
The one sentence#
A compromised or malicious component can only exercise the authority it was explicitly given.
Everything below is a consequence of that sentence, or an honest statement of where it stops.
The trusted computing base#
The trusted computing base is the minimum set whose failure breaks the model. Under the decided design it is:
- the CPU and its IOMMU;
- the measured boot chain up to and including the kernel;
- the kernel itself;
- the root supervisor;
- the root authority holding the seal and recovery key.
That is the complete list. The object store, every driver, the network stack, the compositor and every application sit outside it. A defect in any of them is a bug, not a breach of the model.
In a monolithic operating system, a bug in a graphics driver, a filesystem, or a network stack is a kernel-mode compromise. In Bivdi, each of those is an unprivileged, restartable component holding a narrow capability set. A compromised GPU driver is a graphics outage.
No ambient authority#
A process gains nothing from who launched it. There is no superuser to escalate to and no global namespace in which to name a resource you were not handed. A component that holds no network flow capability has no network access — and that is not a firewall rule that can be misconfigured, it is the absence of a name.
Authority flows strictly downward from a root supervisor and never upward. The kernel holds no policy: it answers "here is a capability, perform the operation it denotes", never "may this component do X".
Hardware boundaries#
- IOMMU required. Every device can DMA only into buffers it was explicitly given. Every DMA buffer must be registered before use, and registration requires holding a capability to that memory.
- IOMMU is necessary but not sufficient. Thunderclap (2019) showed IOMMU protection can be bypassed when DMA buffers share pages. Bivdi therefore uses per-buffer pages, strict rather than deferred IOTLB invalidation, and treats every device in one IOMMU group as a single security domain.
- Measured boot. Each boot stage measures the next into a TPM or measured-boot log, and storage is sealed to the measurement. A tampered system fails to unseal, so the data stays encrypted.
- Updates and tampering are distinguishable. A legitimate update re-seals to the new expected measurement through an authenticated path. A tamper does not.
- CHERI is optional acceleration for fine-grained in-address-space isolation, never a design requirement.
Not every hypervisor exposes a guest-visible IOMMU or a virtual TPM. Where the platform cannot provide them, the in-guest driver-isolation and sealing guarantees are weaker than on hardware that can — and the project treats that as something to state per platform rather than to average away. This applies to the parked microkernel track; on Linux today the boundary is enforced in the Runtime, not by hardware.
Adversaries and answers#
| Adversary | Assumed capability | The answer |
|---|---|---|
| Malicious application | Arbitrary code in its own isolation domain | Holds only manifest-granted capabilities; cannot name another component's resources |
| Compromised dependency | Arbitrary code inside an otherwise trusted component | Blast radius is that component's capability set; provenance records the code hash |
| Compromised driver | Arbitrary code with device access | Confined to its IOMMU domain and capability set; cannot reach kernel memory or another driver; restartable in milliseconds |
| Malicious peripheral | Bus-master DMA over USB or Thunderbolt | IOMMU with per-buffer pages and strict invalidation; no driver receives an identity-mapped window |
| Network attacker | Full control of the path | Encryption and mutual authentication by default; flow capabilities rather than raw sockets |
| Prompt injection | An agent tricked into misusing delegated authority | Narrow, attenuated, leased, quota-bound capabilities; content is data, not instructions; full provenance. Bounds the authority, never the agent's judgement — see what this does not prevent |
| Supply-chain attack | A backdoored package or update | Content-addressed reproducible builds; an authority-widening change appears as a readable diff |
| Privilege-escalation seeker | Syscall fuzzing, race exploitation | A small capability-based syscall surface; no name-based access, so no time-of-check-to-time-of-use-on-name class |
| Offline disk attacker | Physical possession of powered-off storage | Per-object encryption sealed to the boot measurement |
| Insider with a valid credential | A legitimate capability, misused | Attenuated tokens, short expiries, complete provenance, instant revocation |
| Ransomware | A component that can write, misusing it | No ambient write access; a versioned store makes rollback a pointer change |
| Lost device | Physical loss of a powered-off device | Encrypted at rest; root capability in hardware; recovery through identity |
Provenance: authority, never content#
An append-only, hash-chained log records every authority-relevant event: component instantiation with its manifest digest, every capability mint, copy, move and revoke with parent linkage, every token issuance and rejection, every object mutation with before and after hashes, every driver IOMMU-domain change, every update, and every boot with its measurement set.
It records authority, never content — no data, no keystrokes, no network payloads. That distinction is load-bearing: an audit log that captures content becomes the most valuable target on the machine.
A Merkle tree over each epoch is signed, so an attacker who fully compromises the machine still cannot rewrite history undetected. Deletion shows up as a gap; forking shows up as a root mismatch.
"What changed my machine, and what gave it the right to?" is a query, not a forensic investigation.
What is deliberately out of scope#
A threat model that claims everything protects nothing. For v1, these are explicitly not defended against:
- Malicious silicon and hardware backdoors. The CPU and IOMMU are trusted to implement their interfaces.
- Novel speculative-execution side channels. Known mitigations are deployed where the hardware allows. Resistance to the next Spectre-class variant is not claimed.
- Physical attack on a running machine — cold boot, bus probing, chip decapping, evil maid against a powered system.
- Traffic analysis. Bivdi hides what was communicated and by whom, not that communication occurred.
- Denial of service by an authorised holder. A component granted a CPU reservation may waste it.
- The user's own decisions. If a person grants broad authority through a legitimate gesture, Bivdi enforces it faithfully.
Where the model stops#
Revocation is forward-only by construction. Once a component has read bytes, it can retain them; no capability system has ever solved that and Bivdi does not claim to. What the model guarantees is that further access stops immediately, that a revocation takes the entire derived subtree with it, and that the original read is attributable.
Shared memory is the tractable half of the same problem, and it is revoked by unmapping. Data already copied out is not.
Revocation of copied-out data, schema evolution for persistent objects, large-data sharing without shared mutable memory, powerbox usability, and whether GPU acceleration and a small trusted core are compatible at all. These are recorded as open questions rather than quietly assumed to be solvable.
Assurance claims#
The project's rule for itself is "verification-oriented until the proof exists — never overclaim."
The leading proposal for the kernel, if the research track is reactivated, is seL4 — which carries machine-checked proofs, though the properties proven differ by architecture and none of them covers device address translation. The kernel choice is deferred indefinitely, and no verification claim applies to Bivdi's own components today.
Planned assurance work: model-checking the capability-derivation model for authority leakage before Milestone B exits, and a third-party audit of the capability model published in full — including unfixed findings — before the product ships. Audits of the Runtime are already run against execution rather than documentation, and their findings are recorded in the repository whether or not they have been fixed.