密码学原语的混合符号执行分析

在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