Making the NOVA microhypervisor fit for thousands of devices and interrupts

NOVA is a modern open-source (GPLv2) microhypervisor that can host and harden unmodified guest operating systems. NOVA is typically accompanied by a component-based OS that runs deprivileged and implements additional functionality, such as platform services and user-mode device drivers.

Over the years, the interrupt subsystem of modern client and server platforms has evolved significantly, by (1) scaling up from only a few pin-based to thousands of message-signaled interrupts and (2) scaling out the delivery of those interrupts across dozens or hundreds of CPU cores.

Architectural differences between ARMv8-A and x86_64, such as

• Interrupt types: PIN/MSI (x86) vs. (E)SPI/(E)PPI/LPI (Arm)
• CPU-local vectors (x86) vs. global INTIDs (Arm)
• Interrupt remapping by IOMMU (x86) vs. interrupt translation by GIC ITS (Arm)
• Source identifier as bus/device/function (x86) vs. device/stream ID (Arm)

pose a challenge to the design of a uniform API for managing interrupts and devices and motivated the introduction of a new type of kernel object in NOVA: Device Contexts

After a brief discussion of NOVA features added recently, the majority of the talk will focus on NOVA's new interfaces for managing hardware devices and interrupts.

Links:

• NOVA Source Code
• NOVA Formal Specification
• Additional Information
• FOSDEM 2025 Talk - focused on Formal Verification
• FOSDEM 2024 Talk - focused on Trusted Computing
• FOSDEM 2023 Talk - focused on Advanced Features
• FOSDEM 2020 Talk - focused on ARMv8-A