Experience Developing Code for the seL4 Environment - Wyeth Greenlaw Rollins, Caitlyn Wilde

Experience Developing Code for the seL4 Environment - Wyeth Greenlaw Rollins, Caitlyn Wilde

We have developed a minimal networking stack (Ethernet, IP, UDP, and ICMP) with the overarching goal of proving that it implements its specification correctly. We target our implementation for the embedded market and therefore we have chosen to develop our solution around the seL4 Microkit and the seL4 Device Driver Framework.
In this talk, we report on our experience developing, testing, and characterizing the performance of our implementation using the seL4 ecosystem. We have containerized our development environment to simplify building our application and to support users with differing platforms. In addition to relying on automated theorem prover assistants and model checkers, we have written many unit and integration tests to help write correct software. Using a network benchmark, we show that our solution exhibits competitive, if not superior, performance characteristics both in terms of average behavior and variance.