David Cock

seL4 has received the 2022 ACM software system award

Press Release

Check out Enzian at ASPLOS'22

I lead the Enzian project within the Systems Group at ETH (project website). The goal of the project is, firstly, to explore the design space for computing platforms outside of commercially-available offerings (e.g. Linux on a CPU + GPGPU) and optimised industrial point solutions (e.g. Microsoft Catapult). The second goal is to provide a maximally flexible, high-performance platform for systems software and architecture research, and to make it available to the research community.

To this end we have designed and built a series of experimental platforms under the Enzian umbrella, with version 3 being the first publicly-available model comprising a 2GHz 48-core ARMv8 CPU (Cavium/Marvell ThunderX), connected via the CPU's native coherent inter-socket interconnect to a Xilinx XCVU9P Ultrascale+ FPGA, in a standard 2U rackmount server format. The design in fully open source (schematics available here, and production data here), and includes 8 DDR4 channels (up to 1TiB of DRAM), 2x40G and 4x100G network interfaces and many more goodies. A cluster of 7 machines on a 100G Tofino-based software-defined network fabric is now up and running at ETH, and available to external researchers. Contact us at contact@enzian.systems if you're interested!

The Enzian project has significant overlap with the Sockeye project, both in people and topics. Enzian is both a source of relevant and difficult hardware modelling problems, and a convenient experimental platform. This interplay has lead to a number of of efforts, including the model-checked I2C stack, and a declarative model of the CPU/FPGA power tree, allowing trustworthy power-sequencing instructions to be generated with an SMT solver.

Building Enzian forced us to confront head-on the complexity of booting, controlling, and managing a 2-socket server board. In particular, how to build a reliable, secure Baseboard Management Controller (BMC) was a pressing issue, one which affects every hardware manufacturer, and not just us. Our preliminary investigations convinced us that this problem is currently not very well addressed.

Thus we launched the Trustworthy BMC Project as a sub-project of Enzian, with strong links to our formal hardware modelling approach in Sockeye. Our approach, as details by Daniel Schwyn in his presentation at the 2022 seL4 summit is to apply the cyber-retrofit strategy successfully demonstrated in the HACMS project whereby components of an existing monolithic trusted system (in their case flight control software, in ours the OpenBMC software stack) are broken out and securely isolated over a separation kernel such as seL4, with the higher-criticality components gradually replaced with high-assurance replacements. In our case the first components to be isolated are the I2C stack and power-management code generated from a declarative specification.

Sockeye is an umbrella project for a number of efforts to tackle the formal, machine-readable specification of complex, non-uniform modern hardware platforms (from phone SoCs up to experimental server platforms such as Enzian). While Enzian serves as both a source of wonderfully complex examples and a convenient experimental platform for this work, the Sockeye project covers a much wider range of examples.

These include a formal model of the internal interconnect of the OMAP4460 and the non-intuitive effects on the cross-core memory address structure it imposes, as described in our MARS'17 paper, which also introduced the Decoding Net model of address translation which is foundational to the Sockeye effort. In his dissertation, Reto Achermann built on this foundation to formally describe the structure of more complex and/or unusual hardware, including PCIe-based systems with general-purpose accelerators (such as the Xeon Phi), and the infamous MIPS R4000 TLB. Lukas Humbel adapted the Decoding Net formalism to model interrupt delivery and built a model-checked specification and implementation of an I2C stack which cleanly incorporates partially- and non-compliant devices.

The Barrelfish/MAS (Multiple Address Spaces) project explored the implications of this non-uniform, disaggregated model of address translation and memory protection implemented by modern hardware on the systems software mechanisms needed to securely abstract, manage, and partition it. This resulted in an extension of Barrelfish's capability system to securely express authority over memory, address spaces, and translation resources (e.g. MMUs, IOMMUs, etc.) expressed in the Decoding Nets formalism we developed as part of the Sockeye project. This formed the basis of the mmapx() mechanism for UNIX-like OSes presented in our HOTOS'21 paper.

The runtime verification project has been ongoing since 2015, and has the modest goal of building the "Large Program Collider". This work builds on the observation that a modern system produces an enormous amount of detailed data about its execution, and that the tools to process this data at line rate (e.g. FPGAs) are now easily available.

