Themis is a bare-metal capability hypervisor for x86_64 and AArch64 (in progress). It enforces capability-based composable isolation at the hardware level: memory regions, CPUs, and I/O are first-class capabilities handed out to guest domains. No domain — including dom0 — has special privileges.
L2 Nested Guest (Linux VM) ← managed by cloud-hypervisor
L1 Dom0 (Ubuntu + thhv.ko) ← first domain, NOT privileged
L0 Capavisor (Themis) ← bare-metal, capability-enforced
Hardware (x86-64 VT-x/VT-d)
For the full architecture, design axioms, and invariants see
CONTEXT.md.
This is a ground-up reimplementation of Tyche, rebuilt with modern Rust tooling and AI-assisted development. Key differences from the original:
- Full heap inside the capavisor —
Vec,Arc,BTreeMapwork natively - No KVM compatibility — own kernel driver (
thhv), freed from KVM constraints - Formal verification — executable Lean 4 model with 83 proved safety theorems
- Multi-ISA — platform-agnostic engine, AArch64 porting underway instead of the original RISC-V
| Directory | Description | README |
|---|---|---|
capa-engine/ |
Capability engine — platform-agnostic no_std Rust library |
README |
capa-cli/ |
Interactive CLI simulator with Rust & Lean backends | README |
lean-exec/ |
Executable Lean 4 model for differential testing & formal verification | README |
themis/ |
Capavisor (bare-metal hypervisor) + build scripts | README |
thhv/ |
Linux kernel module — dom0↔capavisor interface (/dev/thhv) |
README |
cloud-hypervisor/ |
Forked cloud-hypervisor with Themis VMM backend (submodule) | — |
docs/ |
Project-wide documentation | see below |
| Path | Contents |
|---|---|
docs/building.md |
Unified build guide — all components, first-time setup, day-to-day workflow |
docs/architecture/ |
Design documents: confidential VMs, address translation, interrupts, attestation, ARM porting, platform modularization |
docs/capability-engine/ |
Engine deep-dive: semantics, implementation details, CLI tutorials |
docs/domain-comm.md |
Domain communication protocol (thhv ↔ capavisor ABI) |
docs/archive/ |
Historical docs: old implementation plans, superseded semantics, session notes |
# Ubuntu/Debian
sudo apt install e2fsprogs fuse2fs qemu-utils cloud-image-utils xorriso
# Also: Rust nightly, make, gcccd themis
cargo setup-limine # one-time: Limine boot assets
cargo fetch-dom0 # one-time: Ubuntu Noble image
bash scripts/fetch-kheaders.sh # one-time: kernel headers for thhv.ko
bash scripts/create-bins.sh # one-time: create artifact disk
cargo build-bins # build capavisor + thhv + CHV (from repo root)
SEED=1 cargo themis # first boot (cloud-init provision)
cargo themis # subsequent bootsDom0 login: SSH ssh -p 2222 cloud@localhost (password: cloud123)
For the full build guide covering all components see docs/building.md.
Platform-agnostic no_std library that validates all resource operations before
any hardware change. Domain creation, memory carve/alias/send/revoke, VP
switching, channels — all mediated through capabilities.
cd capa-engine && cargo test # unit + integration tests
cd capa-engine && cargo loom # deterministic concurrency testsTwo independent implementations of the same spec: the Rust production engine and an executable Lean 4 model. Both consume the same CLI scripts and must produce identical output.
cd capa-cli
cargo build --release --features lean-backend
bash regression/run-diff.sh --with-tutos # run all differential testsSee capa-cli/README and lean-exec/README.
| Component | x86_64 | AArch64 |
|---|---|---|
| capa-engine (lib) | ✅ build + test | ✅ check |
| capavisor | ✅ build + run | ✅ QEMU boot (M6) |
| thhv.ko | ✅ build | — |
| cloud-hypervisor | ✅ build | — |
AArch64 boots Linux on QEMU (EL2, GICv3, Stage-2, PSCI). See docs/architecture/arm-porting.md.
CONTEXT.md— axioms, architecture, design decisions, hypercall ABIdocs/building.md— unified build guidedocs/architecture/— design documentsthemis/scripts/README.md— full script & variable referencetodo.md— implementation task tracker