Microkernels and Component-based OS

The HIPPEROS RTOS

A Song of Research and Development
K.4.601
Antonio Paolillo
HIPPEROS is an upcoming open source RTOS that was developed at ULB and by a former spin-off company of ULB. The talk will be a presentation followed by an open discussion about the main architecture principles of the HIPPEROS kernel and OS, what platforms and architectures we support and our agenda regarding open source.
This multitasking RTOS is specifically designed to take advantage of multi-core platforms for critical, hard real-time applications that must be predictable. It targets high-end embedded platforms that exhibit heterogeneous parallelism. The HIPPEROS kernel is designed from scratch in order to support recent process models present in the real-time systems research literature. The RTOS is based on a micro-kernel with an asymmetric master/slave architecture. It allows to natively support parallel processor architectures, by dedicating one core to the heavy operations of the kernel (scheduling, memory management, etc.) and the other cores can then execute user mode application and serve real-time tasks with very few interferences. The OS kernel was designed and implemented by a team made of people from the ULB PARTS laboratory (http://parts.ulb.ac.be/). The goal was to create a spin-off company around the topic of Real-Time Operating Systems, including the creation of a new micro-kernel for high-end embedded systems with an innovative software architecture, backed-up by research (both theoretical and applied), designed, developed and maintained with "good" (and agile) software design methodology. Within this business, a side objective was to maintain strong links with universities and the research world, by validating the OS design in an academic environment and continuous research activities. Currently, the company is under liquidation. The state of the project is frozen but we started an ongoing initiative aiming to open source the code base. This would allow external contributions and therefore continuing maintenance and development of new features. HIPPEROS could then become a test ground for academics and industrials that aim to try new ideas regarding the reliability and efficiency of their systems. With no such undertaking, the code base might just disappear, therefore cancelling out the 7-year team effort.

Additional information

Type devroom

More sessions

2/2/20
Microkernels and Component-based OS
Gernot Heiser
K.4.601
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
Microkernels and Component-based OS
Nils Asmussen
K.4.601
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
Microkernels and Component-based OS
Jakub Jermář
K.4.601
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
Microkernels and Component-based OS
Hajime Tazaki
K.4.601
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
Microkernels and Component-based OS
Dmitry Zavalishin
K.4.601
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
Microkernels and Component-based OS
Johannes Kliemann
K.4.601
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
Microkernels and Component-based OS
Alexander Senier
K.4.601
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, ...