seL4 Summit 2022 Program

All times are local time in Munich, Germany (UTC+2). Session chairs shown on right.

13 October 2022

seL4: from zero to hello world

Ihor Kuz, Kry10

9:00 - 10:00

This session will help you setup a development environment for building and running seL4-based systems.

Most tutorials and trainings begin with a step zero: "set up your development environment and all the prerequisites, then run 'hello world' to confirm that your setup works". It's expected that this step is trivial and "just works" and participants are expected to have already done this (at home) before showing up to the tutorial or training session.

For many people this works. But for some people it doesn't "just work". Maybe they don't have time or resources to do the preparation, maybe despite their best efforts something doesn't work right, or maybe they want to set up their system a bit differently (e.g. a different OS) and the basic instructions are not enough. If that's you, then this session is for you.

In this session we'll walk through the development environment setup, and provide assistance to make sure you have a setup that works so that you can actively participate in any of the other tutorials and trainings sessions.

If you already have a working development environment set up, then you can probably skip this session - unless you want to lend a hand helping others get set up, in which case, come on down. We may even have cookies.

CAmkES

Sebastian Eckl, HENSOLDT Cyber

10:15 - 10:45

CAmkES (Component Architecture for microkernel-based Embedded Systems) is a software development and runtime framework that shall ease systems development by providing an abstraction layer on top of the seL4 microkernel. As part of this workshop, participants shall therefore get to know the general CAmkES architecture as well as its basic building blocks. Finally, the execution of a corresponding CAmkES-based application on top of seL4 will be demonstrated.

TRENTOS

Sebastian Eckl, HENSOLDT Cyber

10:45 - 12:00

With TRENTOS, HENSOLDT Cyber develops a novel secure embedded OS on top of the proven seL4 ecosystem. The CAmkES framework is hereby utilized for providing the respective abstraction layer on top of seL4, which allows for constructing respective OS components and services (e.g. for storage or networking support) within TRENTOS. As part of this workshop, participants shall therefore get to know the general TRENTOS architecture, its basic building blocks as well as the standard TRENTOS operating system components. Finally, with the help of the TRENTOS SDK, a small TRENTOS application will be developed and the corresponding build and deployment process will be demonstrated.

The seL4 Core Platform (seL4CP)

Ivan Velickovic, in collaboration with Peter Chubb, UNSW

13:00 - 14:30

The seL4 Core Platform (seL4CP) is a minimal Operating System built on top of seL4. It was designed to be simple enough that those without prior experience with seL4 can get started easily in building secure performant systems on seL4. seL4CP provides lean abstractions so that seL4 can be used for building reliable systems easily, without being restricted to a specific environment. This workshop will introduce you to seL4CP such that by the end, you will be able to build systems for your own purposes and know how to run them on hardware. We'll also give a brief overview of the internals of seL4CP to make it a little easier for participants to port seL4CP to their own hardware.

DornerWorks' VM Composer: the easy button for virtualized seL4-based systems

Chris Guikema & Robbie VanVossen, DornerWorks

14:30 - 15:15

A secure kernel is more and more attractive these days and seL4 is one of the strongest microkernels around. However, the seL4 ecosystem is still maturing and may not be a drop-in replacement for practical applications in real-world systems. With the strictest security needs, it is probably best to use just the microkernel with user-space applications. However, there are many stacks, libraries, and drivers lacking to meet the needs of most systems. Virtualization and the user-space VMM provide an answer to this. For developers new to the seL4 ecosystem, it is difficult to configure the software to meet system requirements. The traditional approach is to start with a known working configuration and tweak it until it fits the specific application. The latest approach is to use DornerWorks' VM Composer, a graphical, drag-and-drop interface which allows one to easily configure their seL4-based, virtualized systems without needing to modify any CMake, CAmkES, python, or C files. This training session will provide step-by-step instructions to configure an example virtualized system using an evaluation version of the tool. It will show basic and advanced configuration options. It will also create some invalid configurations to show the validation that the tool performs.

BriefCASE Tutorial

Isaac Amundson & Darren Cofer, Collins Aerospace

15:30 - 17:00

As part of DARPA's Cyber Assured Systems Engineering (CASE) program, our team has developed a model-based systems engineering environment called BriefCASE that integrates formal methods at all levels of system design, including the ability to build systems targeting seL4. In this hands-on session we will provide a top to bottom demonstration of the tools, transforming a system model to address cyber requirements, verifying the correctness of the model, generating component implementations from formal specifications, generating infrastructure code to run on seL4, automatically producing an assurance case documenting the design rationale, and running the final system in emulation on QEMU. A virtual machine containing all necessary tools and models will be provided before the session.