Together with a series of excellent Masters students, inluding Pirmin Schmid and Tom Kuchler, we have an FPGA-based platform capable of ingesting ARM processor trace at line rate and evaluating ptLTL and TeSSLa properties (e.g. absence of memory leaks) in real time. We intend to port this platform to Enzian and integrate additional data including coherence traffic and the output of the CPU's integrated logic analyser modules.

I worked as a research engineer (or research assistant), under the supervision of Gerwin Klein, on the L4.verified project, which ran from 2005 until 2009, and produced the world's first formally verified general-purpose operating-system kernel, which is now available as open source!

I was responsible for the high-performance C and assembly implementation of the verified ARM kernel, which achieved the highest published IPC performance of any microkernel on this architecture.

I was also heavily involved in producing our underlying reasoning framework, in particular our monadic Hoare calculus.

A substantial fraction of the code in seL4, and its associated proof of correctness, is generated from a DSL by a tool I developed during the project. This code involves the low-level manipulation of packed structures (or bitfields). A description of this work has been published, and the tool itself is publically available

Since the information-flow proof for seL4 showed that storage channels could be provable eliminated in a kernel such as seL4, my Ph.D. work was on tackling timing channels, which are invisible to the type of formal specification used for seL4. For more detail on this project, see here.

The figure on the right shows the effectiveness of one of our mitigation strategies, scheduled delivery, used here to mitigate the Lucky 13 attack against OpenSSL. This can be implemented without kernel modification, and achieves higher performance and better security than a constant-time implementation. For more information, see our CCS 2014 paper.

While this work began as part of my research as a student at UNSW/NICTA, it has since been continued and extended by further work by Qian Ge (at UNSW), and Nils Wistoff (at ETH). The Time Protection project at UNSW is a follow up to this effort and aims to provide robust hardware and software mechanisms to ensure the provable absence of time-based leakage mechanisms.

To support my PhD work, I developed a formalisation of the probabilistic programming logic/refinement calculus pGCL, of McIver and Morgan. This package is available under an open source license, and is now in the archive of formal proofs. For archival versions, see here.

Also as part of my PhD work, I conducted a systematic large-scale empirical study of side-channel bandwidth on seL4. The toolkit that I built up in the course of this work, in order to efficiently process and analyse large sparse channel matrices, has also now been released.

The figure on the right shows the residual channel on and Exynos4412, after using instruction-based scheduling to mitigate the cache-contention channel. For more details, see the paper, or my Ph.D. thesis, available below.

This toolchain is still in use in the follow-up Time Protection project, alongside the leakiEst tool of Chothia et. al.

The Barrelfish project explored the design space for operating systems on modern hardware, specifically large-scale nonuniform multiprocessor systems and heterogeneous and non-traditional hardware such as programmable NICs. Barrelfish introduced the multikernel: a fully-partitioned per-core capability-based microkernel (called a CPU driver), with synchronisation of kernel state coordinated by a trusted user-level monitor using efficient inter-core communication.

I joined the Barrelfish team as an alumnus of the seL4 project, and my contributions include the ARMv8 port and the formal aspects of the Barrelfish/MAS extension as part of Sockeye.

While Barrelfish is no longer in active development, it is still in use as a teaching system in the Advanced Operating Systems course at ETH.

I teach Advanced Operating Systems in the spring semester, alongside Prof. Roscoe. The official course description is available here, and the spring 2022 course website is here.

AOS is a capstone course in the Systems track at ETH, which gives advanced undergraduate students the opportunity to work in self-guided teams to design, build, evaluate, and document their own operating system on real hardware on top of the Barrelfish CPU driver.

I teach Informal Methods in the autumn semester. The official course description is available here, and the autumn 2022 course website is here.

This course is aimed at students who are already good programmers, but want to be great ones. We take well-known formal techniques (such as Hoare logic) that you have likely encountered in a theoretical setting and see how to apply the most useful parts as a practical toolkit to both improve your programs and help you be confident that your code will work first time. The emphasis is on practicing skills such as identifying a loop invariant until they're second nature, and to really master a set of skills that'll remain useful even if you never apply the full weight of formal verification in your work.