Microkernels and Hypervisors

Microkernels and Hypervisors

Multi-tenant GPU isolation today relies on hypervisors. While hypervisors started small, broadly they have grown into full cloud-operating systems. KVM’s trusted computing base is roughly ten million lines of code; and while Xen is smaller (roughly 400k LoC) it is still quite large. Both have had VM-escape vulnerabilities — Google Project Zero’s 2021 KVM breakout via AMD SVM nested virtualization [1] is a representative example — and the PCI passthrough path that GPU workloads require widens the attack surface further, since IOMMU misconfigurations or missing PCI Access Control Services (ACS) can allow peer-to-peer DMA between devices assigned to different tenants. NVIDIA’s Multi-Instance GPU (MIG) partitioning provides hardware-level memory isolation within a single GPU, but the partitioning is managed by the host driver, which runs inside the hypervisor’s TCB.

Several projects have aimed to establish trust through verification at the hypervisor (and OS) level. To keep verification tractable, these projects aim to partition the system into a minimal trusted core (which holds exclusive access to page tables and privileged resources) and place policy decisions in a de-privileged layer. This architecture reflects the principles of the microkernel philosophy and many of these systems are microkernels, or draw inspiration from that line of work.

seL4 [2] is the poster-child for micro-kernel verification. Popularized in the DARPA HACMS program [3], seL4′s proof connects a top-level specification written in Isabelle to a binary-level semantics of the underlying architecture. The depth of this proof allows it to remove trust from the C compiler (which is known to have bugs) through translation validation. seL4 supports a range of platforms and comes in different variants for different levels of isolation, including an MCS mode built for mixed criticality systems [4]. While seL4′s verification is deep, its proof for modern, server-class machines is somewhat limited. The proof is fundamentally sequential, meaning that the proof itself does not cover running seL4 across multiple cores. Recent work aims to address this through a multi-kernel configuration (where a separate version of seL4 runs on each core). In addition the sequential nature of the proof also assumes the absence of DMA by external devices, though practically speaking the underlying assumption really only requires the lack of DMA to seL4-controlled memory.

Sharing the microkernel-philosophy of seL4, the NOVA microkernel [5] aims to be a modern contender in the verified hypervisor space. In contrast to seL4, NOVA is highly aggressive with respect to concurrency and modern hardware adoption including features such as encrypted memory, measured boot, as well as IOMMU/System MMU support. While the verification of NOVA is still underway, the proof tackles the problem of concurrent verification from the onset leveraging a highly modular proof strategy and recent work (2026) has begun moving NOVA’s proof to support the weak memory systems [6] present on modern architectures. In contrast to the seL4 proof, NOVA’s (partial) proof bottoms out at the source code level leaving the potential for compilers to introduce bugs or vulnerabilities into the final binary.

Amazon’s Nitro Isolation Engine [7] and the seKVM project [8] share similar goals in bringing verified system software to mainstream environments. Both projects verify a trusted core that runs in hypervisor mode and are driven by unverified but deprivileged components. Unlike seL4 and NOVA, these projects are not microkernels and their APIs are highly tailored to operate within their particular stacks. This narrower interface makes concurrency reasoning more tractable and both proofs support concurrent behaviors.

Beyond Hypervisor Mode

The architecture of isolating a small trustworthy (through verification) core from the higher-level requirements of modern hypervisors produces a good verification story, but the expressiveness of the API to the trusted module introduces a trade-off between capabilities and security. Projects such as seKVM embed policies within the verified core ensuring, e.g. that pages can not be shared (or read/write shared) between different domains. Embedding policies such as this directly within the verified code provides a strong guarantee, but can be limiting when trying to leverage these systems in contexts that seek more flexibility, e.g. allowing multiple domains the ability to communicate via shared memory.

On the microkernel side, seL4 and NOVA provide rich capability-based APIs that enable user-mode applications significant flexibility in resource allocation; however, the cost of this is that security guarantees such as isolation rely fundamentally on the correctness of the code that sets up these policies. seL4 provides the CAmkES framework [9] for configuring resources, but only supports static configurations. NOVA’s idiomatic usage is intended to be more dynamic; however, establishing isolation properties in this dynamic world requires user-mode verification. Efforts exist on both of these platforms to establish properties at the user-mode level. In the seL4 ecosystem, Kry10 [10] aims to raise the foundational guarantees of seL4 up the stack, and BlueRock Security has described how it has combined hypervisor- and user-mode verifications to build proofs of complete systems [11] (and technical reports on a verified VMM [12] and a verified virtual switch [13]).

Outlook and Next Steps

The “small trustworthy core” has been the crucial enabler for research and industrial systems to attack the hypervisor problem; however, the approach only goes so far. Neither seL4 nor NOVA, in isolation, is capable of running virtual machines, let alone supporting advanced features that many users expect from modern hypervisors such as dynamic provisioning and virtual machine migration. Bringing these core components into a trustworthy foundational stack is possible, but requires additional engineering effort to verify user-mode applications running atop these components. A core roadblock in this space is the sheer size of the technology stack that hypervisors support. Identifying a core feature set that would enable a wide swath of applications while still remaining tractable to verify with current technology is a key enabler for beginning to build these ecosystems.

A notable omission from the discussion above is device drivers. All of the hypervisor projects noted explicitly remove device drivers from the trusted core, a necessary step in controlling the size of the verified code; following the microkernel philosophy, device drivers are instead implemented in user-mode. While work on verifying device drivers exists [14], a major limiting factor is hardware complexity and modeling. While CPUs generally fall into only a handful of architectures, BlueRock’s work on a verified network switch [13] provides some insight into the complexity of reasoning about a VirtIO device, but the lack of source code makes it difficult to fully evaluate. The accelerator-specific half of this problem — producing a machine-checkable model of a GPU’s command and DMA surface and proving a driver against it — is the widget developed at §.

Solution/project Sketch

Being an enabler rather than a single widget, the deliverable here is the core feature set itself: the smallest set of hypervisor capabilities that lets a verified core run a realistic multi-tenant GPU workload, scoped tightly enough to stay in reach of current proof technology. Start by working backwards from one concrete workload — a fixed set of inference tenants, each pinned to a MIG slice — and enumerate the capabilities it actually exercises: guest creation and teardown, second-stage page-table management, interrupt routing, and the IOMMU configuration that backs MIG isolation. Deliberately exclude what the deployment does not need yet (live migration, memory overcommit, dynamic device hotplug), recording each exclusion as an explicit assumption rather than a silent gap. The output of this first stage is a specification, not a proof: a machine-readable interface to the trusted core plus the isolation invariant it must preserve — no guest can read, write, or fingerprint another guest’s memory or its MIG-partitioned slice — across every reachable sequence of capability calls.

Two build-out paths follow, and they can be pursued independently. On seL4, take the static-configuration story as far as it goes: express the workload’s resource layout in CAmkES [9] and prove the isolation invariant for that fixed configuration, accepting the loss of dynamism as the price of a closed proof. On NOVA, take the dynamic path: model the capability operations the workload issues at runtime and discharge the user-mode verification obligation that establishes the same invariant is preserved as guests are created and destroyed. Either path produces a reusable artifact — a verified minimal-hypervisor profile — and the gap between them measures exactly how much verification dynamism currently costs. The driver underneath both (§) is the one capability this sketch assumes rather than builds; the longer arc is to fold dynamic provisioning and VM migration back in, one capability at a time, each addition re-discharging the invariant.