Microkernel and Component-Based OS
Making the NOVA microhypervisor fit for thousands of devices and interrupts
<p><a href="https://github.com/udosteinberg/NOVA">NOVA</a> 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.</p>
<p>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. </p>
<p>Architectural differences between ARMv8-A and x86_64, such as</p>
<ul>
<li>Interrupt types: PIN/MSI (x86) vs. (E)SPI/(E)PPI/LPI (Arm)</li>
<li>CPU-local vectors (x86) vs. global INTIDs (Arm)</li>
<li>Interrupt remapping by IOMMU (x86) vs. interrupt translation by GIC ITS (Arm)</li>
<li>Source identifier as bus/device/function (x86) vs. device/stream ID (Arm)</li>
</ul>
<p>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</p>
<p>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.</p>
<p>Links:</p>
<ul>
<li><a href="https://github.com/udosteinberg/NOVA">NOVA Source Code</a></li>
<li><a href="https://gitlab.com/bluerocksec/NOVA/-/tree/proof/ver">NOVA Formal Specification</a></li>
<li><a href="https://hypervisor.org/">Additional Information</a></li>
<li><a href="https://archive.fosdem.org/2025/schedule/event/fosdem-2025-5083-a-formal-specification-of-the-nova-microhypervisor/">FOSDEM 2025 Talk</a> - focused on Formal Verification</li>
<li><a href="https://archive.fosdem.org/2024/schedule/event/fosdem-2024-3227-using-the-nova-microhypervisor-for-trusted-computing-at-scale/">FOSDEM 2024 Talk</a> - focused on Trusted Computing</li>
<li><a href="https://archive.fosdem.org/2023/schedule/event/nova">FOSDEM 2023 Talk</a> - focused on Advanced Features</li>
<li><a href="https://archive.fosdem.org/2020/schedule/event/uk_nova">FOSDEM 2020 Talk</a> - focused on ARMv8-A</li>
</ul>
Weitere Infos
| Live Stream | https://live.fosdem.org/watch/k4201 |
|---|---|
| Format | devroom |
| Sprache | Englisch |
Weitere Sessions
| 01.02.26 |
<p>The ongoing digitalization has made cloud services and data centers the backbone of significant parts of our modern society and economy. Thus, exposing more and more sensitive data to a plethora of novel threats, both in terms of security and safety. However, most of today's cloud infrastructure runs on monolithic system software that makes it hard to harden against security leaks or unwanted outages by relying on too coarse-grained capabilities or having to orchestrate multiple security ...
|
| 01.02.26 |
<p>This talk gives an overview of skiftOS’s architecture, focusing on its microkernel core and service model. It explores the design trade-offs behind keeping the kernel minimal yet practical, and the lessons learned from building a complete, usable operating system on top of it.</p> <p>The session is aimed at developers interested in microkernels, operating system internals, and the challenges of scaling a small core into a functional ecosystem.</p> <p>Project Repo: ...
|
| 01.02.26 |
<p>The <em>Genode OS Framework</em> is certainly not a newcomer but still under very active development. While the framework supports various third-party microkernels, its custom-tailored <em>base-hw</em> kernel has proven valuable for putting Genode-specific (kernel) concepts to the test. One of those concepts that we have been test-driving for about a decade was the <em>quota-aware CPU scheduling</em>, which combined CPU-quota trading with priority-based scheduling. However, with Sculpt OS as ...
|
| 01.02.26 |
<p><a href="https://www.redox-os.org/">Redox</a> is a Unix-like microkernel operating system, community developed and written in Rust. Funded through NGI Zero Commons and NLnet, Redox is developing Capability Based Security as a fundamental part of interprocess communication and file I/O. This presentation will look at our strategies for implementing capabilities, POSIX file descriptors, namespaces, containment, and escalation.</p>
|
| 01.02.26 |
<p>As kernels manage hardware, in certain cases the only way to prevent race conditions in kernel code is to disable interrupts. This is a kernel way of granting code exclusive access to resources at lowest levels.</p> <p>In the realm of embedded devices, it is often not feasible to keep interrupts disabled for prolonged period of time. This affects the design of portions of the kernel which modify data structures accessible from within interrupt context. Despite very limited API offered by the ...
|
| 01.02.26 |
<p>This presentation describes the technical implementation of PhantomOS, an orthogonally-persistent operating system, on modern microkernel architecture using the Genode framework. The talk center on the engineering challenges encountered during the porting process, especially the adaptation of the core persistence mechanisms. The talk will also touch on work on network persistence and the added WASM runtime.</p> <p>As part of the port, the snapshot process was reworked and separated into its ...
|
| 01.02.26 |
<p>axle OS (<a href="https://github.com/codyd51/axle">GitHub</a>, <a href="https://axleos.com/blog/">blog</a>) is a hobby microkernel and userspace which includes many home-grown utilities such as <a href="https://github.com/codyd51/axle/tree/paging-demo/rust_programs/linker/src">an x86_64 assembler + ELF linker</a>, a <a href="https://github.com/codyd51/axle/tree/paging-demo/programs/subprojects/net">TCP/IP/(ARP/DNS</a>/<a ...
|
