Introduction

Haven (Hypervisor for Asymmetric Virtualization ENforcement and isolation) is a static partition hypervisor research project targeting heterogeneous ARM64 SoCs. It is the artifact base for a Master’s thesis in Computer Engineering:

Static Partition Hypervisor for Asymmetric Multiprocessing: Enforcing Spatial and Temporal Isolation Between Linux and RTOS on a Heterogeneous SoC

The Problem

Modern heterogeneous SoCs ship multiple cores of fundamentally different classes on a single die - a Cortex-A cluster running Linux, a Cortex-M running FreeRTOS, optionally a Cortex-R for hard real-time - but there is no standard mechanism to guarantee that a bug or compromise in one partition cannot corrupt or starve another.

Existing solutions fall into one of two camps:

Approach	Examples	Problem
Full dynamic hypervisor	Xen, KVM	Large TCB, non-deterministic latency, certification-hostile
Bare-metal co-existence	No hypervisor	No isolation guarantee, shared memory races
Commercial RTOS partitioner	QNX Hypervisor, Integrity	Proprietary, non-auditable

The Approach

Haven runs at EL2 (the ARM hypervisor privilege level). At boot it:

1. Reads a static partition configuration fixed at compile time.
2. Programs stage-2 page tables to isolate each partition’s physical memory.
3. Configures the SMMU to restrict DMA-capable peripherals to their owning partition.
4. Routes each interrupt to exactly one partition via the GIC.
5. Activates a budget-based scheduler that enforces CPU time allocations.

After boot, the configuration is immutable. No partition can be created, migrated, or destroyed at runtime. This is the defining “static” property - it makes formal analysis tractable and reduces the trusted computing base to a few thousand lines of C.

Two Isolation Properties

The thesis must formally define, implement, and measure two properties:

Spatial Isolation

Partition A cannot read or write partition B’s memory or devices, enforced by:

• Stage-2 translation for CPU-initiated accesses (EL1/EL0 → EL2 → physical).
• SMMU policies for all DMA-capable peripheral accesses.
• Static peripheral ownership with deny-by-default: any access to an unowned peripheral triggers a stage-2 fault handled at EL2.

Temporal Isolation

Partition A consuming 100% CPU cannot delay partition B beyond a bounded worst-case, enforced by:

• CPU partitioning: RTOS and Linux assigned to disjoint core sets where the SoC topology permits.
• Budget scheduler: on shared cores, each partition is given a (budget, period) pair; the EL2 scheduler preempts overrunners and recharges budgets at period boundaries.

Why “Static” Is the Right Choice

Property	Static partition	Dynamic hypervisor
TCB size	~5 KLOC C	100 KLOC+
Formal analysis	Tractable	Very hard
IEC 61508 / ISO 26262	Feasible	Not feasible
Runtime reconfiguration	Not supported	Supported
RTOS latency bound	Provable	Statistical only

The gold standard for the security proof side is seL4 - the first formally verified OS microkernel. Haven does not aim for seL4-level formal verification, but it inherits the same architectural principle: minimize what must be trusted.

Thesis Scope

Next Steps

• Quick Start - build Haven, run QEMU smoke test.
• Architecture Overview - full design rationale.
• Chapter Traceability - how each repo artifact maps to a thesis chapter.