对密码学原语执行混合执行分析 - 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工作是一次很棒的体验，并给了我很多激励去探索和学习安全研究的新兴领域。在行业环境中工作推动我理解困难的概念和想法，我将把这些带到大学的第一年。

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

页面内容
玩转密码验证
介绍Sandshrew
编写测试用例
执行具体化
恢复符号状态
结果
局限性
结论
致谢

近期文章
非传统创新者奖学金
劫持您的PajaMAS中的多代理系统
我们构建了MCP始终需要的安全层
利用废弃硬件中的零日漏洞
Inside EthCC[8]：成为智能合约审计员

密码学原语的混合执行分析：Sandshrew工具实战解析

本文介绍基于Manticore的混合执行工具Sandshrew，通过结合符号执行与具体执行分析密码学原语，实现等价性验证与漏洞发现，探讨其在密码学实现验证中的技术架构与局限性。