- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
The project aims at securing Internet transactions, by providing formally certified implementations of protocols, to be deployed as replacements of currently used versions. As the past and ongoing work of this project has shown by trying to prove soundness of current deployments, these are in fact unsound and littered with vulnerabilities (eg attacks such as FREAK, LOGJAM,…).
Specific protocols were considered, in particular: TLS, underlying HTTPS. Current certified implementation miTLS developed at Joint Centre has been released in open source format, as a tool for security research (this is the output of one of the first projects started in the Joint Centre). Current work aims to make it as fast as commercial implementations.
The project also works on the elaboration of a toolchain for formal certification: in particular development of F* language and environment (certified compiler), and bridges between F* and commonly used languages, notably Javascript. Specific objectives within this thread are:
Building a verified crypto library (HACL*);
Analysis of other web security protocols.
A final thread consists in the evangelization of methodology and proposed solutions at IETF, to ensure global adoption of Everest approach and releases.
Relevant pointers are:
