tlspuffin/tlspuffin

# DY Fuzzing: Formal Dolev-Yao 模型与密码协议模糊测试 [](http://github.com/badges/stability-badges)[](https://github.com/tlspuffin/tlspuffin/actions/workflows/on-pr-merged.yml) ## 什么是 `puffin`？ `puffin` 模糊器是 [Dolev-Yao 模糊方法](https://www.computer.org/csdl/pds/api/csdl/proceedings/download-article/1Ub234bjuWA/pdf)（公开可访问的 eprint [在此](https://eprint.iacr.org/2023/57)）的参考实现。 它旨在对密码协议实现进行模糊测试。目前，它附带了多个 TLS 实现（OpenSSL、BoringSSL、LibreSSL 和 wolfSSL）的测试框架，以及 OpenSSH 的初步测试框架。我们构建 `puffin` 是为了可以添加新的协议和协议实现。 在内部，`puffin` 使用库 [LibAFL](https://aflplus.plus/libafl-book/) 来驱动模糊循环。 我们有时会用 `tlspuffin` 而不是 `puffin` 来命名模糊器和该项目。这是因为我们实现的第一个协议是 TLS。然而，`puffin` 和 DY 模糊方法一般并不局限于 TLS 协议。 ## 构建和使用 `puffin` 请参考最新的 [用户手册](https://tlspuffin.github.io/docs/overview)。 我们还提供了一个 [快速入门指南](https://tlspuffin.github.io/docs/guides/quickstart) 用于快速设置。 ## 许可证 根据以下之一许可： * Apache License, Version 2.0 ([LICENSE-APACHE](LICENSE-APACHE) 或 http://www.apache.org/licenses/LICENSE-2.0) * MIT 许可证 ([LICENSE-MIT](LICENSE-MIT) 或 https://opensource.org/blog/license/mit) 由您自行选择。 请注意，tlspuffin 还包含来自外部项目的代码/修改。更多细节请参见 [THIRD_PARTY](THIRD_PARTY)。 ## DY 模糊方法背景 关键且广泛使用的密码协议反复被发现其设计和实现中存在漏洞。此类漏洞的一个主要类别是 **逻辑攻击**，例如利用协议逻辑缺陷的攻击。 基于 **Dolev-Yao (DY) 攻击者**（下图绿色部分）的自动化形式验证方法形式化定义并擅长发现此类漏洞，但仅在抽象规范模型上操作。对现有协议实现进行完全自动化验证目前仍无法实现。这使得我们无法确定这些实现是否安全。不幸的是，这个盲点隐藏了许多攻击，例如近期针对广泛使用的 TLS 实现因实现错误而引入的逻辑攻击。 ### 检测实现级逻辑攻击的挑战 我们关注在大型密码协议代码库中查找实现级逻辑攻击。为此，我们建立在 **模糊测试** 基础上。然而，现有技术模糊器（图中左侧所示）无法捕捉此类逻辑攻击，主要有两个原因。第一，它们无法有效 **捕获 DY 攻击者**，尤其是 DY 模型中对消息项表示的结构化修改能力（例如使用攻击者控制的密钥重新签名消息），这是捕获逻辑攻击的前提条件。我们强调，逻辑攻击可能触发协议或内存漏洞。第二，它们无法检测 **协议漏洞**，即协议级别的安全违规，例如触发非内存相关的攻击，如认证绕过。 ### DY 模型指导的模糊测试 我们在 [1] 中通过提出一种新颖且有效的技术 **DY 模型指导的模糊测试** 来回答这一问题，该技术能够阻止针对协议实现的逻辑攻击。其主要思想是将抽象 DY 执行集视为可能的测试用例，并使用一种新颖的基于变异的模糊器来探索这个集合（图中中间部分）。DY 模糊器将每个抽象执行具体化，并在被测程序上测试它。这种方法使得可以在形式化项表示的消息上进行更结构化和安全相关的级别推理（例如解密消息并使用不同密钥重新加密），而不是随机位级修改，后者极不可能产生相关的逻辑对抗行为。 The gap filled by DY fuzzing and tlspuffin (shown in the middle). ### 实现 [tlspuffin](https://github.com/tlspuffin/tlspuffin) 是此类 DY 模糊器的参考实现。它被模块化构建，以便可以集成和测试新的协议和被测程序（PUT）。我们已经集成了 TLS 协议以及 OpenSSL、BoringSSL、WolfSSL 和 LibreSSL 的 PUT。tlspuffin 已经发现了 8 个 CVE（参见下表），其中包括五个新漏洞（包括一个关键漏洞），所有漏洞均已得到确认并修补。 有趣的是，正如上述主张所证明的， 这五个新发现的漏洞并未被当前最先进的模糊器 [1] 发现。 | CVE ID | CVSS | 类型 | 是否新颖 | 版本 | |--------------------------------------------------------------------|-----|--------------|-----------------------------------------|---------| | [2021-3449](https://www.cve.org/CVERecord?id=CVE-2021-3449) | 5.9 | Server DoS | ❌ | 1.1.1j | | [2022-25638](https://www.cve.org/CVERecord?id=CVE-2022-25638) | 6.5 | Auth. Bypass | ❌ | 5.1.0 | | [2022-25640](https://www.cve.org/CVERecord?id=CVE-2022-25640) | ️7.5❗ | Auth. Bypass | ❌ | 5.1.0 | | [2022-38152](https://www.cve.org/CVERecord?id=CVE-2022-38152) | 7.5❗ | Server DoS | ✅ | 5.4.0 | | [2022-38153](https://www.cve.org/CVERecord?id=CVE-2022-38153) | 5.9 | Client DoS | ✅ | 5.3.0 | | [2022-39173](https://www.cve.org/CVERecord?id=CVE-2022-39173) | 7.5❗ | Server DoS | ✅ | 5.5.0 | | [2022-42905](https://www.cve.org/CVERecord?id=CVE-2022-42905) | 9.1❗ | Info. Leak | ✅ | 5.5.0 | | [2023-6936](https://www.cve.org/CVERecord?id=CVE-2023-6936) | 5.3 | Info. Leak | ✅ | 5.6.6 | 一些特性： * 使用 [LibAFL 模糊框架](https://github.com/AFLplusplus/LibAFL) * 模糊器受 [Dolev-Yao 模型](https://en.wikipedia.org/wiki/Dolev%E2%80%93Yao_model) 启发，用于协议验证 * 针对协议模糊测试的领域特定变异器 * 被测库支持： * OpenSSL 1.0.1f, 1.0.2u, 1.1.1k * LibreSSL 3.3.3 * wolfSSL 5.1.0 - 5.4.0 * BoringSSL（最后测试提交 368d0d87d0bd00f8227f74ce18e8e4384eaf6afa） - 免责声明：使用 asan 在调试模式下构建时存在一个 bug（可通过在 `Cargo.toml` 中设置 `lto=true` 规避） * 对每个 LUT 可重现。我们使用供应商库的新鲜 git 克隆源代码。 * 70% 测试覆盖率 * 使用 Rust 编写！ ## 团队 活跃成员： - [Tom Gouville](https://github.com/aeyno) - 博士生 - [Loria](https://www.loria.fr), [Inria](https://www.inria.fr) - [Lucca Hirschi](https://members.loria.fr/LHirschi/) - 研究员 - [Loria](https://www.loria.fr), [Inria](https://www.inria.fr) - [Steve Kremer](https://members.loria.fr/SKremer/) - 高级研究员 - [Loria](https://www.loria.fr), [Inria](https://www.inria.fr) - [Olivier Demengeon](https://sed-nge.inria.fr/team/olivierd/index.html) - 研究工程师 - [Loria](https://www.loria.fr), [Inria](https://www.inria.fr) - [Nataël Baffou](https://github.com/nataelbaffou) - 研究工程师 - [Loria](https://www.loria.fr), [Inria](https://www.inria.fr) 曾参与贡献： - [Max Ammann](https://github.com/maxammann) - 硕士/安全工程师 - [Trails of Bits](https://www.trailofbits.com/) - [Michael Mera](https://github.com/michaelmera) - 研究工程师 - [Loriahttps://www.loria.fr), [Inria](https://www.inria.fr) 当时 ## 参考文献 [1] [M. Ammann, L. Hirschi and S. Kremer, "DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing," in 2024 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2024 pp. 99-99.](https://www.computer.org/csdl/pds/api/csdl/proceedings/download-article/1Ub234bjuWA/pdf) [2] [DY Fuzzing Poster](https://tlspuffin.github.io/assets/files/SP24_Poster-f90cdd5b2df492a64fa18089c98a7b2e.pdf)

标签：BoringSSL, Dolev-Yao模型, DY Fuzzing, Fuzzing, LibAFL, LibreSSL, OpenSSH, OpenSSL, TLS, tlspuffin, wolfSSL, 加密协议, 协议实现, 可视化界面, 安全测试, 密码协议, 底层编程, 形式化验证, 攻击性安全, 通知系统, 防御工具