对密码学原语执行混合执行分析 - Trail of Bits 博客

Alan Cao

2019 年 4 月 1 日

密码学, 实习项目, Manticore, 程序分析

在 Trail of Bits 的冬季和春季实习期间，我研究了密码学协议符号执行的新技术。分析了密码学库中的各种实现级漏洞，并构建了一个基于 Manticore 的混合单元测试工具原型 Sandshrew，该工具在符号和具体环境下分析 C 语言密码学原语。

Sandshrew 是密码开发人员为其实现轻松创建强大单元测试用例的第一步，得到了符号执行进展的支持。虽然它可作为发现漏洞的安全工具，也可作为密码学验证的框架。

密码学验证实践

在选择和实施密码学时，我们的信任应在于实现是否经过形式化验证。这至关重要，因为密码实现经常引入新类别的漏洞（如大数漏洞），这些漏洞可能概率性出现。因此，通过确保验证，我们也在确保实现的功能正确性。

有几种方法可以检查密码学验证：

• 传统模糊测试：可使用 AFL 和 libFuzzer 等模糊测试工具。这对覆盖率不是最优的，因为找到更深层次的漏洞需要时间。此外，由于它们是随机工具，它们不完全是“形式化验证”，而更多是其随机近似。

• 提取模型抽象：可将源代码提升为可被证明语言验证的密码学模型。这需要学习纯学术工具和语言，并具有可靠的翻译。

• 直接使用已验证的实现！与其尝试证明我们的代码，不如使用已经形式化验证的内容，如 Project Everest 的 HACL 库。这在设计协议和应用时剥夺了可配置性，因为我们仅限于库提供的功能（即 HACL 未实现比特币的 secp256k1 曲线）。

符号执行如何？

由于其能够穷尽探索程序中的所有路径，使用符号执行分析密码学库可能非常有益。它可以高效发现漏洞、保证覆盖率并确保验证。然而，这仍然是一个巨大的研究领域，仅产生了少量可工作的实现。

为什么？因为密码学原语通常依赖于符号执行引擎可能无法模拟的属性。这可能包括使用伪随机源和平台特定的优化汇编指令。这些导致传递给引擎的复杂 SMT 查询，造成路径爆炸和运行时显著减慢。

一种解决方法是使用混合执行。混合执行混合符号和具体执行，其中部分代码执行可以“具体化”，或在没有符号执行器的情况下运行。我们利用这种具体化能力来最大化代码路径的覆盖率而无需 SMT 超时，使其成为处理密码验证的可行策略。

介绍 Sandshrew

意识到密码符号执行的缺点后，我决定编写一个原型混合单元测试工具 Sandshrew。Sandshrew 通过小型 C 测试用例检查目标未验证实现与基准验证实现之间的等价性来验证密码学。然后使用 Manticore 和 Unicorn 通过混合执行分析这些用例，以符号和具体方式执行指令。

图 1. 示例 OpenSSL 测试用例，在 MD5()函数上使用 SANDSHREW_*包装器。

编写测试用例

我们首先编写并编译一个测试用例，测试单个密码学原语或函数与另一个实现的等价性。图 1 所示的示例通过为 OpenSSL 的 MD5()函数实现 libFuzzer 风格的包装器来测试明文输入的哈希碰撞。包装器向 Sandshrew 表明它们包装的原语应在分析期间具体化。

执行具体化

Sandshrew 通过强大的 Manticore 二进制 API 利用符号环境。我实现了 manticore.resolve()功能用于 ELF 符号解析，并用它从测试用例二进制的 GOT/PLT 确定用户编写的 SANDSHREW_*函数的内存位置。

图 2. 使用 Manticore 的 UnicornEmulator 功能具体化对目标密码原语的调用指令。

一旦 Manticore 解析出包装函数，钩子就会附加到二进制中的目标密码原语以进行具体化。如图 2 所示，我们然后利用 Manticore 的 Unicorn 后备指令模拟器 UnicornEmulator 来模拟对密码原语进行的调用指令。UnicornEmulator 在当前状态中具体化符号输入，在 Unicorn 下执行指令，并将修改后的寄存器存储回 Manticore 状态。

一切似乎都很顺利，但有一个问题：如果所有符号输入都被具体化了，那么在调用指令具体化之后将解决什么？

恢复符号状态

在程序测试实现等价性之前，我们引入一个无约束的符号变量作为具体化函数的返回输出。该变量保证一个新的符号输入继续驱动执行，但不包含先前收集的约束。

Mathy Vanhoef（2018）采用这种方法分析 WPA2 协议上的密码协议。我们这样做是为了避免由于复杂 SMT 查询导致的超时问题。

图 3. 具体化后将新的无约束符号值写入内存。

如图 3 所示，这是通过 SANDSHREW_*符号处的 concrete_checker 钩子实现的，如果钩子检测到有符号输入传递给包装器，则执行无约束的重新符号化。

一旦符号状态恢复，Sandshrew 就能够继续使用 Manticore 进行符号执行，在到达程序的等价检查部分时进行分叉，并生成求解器解决方案。

结果

以下是 Sandshrew 对先前示例 MD5 哈希碰撞程序执行分析的情况：

Sandshrew 的原型实现目前存在于此。随附一套测试用例，检查一些真实世界实现库及其实现的原始之间的等价性。

局限性

Sandshrew 拥有一个可观的关键密码原语测试套件。然而，分析仍然在许多测试用例中卡住。这可能是因为需要探索符号输入的大状态空间。到达解决方案是概率性的，因为 Manticore z3 接口经常超时。

由此，我们可以确定未来几个改进领域：

• 添加支持允许用户在符号执行前提供具体输入集进行检查。使用适当的输入生成器（如 radamsa），这可能将 Sandshrew 混合成一个模糊器。

• 为常见密码操作实现 Manticore 函数模型。这可以提高分析期间的性能，并允许我们在 Dolev-Yao 验证模型下正确模拟执行。

• 使用机会状态合并减少不必要的代码分支。

结论

Sandshrew 是解决密码验证问题的一种有趣方法，并展示了 Manticore API 的高效创建安全测试工具的强大功能。虽然它仍然是原型实现和实验性的，但我们邀请您为其开发做出贡献，无论是通过优化还是新的示例测试用例。

致谢

在 Trail of Bits 工作是一次极好的经历，并给了我很多激励去探索和学习安全研究的新兴领域。在行业环境中工作推动我理解困难的概念和想法，我将把这些带到大学的第一年。

如果您喜欢这篇文章，请分享：TwitterLinkedInGitHubMastodonHacker News

页面内容

密码学验证实践

介绍 Sandshrew

编写测试用例

执行具体化

恢复符号状态

结果

局限性

结论

致谢

近期文章

非传统创新者奖学金

劫持您的 PajaMAS 中的多代理系统

我们构建了 MCP 一直需要的安全层

利用废弃硬件中的零日漏洞

Inside EthCC[8]：成为智能合约审计员

© 2025 Trail of Bits.

使用 Hugo 和 Mainroad 主题生成。更多精彩内容 请关注我的个人公众号 公众号（办公 AI 智能小助手）公众号二维码

办公AI智能小助手