Video details

Spunky: a Genode Kernel in Ada/SPARK

C++
08.04.2020
English

by Martin Stein
At: FOSDEM 2020 https://video.fosdem.org/2020/AW1.125/ada_spunky.webm
❮p❯The Genode OS framework is an open-source tool kit for building highly secure component-based operating systems scaling from embedded devices to dynamic desktop systems.
It runs on a variety of microkernels like SeL4, NOVA, and Fiasco OC as well as on Linux and the Muen SK. But the project also features its own microkernel named "base-hw" written in C++ like most of the Genode framework.❮/p❯
❮p❯Spunky is a pet project of mine.
Simply put it's an approach to re-implement the design of the "base-hw" kernel first in Ada and later in SPARK with the ultimate goal to prove its correctness. It is also an opportunity to learn how Genode can benefit from Ada and SPARK in general and promote the use of safety-oriented languages in the project.❮/p❯
Room: AW1.125 Scheduled start: 2020-02-01 14:30:00