We develop techniques and abstractions for building trustworthy computer systems, i.e., systems that are safe and secure. In our work, we:

  • enjoy exploring the fundamental challenges posed to security and safety by large-scale systems consisting of many threads, many nodes, and millions of lines of code written by many programmers
  • seek solutions that solve real-world problems by overcoming theoretical worst-case limitations
  • build prototypes that directly improve the lives of real users and evaluate them on real-world workloads
  • operate at the intersection of operating systems, programming languages, formal methods, and computer architecture

Our work is funded by ERC and Swiss NSF, as well as by generous no-strings-attached gifts from Google, Cyberhaven, Microsoft, Intel, IBM, and VMware.