Praktikum - Betriebssysteme - seL4 & TRENTOS
Learning Goals
- Development of embedded systems
- Understanding of the interplay between hardware, firmware/bootloader and operating system
- Understanding of state-of-the-art L4 microkernel technology
- Understanding of state-of-the-art microkernel based operating system (OS) design
- Teamwork in projects
Description
This course introduces the fundamental aspects of TRENTOS, a novel seL4 microkernel based secure embedded operating system developed by HENSOLDT Cyber. The first part of the course will cover the basic aspects required for embedded computing in general, providing an introduction to fundamental hardware aspects of the ARM and RISC-V architecture, their respective ISA as well as the final integration of a processor on a system on a chip (SoC). Based on the Broadcom BCM2837, the integration and utilization of a SoC is then exemplarily demonstrated by utilizing the widespread Raspberry Pi 3 B+ single-board computer (SBC). The second part will address the relevant preparation steps required for further OS utilization. Relevant aspects therefore include working with technical reference manuals (TRMs) as well as the utilization of relevant firmware and bootloader components (e.g. U-Boot). The third and final part will then introduce TRENTOS, a secure L4 microkernel based operating system for embedded system development. Therefore, in a first step, the design, architecture and the essential building blocks of the seL4 microkernel will be explained. Fundamental aspects like inter-process communication (IPC) or the core concept of capabilities will be presented in more detail. Based on top of seL4, the implementation of elementary OS aspects like system calls, device drivers, I/O management, processing and memory management is then presented. In a second step, the architecture, components and the usage of the CAmkES framework are shown. The framework provides kernel abstractions that are helpful for further OS and application development, allowing the provision of a suitable userland environment on top of seL4. The last step will then serve as a detailed introduction to the core concepts and basic software modules of TRENTOS, a secure operating system that utilizes both the seL4 microkernel and the CAmkES framework. Course participants will understand the inner workings of the OS and get in touch with the main OS aspects storage, networking and crypto support. Additional topics covered will target TRENTOS application and driver development.
Besides the theoretical aspects, the practical part of this course will focus on two aspects:
- As an individual, get in touch with the essential components of TRENTOS by working on homework tasks that deal with aspects like storage, networking and crypto on the Raspberry Pi 3 B+
- As a team, develop a fully featured show case utilizing TRENTOS on top of the Raspberry Pi 3 B+, interacting both with peripherals (different sensor and actuator devices) and a simulation environment (e.g. provided by a robotic simulator)
Prerequisites
- IN0009 or IN0034 or comparable courses with focus on operating systems
- Be proficient in the C or C++ programming language
- Be familiar with basic Linux (Unix) utilities such as ls, rm, grep, tar
- Be comfortable using any of the available text editors (e.g. emacs, vi, atom)
- Experience with any major Linux distribution is helpful but not strictly required
Examination
- Individual part: several homework assignments
- Team part
- Team project realization (Source code & documentation)
- Final presentation of the developed show case