Microkernels and Component-based OS
NOVA Microhypervisor on ARMv8-A
NOVA is a modern open-source microhypervisor that can host unmodified guest operating systems next to critical host applications. Although originally developed for the x86 virtualization extensions of Intel and AMD, the internals of the microhypervisor and its external API were designed with flexibility in mind, such that the code could also be ported to other architectures.
In this talk we present the first ever version of NOVA on ARMv8-A.
We will show how the NOVA abstractions map onto the ARM architecture, how modern virtualization features such as GIC and SMMU are being used, discuss the ongoing evolution of the NOVA API and how the ARM port differs from the earlier x86 version.
The talk will conclude with a short demo, an outlook into the NOVA roadmap and the formal verification efforts around the code base, as well as opportunities for collaboration with the NOVA community.
Additional information
| Type | devroom |
|---|
More sessions
| 2/2/20 |
I will give an overview of where seL4 stands today in terms of functionality, verification, ecosystem, deployment and community. The focus will be on what has happened in seL4 land over the past 12 months, which is a lot: seL4 Foundation, RISC-V support and introducing time protection.
|
| 2/2/20 |
Current microkernels have shown to provide advantages in terms of security, robustness, and flexibility of systems. However, in recent years, the hardware added new challenges that need to be addressed as well, demanding approaches that include the hardware into the picture. First, hardware is getting more and more heterogeneous and consists not only of general-purpose cores, but contains also various accelerators. Second, system designers need to integrate untrusted third-party components ...
|
| 2/2/20 |
This is going to be an all-encompassing update talk for HelenOS developments that happened in the Year of the Pig (since the last FOSDEM).
|
| 2/2/20 |
LKL (Linux Kernel Library) is aiming to allow reusing the Linux kernel code as extensively as possible with minimal effort and reduced maintenance overhead. It allows us to link the library with any programs (which wish to call as a function call) containing Linux kernel code. There are many use cases: reading/writing files without general system calls, putting experimental protocol implementation without neither of host kernel update nor kernel module installation, using customized kernel in ...
|
| 2/2/20 |
Phantom OS is an Operating system based on the orthogonal persistence. Application does not feel OS shutdown and restart. Even abrupt restart. It is guaranteed that application will be restarted in consistent state.
|
| 2/2/20 |
Gneiss is an abstraction layer for component based environments that aims to provide a foundation for formally provable components. It enables the creation of platform independent, asynchronous components in SPARK and provides function contracts that allow to prove the correct interaction with the underlying platform.
|
| 2/2/20 |
With 2.5 billions of active users Android is the most widely deployed mobile operating system in the world. Its vast complexity paired with a monolithic architecture regularly result in severe security issues like the infamous Stagefright bug. In this presentation we talk about an ongoing research project which aims at running Android applications on top of the component-based Genode OS framework and secure them using formally verified components. We discuss how Android applications interact, ...
|
