Spatial Isolation
Stage-2 page tables enforce per-partition memory boundaries. SMMU policies extend this to DMA-capable peripherals. No cross-partition access is possible after boot.
Partition once, isolate forever.
Haven is a research static partition hypervisor for heterogeneous SoCs. Fix CPU, memory, and interrupt ownership at compile time - then enforce it in hardware at EL2 with no runtime overhead.
Temporal Isolation
Budget-based EL2 scheduler assigns CPU time to each partition. Linux load spikes cannot delay RTOS deadlines beyond a proven bound.
Minimal TCB
The trusted computing base is a few thousand lines of C. No dynamic allocation, no garbage collection, no unbounded loops in the core isolation path.
Thesis-grade Evidence
Every claim maps to a measurable artifact: latency distributions, isolation fault-injection results, and chapter traceability matrices.
System Architecture
┌───────────────────────────────────────────────────┐│ Guest Partitions (EL1/EL0) ││ ┌─────────────────┐ ┌──────────────────────┐ ││ │ Linux (A55×4) │ │ FreeRTOS (M7 / A55) │ ││ └────────┬────────┘ └──────────┬───────────┘ │├────────────┼───────────────────────┼──────────────┤│ │ EL2 - Haven │ ││ ┌────────▼────────────────────────▼───────────┐ ││ │ Stage-2 MMU │ IRQ Router │ Budget Sched │ ││ │ SMMU policy │ EL2 exc handler │ Time acct │ ││ └─────────────────────────────────────────────┘ │├───────────────────────────────────────────────────┤│ Hardware (ARM64 SoC) ││ Cortex-A55 × 4 │ GIC-700 │ SMMU-700 ││ Cortex-M7 (MCU) │ DDR5 │ Peripherals │└───────────────────────────────────────────────────┘Primary Platform
| Board | SoC | Cores | Status |
|---|---|---|---|
| NXP i.MX95 Dev Kit | i.MX95 | Cortex-A55 × 4 + Cortex-M7 | Primary target |
| QEMU virt (arm64) | virtual | Cortex-A57 (emulated) | CI gating |
| NXP i.MX8QM-MEK | i.MX8QM | Cortex-A53 × 4 + Cortex-M4 | Secondary validation |