I am a member of the Systems Research Group at Microsoft Research. My interests include programming languages, operating systems, verification, and security. I am particularly interested in the use of safe programming languages as operating systems, and I have worked to integrate features traditionally associated with operating systems into safe programming language environments.


Checked C

The Checked C research project is investigating how to extend the C programming language so that programmers can write more secure and reliable C programs. The project is developing an extension to C called Checked C that adds checking to C to detect or prevent common programming errors such as buffer overruns, out-of-bounds memory accesses, and incorrect type casts. The extension is designed to be used for existing system software written in C. Finding out…

Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year. Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem. We…


Established: October 2, 2014

An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times. Our specifications, code, proofs, and tools for our projects Ironclad Apps (verifying the…

SymDiff: Differential Program Verifier

Established: October 14, 2010

SymDiff is a tool for performing differential program verification. Differential program verification concerns with specifying and proving interesting properties over program differences, as opposed to the program itself. Such properties include program equivalence, but can also capture more general differential/relational properties. SymDiff provides a specification language to state such differential (two-program) properties using the concept of mutual summaries that can relate procedures from two versions. It also provides proof system for checking such differential specifications…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers…

Experiment 19

Established: October 13, 2008

A skunkworks project in 2008/2009 to re-imagine the OS platform for Windows Phone. The prototype proved that Windows NT and the CLR could deliver better performance than Windows CE and the .NET Compact Framework on identical hardware. Within months of the completion of Experiment 19, Microsoft launched efforts to build what would become Windows Phone 8 and Windows RT for ARM tablets. Re-imagining the Windows Phone Platform In the fall of 2008,…


Established: July 9, 2003

OS and tools for building dependable systems. The Singularity research codebase and design evolved to become the Midori advanced-development OS project. While never reaching commercial release, at one time Midori powered all of Microsoft's natural language search service for the West Coast and Asia. "...it is impossible to predict how a singularity will affect objects in its causal future." - NCSA Cyberia Glossary What's New? The Singularity Research Development Kit (RDK) 2.0 is available for…



Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Beguelin, Jean-Karim Zinzindohoué, in SNAPL 2017, May 2, 2017, View abstract, Download PDF, View external link














Professional Activities