You are here

Event Details

MP Associates, Inc.
SUNDAY September 30, 2:00pm - 6:00pm | Einaudi
EVENT TYPE: TUTORIAL
SESSION 4T
Kickstarting Developing on seL4, the World’s Most Trustworthy and Difficult to Work With Microkernel

Speakers:
Gernot Heiser - Univ. of New South Wales & Commonwealth Scientific and Industrial Research Organisation
Kofi Doku Atuah - Univ. of New South Wales & Commonwealth Scientific and Industrial Research Organisation
Kent McLeod - Commonwealth Scientific and Industrial Research Organisation
Organizers:
Anna Lyons - Univ. of New South Wales & Commonwealth Scientific and Industrial Research Organisation
Gernot Heiser - Univ. of New South Wales & Commonwealth Scientific and Industrial Research Organisation
seL4 is a microkernel offering unprecedented trustworthiness in the form of formal verification of correctness, integrity, isolation and a known WCET. This tutorial will kick-start everything you need to know to start working on seL4 and is in four parts: an introduction to seL4, hands on working with the kernel API and scheduling model, hands on use of rump kernels for basic POSIX support, and a presentation on how to set up Linux VMs with guest to guest communication.

BIOGRAPHIES:
Anna just submitted her PhD at UNSW which completely altered the seL4 scheduling model, offering for the first time a principled model for managing time in L4 kernels. She’s now working as a senior engineer at CSIRO’s Data61 and assisting with UNSW’s Advanced Operating Systems course, which is based on seL4. Anna is interested in microkernel based OSes, trustworthy systems, practical real-time scheduling and teaching systems.

Gernot is Scientia Professor and John Lions Chair at UNSW Sydney, a Chief Research Scientist at CSIRO's Data61 and a Fellow of the IEEE, the ACM and the Academy of Technology and Engineering (ATSE). UNSW Gernot's main research interests are in operating systems, especially microkernel-based systems, and their use in critical systems; cyber-security, especially operating-system security; system trustworthiness and robustness; real-time systems; virtualisation; energy/power management and architectural support for operating
systems

Kofi is an engineer at UNSW working with CSIRO’s Data61 on seL4 and the surrounding ecosystem. Kofi cares about coordinating the currently disjoint world of drivers, and unifying the Free and Open Source world and strengthening open-source Operating Systems' ability to work with hardware vendors to get the drivers they need.

Kent is also an engineer at CSIRO’s Data61. His interests include Systems engineering and how using different operating system architectures can help construct trustworthy applications. He has previously worked on efficient reuse of existing operating system services in alternative operating environments. In the near future he is interested in finding out how better temporal and spatial isolation can be used to build useful mixed-criticality trustworthy systems.