在密码学原语上执行混合符号执行

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
编写测试用例
执行具体化
恢复符号状态
结果
限制
结论
感谢
最近帖子
我们构建了MCP始终需要的安全层
利用废弃硬件中的零日漏洞
Inside EthCC[8]：成为智能合约审计员
使用Vendetect大规模检测代码复制
构建安全消息传递很难：对Bitchat安全辩论的细致看法
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。