Systems Group, ETH Zürich
It has become apparent that producing hardware and systems software to the highest degree of assurance is possible, without sacrificing performance, and at lower cost than has historically been assumed. With careful design and effective use of automation, it should be possible to reduce the cost to the point that such an approach is commonplace for critical systems, and tackle currently unsolved issues, including concurrency. A strong familiarity with the discipline of low-level systems programming, and an understanding of the application domain will remain essential to ensure that performance is not sacrificed. Likewise, a clear understanding of the state of the art in formal verification is essential to ensure that systems are designed such that verification remains tractable.
Check out Enzian at ASPLOS'22
CVFull CV here.
- Senior Researcher & Lecturer, ETH Zürich.
- Ph.D., UNSW, "Leakage in Trustworthy Systems", adviser Gernot Heiser.
- Research Engineer, L4.verified.
- B.Sc. (hons), UNSW
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 firstname.lastname@example.org 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.
Verified Bitfield Generation
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
Timing Channels in seL4
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.
pGCL in Isabelle
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.
Covert Channel Analysis Suite
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.
Advanced Operating Systems
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.
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.
Selected Talk Slides & Recordings
|Enzian: An Open, General, CPU/FPGA Platform for Systems Software Research||ASPLOS 2022||video|
|The Enzian Project - Status 2021||ETH Systems Lunch Seminar 2021||video|
|Generating correct initial page tables from formal hardware descriptions||PLOS 2021||video|
|mmapx: Uniform Memory Protection in a Heterogeneous World||HOTOS 2021||video|
|Modeling the OS/Hardware Interface with Sockeye||ENTROPY 2018||slides|
|Enzian: A Research Computer||ETH Systems Group Industry Retreat 2018||slides|
|The Impact of Incomprehensible Hardware on Security||Inria Rennes 2017||slides|
|New Projects at ETH Systems||Data61/CSIRO 2017||slides|
|Runtime Verification: Building the Large Program Collider||ARM Research Summit 2017||slides||video|
|Runtime Verification||ETH Systems Group Industry Retreat 2017||slides|
|ARM at ETH Systems||ARM Research Summit 2016||slides|
|FPGAs as Tools and Architectures at ETH Systems||Xilinx Dublin 2016||slides|
|Litmus Testing at Rack Scale||MARS 2016||slides|
|Formal Methods and Systems||ETH Systems Group Industry Retreat 2016||slides|
|The State of the Barrelfish Project||ETH Systems Group Internal Retreat 2015||slides|
|Capabilities in seL4||ETH Systems Group Lunch Seminar 2015||slides|
|Program Verification as a Toolbox||ETH Systems Group Industry Retreat 2015||slides|
|The Last Mile—An empirical study of timing channels on seL4||CCS 2014||slides|
|Navigating the Literature||SSRG Student Bootcamp 2014||slides|
|Ten Years of Trustworthy Systems||ETH, EPFL 2014||slides|
|From Probabilistic Operational Semantics to Information Theory—Side Channels with pGCL in Isabelle||ITP 2014||slides|
|Measuring and Mitigating Side Channels||ETH, EPFL, LIP6 2013; SSRG Summer School 2014||slides|
|Practical Probability—Applying pGCL to Lattice Scheduling||ITP 2013||slides|
|Verifying Probabilistic Correctness in Isabelle with pGCL||SSV 2012||slides|
|Lyrebird||SSV 2010; Cambridge 2013||slides|
|[CRS+22]||David Cock, Abishek Ramdas, Daniel Schwyn, Michael Giardino, Adam Turowski, Zhenhao He, Nora Hossle, Dario Korolija, Melissa Licciardello, Kristina Martsenko, Reto Achermann, Gustavo Alonso, and Timothy Roscoe. Enzian: An open, general, CPU/FPGA platform for systems software research. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, page 434–451. ACM, 2022. [ DOI ]|
|[ACH+21a]||Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, and Daniel Schwyn. Generating correct initial page tables from formal hardware descriptions. In Proceedings of the 11th Workshop on Programming Languages and Operating Systems, page 69–75. ACM, October 2021. [ DOI ]|
|[SSG+21]||Jasmin Schult, Daniel Schwyn, Michael Giardino, David Cock, Reto Achermann, and Timothy Roscoe. Declarative power sequencing. ACM Transactions on Embedded Computing Systems, 20(5s), September 2021. [ DOI ]|
|[ACH+21b]||Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, and Daniel Schwyn. mmapx: Uniform memory protection in a heterogeneous world. In Proceedings of the 18th Workshop on Hot Topics in Operating Systems, page 159–166. ACM, June 2021. [ DOI ]|
|[HSH+21]||Lukas Humbel, Daniel Schwyn, Nora Hossle, Roni Haecki, Melissa Licciardello, Jan Schaer, David Cock, Michael Giardino, and Timothy Roscoe. A model-checked I2C specification. In Alfons Laarman and Ana Sokolova, editors, Proceedings of the 27th International SPIN Symposium on Model Checking of Software, pages 177--193. Springer, 2021. [ DOI ]|
|[ARC+20]||Gustavo Alonso, Timothy Roscoe, David Cock, Mohsen Ewaida, Kaan Kara, Dario Korolija, David Sidler, and Zeke Wang. Tackling hardware/software co-design from a database perspective. In Proceedings of the 10th Conference on Innovative Data Systems Research, January 2020. [ DOI ]|
|[AHH+19]||Reto Achermann, Nora Hossle, Lukas Humbel, Daniel Schwyn, David Cock, and Timothy Roscoe. A least-privilege memory protection model for modern hardware. 2019. eprint. [ DOI ]|
|[HHA+19]||Roni Haecki, Lukas Humbel, Reto Achermann, David Cock, Daniel Schwyn, and Timothy Roscoe. CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer. 2019. eprint. [ DOI ]|
|[AHCR18]||Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Physical addressing on real hardware in Isabelle/HOL. In Jeremy Avigad and Assia Mahboubi, editors, Proceedings of the 9th International Conference on Interactive Theorem Proving, volume 10895 of Lecture Notes in Computer Science, pages 1--19. Springer, July 2018. [ DOI ]|
|[GYCH18]||Qian Ge, Yuval Yarom, David Cock, and Gernot Heiser. A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. Journal of Cryptographic Engineering, 8(1):1--27, 2018. [ DOI ]|
|[AHCR17]||Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Formalizing memory accesses and interrupts. In Holger Hermanns and Peter Höfner, editors, Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems, volume 244 of Electronic Proceedings in Theoretical Computer Science, pages 66--116. Open Publishing Association, April 2017. [ DOI ]|
|[CGMH14]||David Cock, Qian Ge, Toby Murray, and Gernot Heiser. The last mile: An empirical study of timing channels on seL4. In Proceedings of the 21st ACM SIGSAC Conference on Computer and Communications Security, pages 570--581. ACM, November 2014. [ DOI ]|
|[Coc14b]||David Cock. Leakage in Trustworthy Systems. PhD thesis, UNSW Computer Science and Engineering, Sydney, Australia, August 2014. https://doi.org/10.26190/unsworks/16942. [ DOI ]|
|[Coc14c]||David Cock. pGCL for Isabelle. Archive of Formal Proofs, July 2014. http://isa-afp.org/entries/pGCL.shtml, Formal proof development.|
|[Coc14a]||David Cock. From probabilistic operational semantics to information theory - side channels with pGCL in Isabelle. In Proceedings of the 5th International Conference on Interactive Theorem Proving, volume 8558 of Lecture Notes in Computer Science, pages 177--192, Vienna, Austria, July 2014. Springer. [ DOI ]|
|[Coc13]||David Cock. Practical probability: Applying pGCL to lattice scheduling. In Proceedings of the 4th International Conference on Interactive Theorem Proving, volume 7998 of Lecture Notes in Computer Science, pages 311--327, Rennes, France, July 2013. Springer. [ DOI ]|
|[Coc12]||David Cock. Verifying probabilistic correctness in Isabelle with pGCL. In Proceedings of the 7th International Conference on Systems Software Verification, volume 102 of Electronic Proceedings in Theoretical Computer Science, pages 167--176. Open Publishing Association, November 2012. [ DOI ]|
|[Coc11]||David Cock. Exploitation as an inference problem. In Proceedings of the 4th ACM Workshop on Artificial Intelligence and Security, pages 105--106. ACM, October 2011. [ DOI ]|
|[Coc10]||David Cock. Lyrebird -- assigning meanings to machines. In Gerwin Klein, Ralf Huuck, and Bastian Schlich, editors, Proceedings of the 5th International Conference on Systems Software Verification, pages 1--9. USENIX, October 2010. [ .pdf ]|
|[KAE+10]||Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an operating system kernel. Communications of the ACM, 53(6):107--115, June 2010. [ DOI ]|
|[KEH+09]||Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pages 207--220. ACM, October 2009. [ DOI ]|
|[WKS+09]||Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, and Michael Norrish. Mind the gap: A verification framework for low-level C. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 500--515, Munich, Germany, August 2009. Springer. [ DOI ]|
|[CKS08]||David Cock, Gerwin Klein, and Thomas Sewell. Secure microkernels, state monads and scalable refinement. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science, pages 167--182. Springer, August 2008. [ DOI ]|
|[Coc08]||David Cock. Bitfields and tagged unions in C: Verification through automatic generation. In Bernhard Beckert and Gerwin Klein, editors, Proceedings of the 5th International Verification Workshop, volume 372 of CEUR Workshop Proceedings, pages 44--55, August 2008. [ .pdf ]|
|[DEK+06]||Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. Running the manual: An approach to high-assurance microkernel development. In Proceedings of the ACM SIGPLAN Haskell Workshop, September 2006. [ DOI ]|