EPI Prosecco: high assurance cryptography for Mozilla Firefox
This summer Inria's Prosecco team worked in collaboration with Mozilla, the company that created the Firefox web browser, to integrate high assurance cryptography into its networking library NSS.
Originally, the HACL* project is a joint effort between people from the Inria Prosecco team and Project Everest (CMU, INRIA, Microsoft Research) to produce a High Assurance Cryptographic Library
written in the F* formal verification language and generating C through a compiler called KreMLin.
The global idea behind this partnership is to leverage state-of-the-art techniques from academic research to benefit real world products such as Firefox. These techniques allow to get rid of large classes of bugs such as memory safety-related issues, functional correctness issues and some side channel attacks.
The development (“Nightly”) version of Firefox now contains verified code for the Curve25519 elliptic curve, implemented and verified in HACL* by Jean-Karim Zinzindohoué as part of his Ph.D at INRIA.
Curve25519 is a modern curve that is used for key establishment in many important security protocols such as TLS. This is only the first step; we plan to keep working with Mozilla to transfer more verified cryptography from HACL* into Firefox.
Source : blog Mozilla Firefox