Prosecco: cryptographic protocols in safe custody

Based in Paris since it was created in 2012, the Prosecco team has developed expertise in cryptographic protocols and program verification to contribute to securing applications and hardware peripherals. Led by Karthik Bhargavan, the team now has three permanent and three non-permanent researchers, three post-doctoral researchers, eight PhD students and three research engineers. 

Studying...

"The first aspect of our work involves studying the security properties of protocols, in particular with regard to confidentiality, integrity and authentication," explains Benjamin Beurdouche, one of the PhD students on the team. "To do that, we use two tools developed by the team: ProVerif and CryptoVerif." Created by Bruno Blanchet, senior researcher with Prosecco, they have been used to study numerous protocols, such as Signal which is used by instant messaging systems like WhatsApp or Skype, WireGuard, a new type of VPN which could soon be integrated into the Linux kernel, or the ARINC protocol used to secure communications in civil aviation.

...Implementing…

At the same time, the team is also working on creating programming languages and formal verification tools. "In this respect, our flagship tool is without doubt the F* programming language, developed as part of the Everest project, a partnership between Microsoft Research and Inria. F* is a functional language designed for formal verification, which allows high-assurance C code to be generated whilst reducing the proof effort by using an automated prover." F* is itself at the heart of the development of highly structured projects, such as the miTLSsecurity platform or HACL*, a fast, formally verified cryptolibrary that is secure, correct and without covert channels dedicated to applications such as cryptographic protocols, web browsing or the internet of things. Already in use in the Mozilla Firefox browser, HACL* is also used by Wireguard, the TLS library of Facebook and the Tezos blockchain.

…And creating tomorrow's compilers

Led by Cătălin Hriţcu, the latest research strand conducted by the Prosecco team concerns secure compilation. "Writing high-assurance programs is important, but not enough," emphasises Benjamin Beurdouche. "Although these programs are carefully developed, they run in an ecosystem populated with other programs with which they interact. These external software components sometimes contain bugs, or they may be malicious, and not obliged to obey the rules imposed by the developer. They can therefore cause security flaws by composition. The aim of "secure compilation" is to build a new generation of compilers that guarantee that the security of programs developed in high-level languages is preserved, even in the presence of adversaries."

TLS 1.3, MLS - large-scale projects

"Several of the team's key projects are at the interface of our different areas of research," adds Benjamin Beurdouche, "This is the case, in particular, of the work we did from 2014 to 2018 around the secure web communication protocol, TLS 1.3, which was approved last August by the IETF (Internet Engineering Task Force), one of the Internet standards organisations. We not only studied the security properties of this protocol used by billions of people every day, but also contributed to its design." Recently a project of the same type has started to be set up for MLS (Messaging Layer Security), a secure communication protocol designed for group messaging, also sponsored by the IETF, with the support of web giants like Google, Facebook, Microsoft, Mozilla, etc. "The stakes are huge because group messaging has long been the "poor relation" when it comes to security. For the moment, the reference protocol is Signal, but the way it works, by establishing numerous connections, limits the size of discussion groups. With MLS, the idea is to provide a reliable solution for groups of several thousand people, which would open up a whole range of new possibilities. And this time, Prosecco will not only be a contributor, but actually one of the authors of the future protocol expected to see the light of day within the next two years!" announces Benjamin Beurdouche in conclusion.