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

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 in the cloud service provider, or hackers break into the data center, they still should not be able to get access to customer data. Trust model: We use a non-hierarchical trust model. That is, we don’t want…

Verifiable Computing

Established: August 24, 2011

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 than performing the computation itself. In more detail, we introduce and formalize the notion of Verifiable Computation, which enables a computationally weak client to "outsource" the computation of an arbitrary function F on various dynamically-chosen…

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

Established: October 21, 2010

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 allow for privacy-friendly real-time aggregation of smart-meter readings. Information computed on the basis of fine-grained smart-meter readings has multiple uses within the energy industry, including billing, providing energy advice, settlement, forecasting, demand response, and fraud…



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










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











Distributed Key-Manager Verification

December 2010

This package contains the F# and F7 source files to aid in the verification of a distributed key-management system. This new component implements a data-protection API for groups of clients. To enable long-term data protection, it supports cryptographic agility so cryptography algorithms and policies can evolve for protecting fresh data while preserving access to old…

Size: 32 KB

    Click the icon to access this download

  • Website


Events (future, recent, then not so recent)