Repository files navigation

Bertie is a minimal, high-assurance implementation of TLS 1.3 written in a subset of Rust calledhacspec.

It is built upon the following design principles:

1. Purely functional: no mutable data structures or externally visible side-effects.
2. Verification friendly: written in hacspec and translates toF*.
3. Succinct and minimal: configured with a single protocol version and cipher suite.

Karthikeyan Bhargavan first authored Bertie at Inria in 2021 and transferred it toCryspen in 2022.It is licensed underApache 2.0 but not yet ready for public consumption.

An example HTTPS client using Bertie is provided in thesimple_https_client crate.The client retrieves a web page using Bertie as the underlying TLS implementation.

You can try it out by executing ...

$ cargo run -p simple_https_client -- google.com

There is also a HTTPS server available assimple_https_server.

WARNING: Do not use in production. This is an early draft of Bertie and strictly work-in-progress.

If you are looking for commercial support for Bertie, pleasereach out to Crypsen.

Note: You do not need to do any of this when you just want to build and run Bertie. This is only if you intend towork on Bertie, i.e., change its core and contribute the changes to the project.

Keep in mind that Bertie is written inhacspec -- a more "restrictive" version of Rust that lends itself to formal verification.Working on Bertie feels a lot like working on a typical Rust crate but all code needs to be valid according to hacspec.Thus, you may also find that some code is "unusual" compared to vanilla Rust.

But no worries!There is a Cargo plugin to verify that everything is valid according to hacspec.Just follow the instructions on thehacspec website to install it.Then, set arustup override to the channel currently used in thehacspec repository, i.e., ...

rustup overrideset<channel>

You can thencargo clean,cargo build, andcargo hacspec to verify that your changes conform to the hacspec specification.

To see what we are working on and what is in the pipeline, you can follow ourproject tasks.

Before contributing, please have a look at thecontributing guidelines and thecode of conduct.

• .github contains the configuration for GitHub Actions CI.
• assets contains non-code files that are used in the Bertie project.
• bogo_shim contains the BoGo shim application that is used for testing against BoringSSL's test runner.
• record is a crate that provides common functionality used insimple_https_client andsimple_https_server.
• simple_https_client is an example crate that implements a Bertie HTTPS client.
• simple_https_server is an example crate that implements a Bertie HTTPS server.
• src contains the Bertie source code (that must be valid according to hacspec.)
• tests contains all tests.

Bertie is inspired by a number of prior research works, including works onhacspec and TLS 1.3.

Some of the most relevant publications are listed below:

• Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust. Denis Merigoux, Franziskus Kiefer, Karthikeyan Bhargavan. Inria Technical Report, 2021.hal-03176482
• Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi. 38th IEEE Symposium on Security and Privacy, 2017.hal-01575920
• A Messy State of the Union: Taming the Composite State Machines of TLS. Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-yves Strub, Jean Karim Zinzindohoue. IEEE Symposium on Security & Privacy, 2015.hal-01114250

Bertie is licensed underApache 2.0.

The Bertie project is supported byInria and thenlnet foundation.