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 for the HTTPS ecosystem. I lead the Constructive Security team at Microsoft Research in Cambridge, UK. Since 2006, I also lead a project on Secure Distributed Computations at the MSR-INRIA Joint Center, in collaboration with the Prosecco team at INRIA Paris.

My recent research subjects include cryptographically-verifiable computing (Pinocchio, Geppetto, Cinderella); TLS security; secure cloud outsourcing relying on trusted hardware (SGX, TPM);  resistance against side-channels; models for cryptography; information-flow security; secure multiparty sessions; dependent types, notably for the F* programming language; 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.


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,…

Trusted Cloud

Established: August 31, 2015

The Trusted Cloud project at Microsoft Research aims to provide customers of cloud computing complete control over their data: no one should be able to access the data without the customer’s permission. Even if there are malicious employees…

Verifiable Computing

Verifiable computation schemes enable a client to outsource the computation of a function F on various inputs to an untrusted worker, and then verify the correctness of the returned results. Critically, the outsourcing and verification procedures must be more efficient…

The F* Project

Established: March 25, 2011

F* is a verification-oriented dialect of ML. For more information, please visit https://fstar-lang.org or click on the logo below.

Privacy-friendly smart metering

Many smart metering proposals threaten users' privacy by disclosing fine-grained consumption data to utilities. We have designed protocols that allow for precise billing of consumption while not revealing any consumption information to third parties. We also have developped protocols that…











Code-Carrying Authorization
Sergio Maffeis, Martín Abadi, Cédric Fournet, Andy Gordon, in 13th European Symposium on Research in Computer Security, Málaga, Spain, October 6-8, 2008. Proceedings, Springer Berlin Heidelberg, October 6, 2008, View abstract, Download PDF





Private Authentication
Martın Abadi, Cédric Fournet, in Theoretical Computer Science 322(3):427--476. September 2004. Special issue on Foundations of Wide Area Network Computing. Parts of this work were presented at PET'02 (LNCS 2482) and ISSS'02 (LNCS 2602), September 1, 2004, View abstract, Download PDF











Events (future, recent, then not so recent)