As a member of the Systems Group at Microsoft Research Redmond, I design and build software systems, often from scratch, to solve new problems. My research interests are operating systems and systems security, with a particular focus on problems driven by hardware evolution, or close to the hardware/software boundary. Most recently, I have built confidential computing systems that protect the confidentiality and integrity of user computations in shared infrastructure even against untrusted hosts and malicious administrators.
Please see my personal homepage for more information.
Selected Research Projects
Drawbridge & Haven
Much of my work at MSR has been connected to Drawbridge, a new form of virtualization for application sandboxing based on a library OS version of Windows. As reported in the Bascule paper, we generalised the architecture to permit other guest and host operating systems (including Barrelfish and Linux), and to support lightweight interposition of extensions that are independent of both host and guest. This became the basis of Microsoft SQL Server for Linux.
In the Haven project, we introduced the notion of shielded execution: running existing, unmodified applications, while protecting them from an untrusted cloud host. Haven leverages Intel SGX: a hardware implementation of secure enclaves backed by encrypted memory. A significant outcome of Haven was the joint development with Intel of extensions to the SGX ISA to enable dynamic memory management and shielded execution of unmodified binaries.
In Komodo, we showed how to achieve SGX-like security for isolating enclaves from an untrusted OS without baking the entire isolation mechanism into the instruction set. Komodo decouples the core hardware mechanisms such as memory encryption, address-space isolation and attestation from the management thereof, which is delegated to a privileged software monitor that in turn implements enclaves. We formally-verified the implementation of a prototype monitor for ARM TrustZone.
SGX suffers from a number of unique side-channel attacks that stem from the use of an untrusted host OS to manage enclave resources, virtual memory in particular. These “controlled channel” attacks are particularly devastating, and have resisted effective mitigation (several prior research efforts notwithstanding), because they are architectural: the leak is deterministic, noise-free, and guaranteed by the architecture specification. In Autarky, we proposed an incremental, cost-effective, and deployable change to the SGX ISA to close this channel. Autarky leverages the old idea of user-level self-paging to support demand-paging efficiently in trusted code, removing it from the realm of the untrusted host.
I was a founding member of the Barrelfish project, which is exploring how to structure an OS for future multi- and many-core systems. I led this project for its first three years as a postdoc at ETH Zurich, working with Timothy Roscoe and some talented students. Together with collaborators at MSR, we built an OS from scratch to exploit our observation that modern computers are increasingly structured as distributed systems, by mirroring that structure in the OS. For example, we used an asynchronous message-passing abstraction for all inter-core communication, rather than assuming shared memory. Today Barrelfish is a substantial prototype OS, and is still under active research and development.