Lib.rs

伯特尼是使用Rust的子集编写的TLS 1.3的最小化、高保证实现。

它基于以下设计原则

1. 纯函数式：没有可变的数据结构或外部可见的副作用。
2. 易于验证：使用hacspec编写并转换为F*。
3. 简洁且最小化：配置了单个协议版本和加密套件。

Karthikeyan Bhargavan于2021年在Inria首次编写了伯特尼，并于2022年将其转移到Cryspen。它受Apache 2.0许可，但尚未准备好供公众使用。

使用BERTIE

在simple_https_client包中提供了一个使用伯特尼作为底层TLS实现的HTTPS客户端的示例。客户端使用伯特尼检索网页。

您可以通过执行...来尝试它

$ cargo run -p simple_https_client -- google.com

还有一个HTTPS服务器作为simple_https_server可用。

警告：不要在生产环境中使用。这是伯特尼的早期草案，严格处于开发阶段。

如果您正在寻找对伯特尼的商业支持，请联系Crypsen。

在BERTIE上工作

注意：如果您只想构建和运行伯特尼，您不需要做任何这些。这仅适用于您打算在伯特尼上工作，即更改其核心并向项目贡献更改。

请记住，伯特尼是用hacspec编写的--一种更“限制性”的Rust版本，适用于形式化验证。在伯特尼上工作的感觉与在典型的Rust包上工作非常相似，但所有代码都必须根据hacspec有效。因此，您也可能发现一些代码与普通的Rust相比有些“不寻常”。

但别担心！有一个Cargo插件可以验证一切是否符合hacspec规范。只需按照网站上的说明hacspec安装它。然后，将rustup覆盖设置为当前在hacspec repository中使用的通道，即...

rustup override set <channel>

然后，您可以使用以下命令验证您的更改是否符合hacspec规范：cargo clean，cargo build和cargo hacspec。

贡献

要了解我们正在做什么以及正在进行中的工作，您可以关注我们的项目任务。

在贡献之前，请查看贡献指南和行为准则。

项目结构

• .github包含GitHub Actions CI的配置。
• assets包含Bertie项目中使用的非代码文件。
• bogo_shim包含用于针对BoringSSL测试运行器进行测试的BoGo shim应用程序。
• record是一个crate，它提供了在simple_https_client和simple_https_server中使用的常见功能。
• simple_https_client是一个实现Bertie HTTPS客户端的示例crate。
• simple_https_server是一个实现Bertie HTTPS服务器的示例crate。
• src包含Bertie源代码（必须符合hacspec规范。）
• tests包含所有测试。

出版物

Bertie受到许多先前研究工作的启发，包括关于和TLS 1.3的工作。

以下是一些最相关的出版物

• Hacspec：嵌入Rust中的简洁、可执行、可验证的高安全性密码学规范。 Denis Merigoux，Franziskus Kiefer，Karthikeyan Bhargavan。Inria技术报告，2021。hal-03176482
• TLS 1.3标准候选者的验证模型和参考实现。 Karthikeyan Bhargavan，Bruno Blanchet，Nadim Kobeissi。第38届IEEE安全与隐私研讨会，2017。hal-01575920
• 一个混乱的联盟状态：驯服TLS的复合状态机。 Benjamin Beurdouche，Karthikeyan Bhargavan，Antoine Delignat-Lavaud，Cédric Fournet，Markulf Kohlweiss，Alfredo Pironti，Pierre-yves Strub，Jean Karim Zinzindohoue。IEEE安全与隐私研讨会，2015。hal-01114250

许可证

Bertie根据Apache 2.0许可。

致谢

Bertie项目得到Inria和nlnet基金会的支持。