About
I am interested in security, privacy, cryptography, programming, and distributed systems. My main project these days is Everest, aiming at building, verifying, and deploying secure components such as miTLS (opens in new tab) for the HTTPS ecosystem. I lead the Constructive Security (opens in new tab)team at Microsoft Research in Cambridge, UK. Since 2006, I also lead a project on Secure Distributed Computations (opens in new tab) at the MSR-INRIA Joint Center, in collaboration with the Prosecco team at INRIA Paris.
My recent research subjects include cryptographically-verifiable computing (opens in new tab) (Pinocchio, Geppetto, Cinderella); TLS security (opens in new tab); secure cloud outsourcing relying on trusted hardware (opens in new tab) (SGX, TPM); resistance against side-channels; models for cryptography; information-flow security; secure multiparty sessions; dependent types, notably for the F* programming language (opens in new tab); JavaScript and TypeScript security; authorization policies; secure logs; secure implementations of communication abstractions; access control for mobile code; concurrency in C# and F#, private authentication; and the verification of cryptographic protocols for Internet security and Web Services security.
I joined Microsoft Research in 1998. Before that, I graduated from Ecole Polytechnique in 1992, worked for a year on deductive databases at BULL, obtained a second engineering degree from Ecole Nationale des Ponts et Chaussées in 1995, then did a PhD in computer science at INRIA Rocquencourt. In my PhD, I applied some concurrency theory to model distributed programming: I proposed a variant of the pi calculus as the core of a distributed programming language. I used this calculus to model the behavior of programs and implementations, in particular agent-based mobility, partial failure, and security. I also wrote the distributed runtime for a prototype implementation of the language.