Notes from the first seL4 workshop

This was a presentation by Alexsey Nogin from HRL about the work they are doing as part of the "ground team" of DARPA’s HACMS program. This included some of the various components they are using and the overall system structure.

Gernot talked about the current roadmap for seL4 and what recent work has been done. In particular he pointed out that the RT kernel is currently available and that multicore and x64 is in master. He also announced that, in the near future, there will be an explicit "stage" branch which will eventually be merged into master, as verification is completed for new pieces. The first thing added will be RT. The seL4 roadmap has been updated to reflect current reality.

This was my talk. The slides are available. I talked about some design patterns that we’ve come up with for robust dynamic systems: space banks, bushels, extended virtual message registers, and briefly mentioned persistence and drivers.

There will be more available on this in the coming weeks.

Oak Rattanavipanon, from UC Irvine, talked about the work they have been doing to get remote attestation on seL4. Their approach right now considers only remote adversaries. They modify the kernel to work with the Sabre Lite’s secure boot. From this, they have some code which runs (currently) in the root thread to provide a hybrid attestation scheme. Using the hardware root of trust provided by the Sabre Lite’s secure boot implementation, they use the guarantees provided by seL4 to ensure confidentiality of the attestation key and integrity of the attestation code.

On top of this, they implement a simple network protocol wherein a remote verifier can request a MAC of a region of memory on the verifier. If the MAC matches what the verifier expects, then the verifier can trust that the software on the remote device hasn’t been subverted. There were a bunch of questions about the actual network protocol they use. Currently, they use a nonce to prevent replay, but the MAC is otherwise transported in cleartext with no other authentication.

I recall that they plan on releasing their code open source, but don’t have that written in my notes so that memory may be faulty.

Andrea Sorbini, from Real Time Innovations, talked about work they have been doing to bring one of their products, "RTI Connext DDS Micro", a :dds:[data distribution service] middleware, to seL4. They are doing this as part of a DARPA SBIR project. The tagline used to introduce the project was "What good is formal verification if you don’t have friends to talk to?". DDS is a pub/sub based peer-to-peer communications system. It provides structured message transport and has a variety of quality of service configuration such as transport reliability, message history, delivery deadlines, durability, liveliness, and resource limits. The seL4 implementation supports most of these properties, and it was created from the DO178C certifiable subset of the product which requires static configuration of resources and communication paths. They are investigating using formal verification in cooperation with Galois to show memory safety of their receive path.

The primary challenge they ran into was a lack of an OS personality to target. They ended up building a libsel4osapi which provides interfaces for a clock, network, UDP, serial communication, timers, and a process abstraction. They did not enjoy doing this, commenting that "minimalism is no excuse for poor developer experience". They had quite a few suggestions for what would make their experience much more pleasant, many of which came up during the "gaps" conversation.

Chris Guikema, from DornerWorks, talked about the work they have been doing to enable more robust and advanced GDB debugging of especially CAmkES components. They have taken the x86 GDB server that Data61 has developed and ported it to ARM, adding some features along the way. Parts of their code are available online to start using. I recall seeing a link to their GDB server in the slides, but can’t find it now.

Ihor Kuz, from Data61, gave an introduction to virtualization theory, including the basics of Popek-Goldberg virtualizability and the distinction between privileged and sensitive instructions. He gave an overview of virtualization in practice on x86 and ARM, as well as how some of the seL4 abstractions of these mechanisms work.

At the end of the day, we wrapped up with a discussion of gaps in seL4. Gernot went over a document that they created listing what they perceive as the gaps. There was general agreement among the audience with the analysis. I requested access to x86 MSRs, but no one else had any additions. There was then a brief conversation about one of the most pressing issues: drivers. The current idea is to have tables on the wiki containing links to open source drivers and a basic evaluation of them. Someone also floated the idea of a tool which boots Linux on a board, scans what devices are available, and puts together a report indicating which have drivers available for seL4 and where they can be found.