https://github.com/cryspen/bertie Skip to content Toggle navigation Sign in * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions For + Enterprise + Teams + Startups + Education By Solution + CI/CD & Automation + DevOps + DevSecOps Resources + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} cryspen / bertie Public * Notifications * Fork 2 * Star 79 * Bertie TLS 1.3 Implementation License Apache-2.0 license 79 stars 2 forks Branches Tags Activity Star Notifications * Code * Issues 22 * Pull requests 2 * Discussions * Actions * Projects 1 * Security * Insights Additional navigation options * Code * Issues * Pull requests * Discussions * Actions * Projects * Security * Insights cryspen/bertie This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. main BranchesTags Go to file Code Folders and files Last commit Last Name Name message commit date Latest commit History 232 Commits .github .github assets assets benches benches bogo_shim bogo_shim integration_tests integration_tests proofs proofs record record simple_https_client simple_https_client simple_https_server simple_https_server src src test_certs test_certs tests tests util util .gitignore .gitignore Benchmarks.md Benchmarks.md CHANGELOG.md CHANGELOG.md CLA.md CLA.md CODEOWNERS CODEOWNERS CODE_OF_CONDUCT.md CODE_OF_CONDUCT.md CONTRIBUTING.md CONTRIBUTING.md Cargo.toml Cargo.toml LICENSE LICENSE README.md README.md SECURITY.md SECURITY.md deny.toml deny.toml flamegraph.svg flamegraph.svg hax-driver.py hax-driver.py libcrux.fst.config.json libcrux.fst.config.json View all files Repository files navigation * README * Code of conduct * Apache-2.0 license * Security [bertie-logo] CI Scheduled Bertie is a minimal, high-assurance implementation of TLS 1.3 written in a subset of Rust called hacspec. 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 to F*. 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 to Cryspen in 2022. It is licensed under Apache 2.0 but not yet ready for public consumption. USING BERTIE An example HTTPS client using Bertie is provided in the simple_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 as simple_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, please reach out to Crypsen. WORKING ON BERTIE 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 to work on Bertie, i.e., change its core and contribute the changes to the project. Keep in mind that Bertie is written in hacspec -- 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 the hacspec website to install it. Then, set a rustup override to the channel currently used in the hacspec repository, i.e., ... rustup override set You can then cargo clean, cargo build, and cargo hacspec to verify that your changes conform to the hacspec specification. CONTRIBUTING To see what we are working on and what is in the pipeline, you can follow our project tasks. Before contributing, please have a look at the contributing guidelines and the code of conduct. PROJECT STRUCTURE * .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 in simple_https_client and simple_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. PUBLICATIONS Bertie is inspired by a number of prior research works, including works on hacspec 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, Cedric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-yves Strub, Jean Karim Zinzindohoue. IEEE Symposium on Security & Privacy, 2015. hal-01114250 LICENSE Bertie is licensed under Apache 2.0. ACKNOWLEDGEMENTS The Bertie project is supported by Inria and the nlnet foundation. About Bertie TLS 1.3 Implementation Resources Readme License Apache-2.0 license Code of conduct Code of conduct Security policy Security policy Activity Custom properties Stars 79 stars Watchers 7 watching Forks 2 forks Report repository Releases 1 tags Packages 0 No packages published Contributors 7 * @franziskuskiefer * @duesee * @karthikbhargavan * @jschneider-bensch * @jallmann * @W95Psp * @dependabot[bot] Languages * F* 62.5% * Rust 35.9% * Other 1.6% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.