Send in your ideas. Deadline October 1, 2024
Source code :
Theme fund: NGI Assure
Start: 2022-02
End: 2024-04
More projects like this
Software engineering


Formally verified TLS 1.3 implementation

The security of the Web ecosystem relies crucially on Transport Layer Security (TLS) protocol, but despite years of study, cryptographic weaknesses and implementation bugs in TLS implementations continue to be found on a regular basis. Bertie is a high-assurance TLS 1.3 implementation written in a subset of Rust called hacspec. Bertie uses the formally verified HACL* cryptographic library and its protocol code can be verified using the F* framework. Hence, it offers strong guarantees from the crypto layer up to the protocol API. The funding from NLnet will be used to stabilise Bertie, add documentation and tests, improve its performance, maintain its proofs, and set it up as an open source project with best practices and long-term software support.

Run by Cryspen SARL

Logo NLnet: abstract logo of four people seen from above Logo NGI Assure: letterlogo shaped like a tag

This project was funded through the NGI Assure Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 957073.