在形式化验证工具中寻找遗漏警报漏洞

# 在形式验证工具中寻找遗漏报警缺陷——学术中的嵌入式研究 来源：https://blog.regehr.org/archives/2124 \[本文与 Vsevolod Livinskii 共同撰写。\] 形式验证并非洒在计算机系统上的神奇魔法粉尘。真正的形式验证涉及大量与其他系统级工作相同的艰难、繁重且技术性工程工作。此外，验证工具本身也极难做到正确。它们可能受到多种缺陷的影响，甚至可能比其他软件更难以调试。如果我们需要信任这些工具，就必须对其进行严格测试。 Alive2 是一个翻译验证工具（https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf）：给定 LLVM IR 中函数的两个版本——通常对应于优化前后的代码——Alive2 会尝试证明该优化是正确的，或者证明它是错误的。Alive2 在实践中被编译器工程师使用：超过 600 个 LLVM 问题（https://github.com/llvm/llvm-project/issues?q=is%3Aissue+alive2.llvm.org）链接到我们的在线 Alive2 实例（https://alive2.llvm.org/ce/）。 忽略崩溃等情况，我们可以将 Alive2 中的缺陷大致分为两类： - 误报：当没有错误时，Alive2 发出错误信号。 - 漏报：当存在错误时，Alive2 未能发出错误信号。 第一类错误（误报）相对容易测试：我们只需让 Alive2 验证大量优化，并仔细检查它发出的错误信号。每个此类错误都是 LLVM 或 Alive2 中 bug 的结果。第二类错误（即左下象限的那些）则要难测试得多： 我们缺少的是可能触发漏报缺陷的测试用例：每个此类测试都需要一对具有相同签名的 LLVM IR 函数，但可以证明它们对至少一种输入选择的行为不同。我们不能依赖编译器 bug 来创建这些测试用例，因为 LLVM 并不是一个 bug 很多的编译器！它执行的绝大多数优化都是正确的。 为了寻找漏报缺陷，我们尝试了两种不同的思路。在本文的其余部分，我们将对两者进行描述。 首先，我们从 YARPGen（https://github.com/intel/yarpgen）入手，这是一个随机程序生成器，曾用于发现大量编译器缺陷。YARPGen 提供的关键保证是它生成的 C 或 C++ 函数没有未定义行为。没有这个保证，我们就无法真正进行随机化差异测试，因为不同的编译器倾向于以不同的方式利用未定义行为。然而，这个保证本身不足以用来寻找漏报缺陷，因此我们修改了 YARPGen 以适应我们的目的。我们修改后的版本像往常一样生成一个随机函数，然后做了一件新的事情：它在保持新函数同样没有未定义行为的保证下，对该函数进行微小的随机变异。 现在我们得到了两个非常相似且都保证没有未定义行为的函数。这能否作为寻找漏报缺陷的基础？还不够——我们仍然需要确保这些函数在执行时至少对一组输入产生不同的结果。为此，我们只需编译并运行函数对，丢弃那些变异恰好未改变可观察行为的对。最后，我们将函数对编译成 LLVM IR，然后让 Alive2 查看其中一个是否精化（refines）另一个。根据构造，此检查必须失败——如果 Alive2 未发出错误信号，那么我们就发现了我们最初寻找的 Alive2 中的那类漏报缺陷。 我们寻找漏报缺陷的另一种方法是偶然发现的。我们意识到郑阳的 LLVM 超级优化器 Minotaur 在每次使用时，本质上都在被动地寻找漏报缺陷。这里是 Minotaur（https://github.com/minotaur-toolkit/minotaur）的源代码，以及一篇相关论文（https://users.cs.utah.edu/~regehr/minotaur.pdf）。 对于正在优化的程序中的每条 LLVM 指令，Minotaur 都会尝试找到一种更低成本的计算方式。它通过提取该指令及其部分向后数据、控制和内存依赖关系到一个新的 LLVM 函数中来实现这一点，该新函数返回目标指令计算的值。这个新函数作为一个程序综合问题的*规范*，目标是找到一种更低成本的方式来计算该规范。Minotaur 使用 Alive2 确保新函数精化旧函数，并使用 llvm-mca（https://llvm.org/docs/CommandGuide/llvm-mca.html）确保新函数的计算成本低于旧函数。 综合过程通过枚举大量*部分符号化*候选程序来工作，其中指令被具体表示，但字面常量被符号化表示。郑阳修改了 Alive2，使得当一个候选程序包含至少一个符号常量时，它会发出一个存在-全称求解器查询，询问求解器：“是否存在候选程序中符号常量的取值，使得该候选程序精化规范？” Minotaur 综合过程的细节并不太重要；关键点是由于存在大量的候选程序，其中绝大多数并不精化规范，最终我们给了 Alive2 许多次漏掉报警的机会。 但是，如果 Alive2 在被 Minotaur 调用时漏掉了报警，我们如何得知呢？请注意，漏报意味着 Alive2 声称一个候选程序精化了规范，而实际上并不存在精化关系。由于精化是优化器的正确性标准，这些失败按定义会导致错误编译。由于我们经常使用 Minotaur 编译大型开源程序并运行其测试套件，我们应该有相当大的机会发现它引入的任何错误编译。 我们考察了两种不同的方法，一种使用随机搜索，另一种使用小规模穷举搜索，来寻找 Alive2 中的漏报缺陷。到目前为止我们发现了什么？不多！看起来 Alive2 和 Z3 并不习惯于漏报。这意味着它实现了其顶层设计目标，这是好事，因为人们在实践中确实依赖 Alive2。 那么，故事到此结束了吗？我们现在可以确定 Alive2 不会漏报了吗？唉，并不，我们不确定。我猜想，如果我们真的想找到漏报缺陷，应该关注 Alive2 对函数属性和类似构造的支持，而 YARPGen 和 Minotaur 都没有以有趣的方式对这些方面进行压力测试。