在密码学原语上执行混合执行 - 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. 带有MD5()函数上SANDSHREW_*包装器的示例OpenSSL测试用例。

编写测试用例

我们首先编写并编译一个测试用例，测试单个密码原语或函数与另一个实现的等价性。图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工作是一次很棒的体验，并给了我很多激励去探索和学习安全研究的新颖领域。在行业环境中工作推动我理解困难的概念和想法，我将把这些带到我的大学第一年。

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

页面内容
近期帖子
使用Deptective调查您的依赖项
系好安全带，Buttercup，AIxCC的评分回合正在进行中！
使您的智能合约超越私钥风险成熟
Go解析器中意外的安全陷阱
我们从审查Silence Laboratories的首批DKLs23库中学到了什么
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。