tpt-hermes

The Universal WASM Driver Ecosystem — RFC 004

Write a hardware driver once in Rust, compile it to WebAssembly, and run it securely on any OS that implements the Hermes host runtime. Drivers are sandboxed by capability-based security and can be formally verified.

This repository covers Phase 1 (the foundation) and Phase 2 (driver catalog expansion + formal verification). Phase 1 delivered the core traits, the host runtime, the packaging format, the CLI, and a reference GPIO driver. Phase 2 adds UART / SPI / I2C / Ethernet reference drivers, GPIO drivers for additional RISC-V boards (SiFive HiFive, Allwinner D1), and the tpt-telos formal-verification pipeline with certificate embedding.

Repository layout

Crate / dir	Purpose
crates/tpt-hermes-driver	#![no_std] core traits (HermesDriver, Host, GpioDriver, …) and ABI constants.
crates/tpt-hermes-package	The .hermes package format (ZIP + manifest + verification cert).
crates/tpt-hermes-host	hermes-host: the tpt-archon / Linux host runtime (wasmtime + capability enforcement + real MMIO/DMA).
crates/tpt-hermes-cli	hermes: package / inspect / verify / completions tooling.
crates/tpt-hermes-telos	tpt-telos: formal-verification pipeline (static + Kani/Prusti backends) and certificate generation.
drivers/esp32-p4-gpio	Reference GPIO driver compiled to wasm32-unknown-unknown.

Quick start

1. Prerequisites

rustup toolchain install stable
rustup target add wasm32-unknown-unknown
cargo install --path crates/tpt-hermes-cli   # builds the `hermes` binary

2. Build the workspace

cargo build --workspace
cargo test  --workspace

3. Build and package the example driver

cd drivers/esp32-p4-gpio
cargo build --target wasm32-unknown-unknown --release
hermes package \
  target/wasm32-unknown-unknown/release/esp32_p4_gpio.wasm \
  --name esp32-p4-gpio --version 0.1.0 \
  --mmio 0x50000000:0x1000 --irq 32 --irq 33
cd ../..

This writes esp32-p4-gpio-0.1.0.hermes.

4. Inspect it

hermes inspect esp32-p4-gpio-0.1.0.hermes

5. Load it in the host runtime (tested)

The hermes-host integration test loads_real_esp32_gpio_driver loads the packaged WASM, enforces its capabilities, and confirms the driver reports a successful init. Run it with:

cargo test -p hermes-host loads_real_esp32_gpio_driver

6. Map real hardware (optional, Linux)

By default the runtime maps granted MMIO ranges into isolated heap buffers so tests run without privileges. To map actual device registers on a Linux host, swap in the /dev/mem backend:

use hermes_host::{HermesHostRuntime, DevMemMmioBackend};

let mut rt = HermesHostRuntime::new();
rt.set_mmio_backend(Box::new(DevMemMmioBackend));

The runtime also allocates real, OS-owned DMA buffers (anonymous mmap on Linux, heap otherwise) and releases every MMIO mapping on driver unload or runtime drop.

How capability enforcement works

1. A package's manifest.json declares the MMIO ranges, IRQs, and DMA budget it requests.
2. hermes-host parses these into normalized DriverCapabilities and rejects obviously invalid grants (zero-size MMIO, out-of-range IRQs, address overflow).
3. At load time each granted MMIO range is mapped into the driver's address space.
4. Every mmio_read / mmio_write / irq_register / dma_alloc call from the driver is checked against the granted capabilities before it proceeds — an out-of-range access traps instead of touching hardware.

This policy is enforced by the runtime, not by trusting the driver.

CLI reference

See crates/tpt-hermes-cli/docs/hermes.1 for the full man page, or run:

hermes --help
hermes completions bash   # shell completion scripts

Phase 2: driver catalog & verification

Reference drivers shipped

Driver crate	Board / class	Trait(s) implemented
drivers/esp32-p4-gpio	ESP32-P4	GpioDriver
drivers/esp32-p4-uart	ESP32-P4	UartDriver
drivers/esp32-p4-spi	ESP32-P4	SpiMasterDriver
drivers/esp32-p4-i2c	ESP32-P4	I2cMasterDriver
drivers/reference-ethernet-gmac	TBD hardware (GMAC)	EthernetDriver (DMA)
drivers/sifive-hifive-gpio	SiFive HiFive (JH7110)	GpioDriver
drivers/allwinner-d1-gpio	Allwinner D1	GpioDriver

The SiFive and Allwinner GPIO drivers are the portability proof: the exact same HermesDriver + GpioDriver logic runs on a second and third RISC-V SoC with only the MMIO base and register layout changed — no host-runtime changes. See cargo test -p hermes-host for loads_real_sifive_gpio_driver / loads_real_esp32_uart_driver, which load these Phase 2 packages through the existing hermes-host runtime.

Formal verification (tpt-telos)

hermes verify <pkg>.hermes now runs the real tpt-telos pipeline:

• memory safety — WASM linear memory is bounds-checked; the driver imports only from the hermes host module.
• capability isolation — every host capability the driver uses (MMIO / DMA / IRQ) is granted by the manifest. Drivers declare only the host imports they need (least privilege), so an over-broad import is caught.
• interrupt safety — the driver exports an interrupt handler and holds the IRQ capability it needs.
• power management — suspend / resume are exported.

Use hermes verify --embed to write the generated Certificate back into the package (the host can then check it before loading). Deeper proofs are layered on via the Kani and Prusti backends, which detect their tools on PATH and upgrade the relevant checks when available (otherwise they report skipped rather than downgrading the static proof). See docs/phase2-verification.md.

Project status

Phase 1 is complete (core traits, package format, host runtime with capability enforcement and real MMIO/DMA, CLI, and a packaged reference driver). Phase 2 delivers the driver catalog above and the tpt-telos verification pipeline. Items that still require hardware, external tooling, or publishing — QEMU integration tests, real-ESP32 LED blink, Kani/Prusti proof harnesses, crate publication, and vendor partnerships — are tracked in todo.md and the later roadmap phases.

License

Licensed under MIT OR Apache-2.0 at your option.