I'm a researcher in the Systems Group at Microsoft Research Redmond. My research interests include operating systems, systems security, and distributed systems. I'm particularly interested in problems driven by hardware evolution, or close to the hardware/software boundary.
I completed my BE (2002) and PhD (2007) in the School of Computer Science and Engineering, University of New South Wales, in the research group that evolved into Trustworthy Systems @ Data61. I then spent three years as a postdoctoral researcher in the Systems Group at ETH Zurich, before moving to "sunny" Redmond at the end of 2010.
In Komodo, we showed how to achieve SGX-like security for isolating secure 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.
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 to support lightweight interposition of extensions that are independent of both host and guest. Haven exploits this ability, along with new hardware extensions (Intel SGX), to shield unmodified applications from an untrusted cloud 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.
In the distant past, I also worked on microkernels, single-address-space operating systems, and dynamic updates (kernel patches) to a running OS.
- Andrew Ferraiuolo (2016) formalised and verified much of Komodo
- Sai Deep Tetali (2014) ported Ironclad apps to run in an SGX enclave
- Mihir Nanavati (2013) prototyped support for multiple address spaces in Drawbridge
- Dongyoon Lee (2012) created a prototype Linux LibOS for Drawbridge
- Pedro Fonseca (2011) helped bring up Drawbridge on Barrelfish, including checkpointing support
- ASPLOS’18 program committee
- EuroSys’17 program committee
- OSDI’16 program committee
- SOSP’15 program committee
- SYSTOR’15 program committee and keynote speaker
- ASPLOS’15 program committee
- EuroSys’15 sponsorship chair
- ICDCS’14 program committee
- Conference on Timely Results in Operating Systems (TRIOS) program committee
- 5th Workshop on Hot Topics in Software Upgrades (HotSWUp’13) program committee
- 3rd Workshop on Systems for Future Multicore Architectures (SFMA’13) program committee
- EuroSys’11 program committee
- HotOS’11 program committee
- 2010 USENIX Annual Technical conference program committee
- 2010 ACM/IEEE Symposium on Architectures for Networking and Communications Systems program committee
- ICDCS 2010 Data Management and Data Centers track program committee
- 2nd Workshop on I/O Virtualization (WIOV ’10) program committee
- 2009 EuroSys Doctoral Workshop organiser
- Autumn 2014: PMP Operating Systems, with Simon Peter
At ETH Zurich, with Timothy Roscoe:
- Autumn 2010: Advanced Operating Systems
- Spring 2010: Lions’ Commentary on 6th Edition UNIX Seminar
- Autumn 2009: Advanced Operating Systems
- Spring 2009: Advanced Operating Systems
- Autumn 2008: Data Processing Architectures for New Hardware Platforms Seminar
- Spring 2008: Advanced Operating Systems
- Autumn 2007: Advanced Topics in OS Kernel Design Seminar