PDFSAGE：用于安全测试的白盒模糊测试
SAGE 在微软产生了显著的影响。
Patrice Godefroid, Michael Y. Levin, David Molnar, 微软
大多数的读者可能会认为“程序验证研究”主要偏理论，对现实世界影响甚微。请重新思考。如果您正在一台运行某种 Windows 系统的 PC 上阅读这些文字（像 93% 以上的 PC 用户一样，也就是超过十亿人），那么您已经受到了这项工作的影响——在您不知情的情况下，这正是我们希望达到的效果。
安全漏洞的高昂代价
每个月第二个星期二，也被称为“补丁星期二”，微软都会发布一份安全公告列表以及相关的安全补丁，以部署到全球数亿台机器上。每个安全公告都会给微软及其用户带来数百万美元的损失。如果每月的安全更新仅在电费或生产力损失方面花费您 0.001 美元（十分之一美分），那么这个数字乘以十亿人就是 100 万美元。当然，如果恶意软件在您的机器上传播，可能泄露您的一些私人数据，那么这可能会给您带来远高于 0.001 美元的损失。这就是为什么我们强烈建议您应用那些烦人的安全更新。
许多安全漏洞是由于解析通过互联网传输的文件和数据包的代码中的编程错误造成的。例如，Microsoft Windows 包括数百种文件格式的解析器。
如果您正在电脑上阅读这篇文章，那么图 1 中显示的图片会在您的屏幕上显示，这是在 jpg 解析器（通常是您操作系统的一部分）读取图像数据、解码、使用解码后的数据创建新的数据结构，并将这些数据传递给您电脑中的显卡之后发生的。如果实现该 jpg 解析器的代码包含一个错误，例如缓冲区溢出，该溢出可以由损坏的 jpg 图像触发，那么在您的计算机上执行此 jpg 解析器可能会被劫持以执行其他代码，这些代码可能是恶意的并隐藏在 jpg 数据本身中。
这只是一个可能的安全漏洞和攻击场景的例子。本文余下部分讨论的安全漏洞主要都是缓冲区溢出。
寻找“百万美元”漏洞
如今，黑客使用两种主要方法在软件产品中发现安全漏洞。第一种是二进制文件的代码检查（使用好的反汇编器，二进制代码就像源代码）。
第二种是黑盒模糊测试，这是一种黑盒随机测试的形式，它随机地变异格式良好的程序输入，然后用这些修改后的输入测试程序，3 希望触发诸如缓冲区溢出之类的错误。在某些情况下，语法被用来生成格式良好的输入。这也允许编码特定于应用程序的知识和测试生成启发式方法。
黑盒模糊测试是一种简单但有效的技术，用于发现软件中的安全漏洞。已经通过这种方式发现了数千个安全错误。在微软，根据安全开发生命周期7 中的规定，对每个产品的每个不受信任的接口都必须进行模糊测试，该生命周期记录了关于如何开发安全软件的建议。
尽管黑盒模糊测试可能非常有效，但其局限性是众所周知的。例如，then条件语句的分支在
int foo(int x) { // x 是一个输入
int y = x + 3;
if (y == 13) abort(); // 错误
return 0;
}
中只有 232 分之一的机会被执行，如果输入变量x具有随机选择的 32 位值。这直观地解释了为什么黑盒模糊测试通常提供较低的代码覆盖率，并且可能会遗漏安全错误。
介绍白盒模糊测试
几年前，我们开始开发一种替代黑盒模糊测试的方法，称为白盒模糊测试。5 它建立在系统动态测试生成4 的最新进展之上，并将其范围从单元测试扩展到整个程序的安全测试。
从格式良好的输入开始，白盒模糊测试包括符号化地动态执行被测程序，收集来自沿执行路径遇到的条件分支的关于输入的约束。然后系统地否定收集到的约束，并使用约束求解器求解，其解决方案被映射到新的输入，这些输入执行不同的程序执行路径。这个过程使用新颖的搜索技术重复进行，这些技术试图遍历程序的所有（实际上是许多）可行执行路径，同时使用运行时检查器（例如 Purify、Valgrind 或 AppVerifier）同时检查许多属性。
例如，对于输入变量的初始值 0，符号化执行之前的程序片段x采取else条件语句的分支，并生成路径约束x+3 ≠ 13。一旦这个约束被否定并求解，它产生x = 10，提供了一个新的输入，使程序遵循then条件语句的分支。这使我们能够执行和测试额外的代码以查找安全错误，即使没有关于输入格式的特定知识。此外，这种方法自动发现和测试“角落情况”，在这些情况下，程序员可能无法正确分配内存或操作缓冲区，从而导致安全漏洞。
理论上，系统动态测试生成可以导致完整的程序路径覆盖率，即程序验证。然而，在实践中，搜索通常是不完整的，这既是因为被测程序中的执行路径数量巨大，也是因为符号执行、约束生成和约束求解可能由于复杂的程序语句（指针操作、浮点运算等）、对外部操作系统和库函数的调用以及大量无法在合理的时间内完美求解的约束而变得不精确。因此，我们不得不探索实际的权衡。
SAGE
白盒模糊测试首先在 SAGE (Scalable Automated Guided Execution，可扩展的自动化引导执行) 中实现。5 由于 SAGE 针对大型应用程序，其中单次执行可能包含数亿条指令，因此符号执行是其最慢的组件。因此，SAGE 实现了一种新颖的定向搜索算法，称为世代搜索，该算法最大限度地提高了从每次符号执行中生成的新输入测试的数量。给定一个路径约束，所有该路径中的约束都将被系统地逐个否定，与导致它的路径约束前缀结合，并尝试由约束求解器求解。这样，单次符号执行可以生成数千个新测试。（相比之下，标准的深度优先或广度优先搜索将仅否定每个路径约束中的最后一个或第一个约束，并且每次符号执行最多生成一个新测试。）
图 2 所示的程序接受四个字节作为输入，当变量的值cnt大于或等于四时会包含一个错误。从一些初始输入good开始，SAGE 在动态执行符号执行的同时运行此程序。由于此第一次运行期间采取的程序路径由程序中的所有else分支形成，因此此初始运行的路径约束是约束的合取i0 ≠ b, i1 ≠ a, i2 ≠ d和i3 ≠ !。这些约束中的每一个都逐个被否定，与导致它的路径约束前缀结合，然后用约束求解器求解。在这种情况下，所有四个约束都是可解的，从而产生四个新的测试输入。图 2 还显示了函数top的所有可行程序路径的集合。最左边的路径代表程序的初始运行，并标记为第 0 代的 0。通过系统地否定和求解第 0 代路径约束中的每个约束，获得四个第 1 代输入。通过重复此过程，最终枚举此示例的所有路径。在实践中，搜索通常是不完整的。
SAGE 是第一个在 x86 二进制级别执行动态符号执行的工具。它是在跟踪重放基础设施 TruScan8 之上实现的，TruScan 使用 iDNA 框架1 生成的跟踪文件，并虚拟地重新执行记录的运行。TruScan 提供了几个大大简化符号执行的功能，包括指令解码、提供程序符号信息的接口、监视各种输入/输出系统调用、跟踪堆和栈帧分配以及跟踪数据通过程序结构的流动。由于离线跟踪，SAGE 中的约束生成是完全确定性的，因为它使用执行跟踪，该执行跟踪捕获记录运行期间遇到的所有非确定性事件的结果。在 x86 二进制级别工作使 SAGE 可以用于任何程序，而不管其源语言或构建过程如何。它还确保了“您模糊测试的内容就是您交付的内容，” 因为编译器可以执行可能影响安全性的源代码更改。
SAGE 使用了几种对于处理庞大的执行跟踪至关重要的优化。例如，对具有 45,000 个输入字节的 Excel 进行单次符号执行会执行近 10 亿条 x86 指令。为了扩展到如此大的执行跟踪，SAGE 使用了几种技术来提高约束生成的速度和内存使用率：符号表达式缓存 确保结构上等效的符号项映射到相同的物理对象；不相关约束消除 通过删除与否定约束不共享符号变量的约束来减少约束求解器查询的大小；本地约束缓存 如果约束已添加到路径约束中，则跳过该约束；翻转计数限制 建立从特定程序分支生成的约束可以翻转的最大次数；使用廉价的语法检查，约束蕴含 消除由在同一程序分支注入的其他约束逻辑上蕴含的约束（最有可能来自输入相关循环的连续迭代）。
SAGE 架构
图 3 描绘了 SAGE 的高层架构。给定一个（或多个）初始输入Input0，SAGE 首先使用 AppVerifier 运行被测程序，以查看此初始输入是否触发错误。如果没有，SAGE 随后收集在此运行期间执行的唯一程序指令列表。接下来，SAGE 使用该输入符号化执行程序，并生成路径约束，用输入约束的合取来表征当前的程序执行。
然后，实现世代搜索，该路径约束中的所有约束都逐个被否定，与导致它的路径约束前缀结合，并尝试由约束求解器求解（我们目前使用 Z3 SMT 求解器2）。所有可满足的约束都映射到N个新输入，这些输入根据增量指令覆盖率进行测试和排名。例如，如果使用新的Input1执行程序发现 100 条新指令，那么Input1获得 100 分的分数，依此类推。选择得分最高的新输入来完成（昂贵的）符号执行任务，并重复该循环，可能会永远重复下去。请注意，所有 SAGE 任务都可以在多核机器上甚至在一组机器上并行执行。
构建像 SAGE 这样的系统提出了许多其他挑战：如何从符号执行中的不精确性中恢复，如何有效地一起检查许多属性，如何在复杂输入格式中利用语法（如果可用），如何处理路径爆炸，如何精确地推理指针，如何处理浮点指令和输入相关的循环。空间限制阻止我们在此处讨论这些挑战，但作者的网页提供了访问其他论文的途径，这些论文解决了这些问题。
一个例子
2007 年 4 月 3 日，微软发布了一个针对解析 ANI 格式动画光标代码的带外关键安全补丁 (MS07-017)。该漏洞最初由 Determina Security Research 的 Alex Sotirov 于 2006 年 12 月报告给微软，然后在利用代码在野外出现后公开。9 这是自 2006 年 1 月以来微软发布的第三个此类带外补丁，表明该错误的严重性。Microsoft SDL Policy Weblog 指出，对此代码进行广泛的黑盒模糊测试未能发现该错误，并且现有的静态分析工具无法在没有过多误报的情况下找到该错误。6
相比之下，SAGE 在从格式良好的 ANI 文件开始的几个小时内，合成了一个展示该错误的新输入文件，尽管它对 ANI 格式一无所知。从格式良好的 ANI 文件库中任意选择了一个种子文件，并在一个调用user32.dll来解析 ANI 文件的的小型测试程序上运行了 SAGE。初始运行在超过 10,072 个符号输入字节执行 1,279,939 条 x86 指令后，生成了一个包含 341 个分支约束的路径约束。SAGE 然后在 7 小时 36 分钟和 7,706 个测试用例后创建了一个崩溃的 ANI 文件，使用运行 32 位 Windows Vista 和 4 GB RAM 的 2-GHz AMD Opteron 270 双核处理器的单核。
SAGE 的影响
自 2007 年以来，SAGE 在许多大型微软应用程序中发现了许多与安全相关的错误，包括图像处理器、媒体播放器、文件解码器和文档解析器。值得注意的是，SAGE 大约发现了微软 Windows 7 开发期间通过文件模糊测试发现的所有错误的三分之一。由于 SAGE 通常最后运行，因此这些错误被其他所有方法遗漏了，包括静态程序分析和黑盒模糊测试。
找到所有这些错误为微软节省了数百万美元，也为世界节省了时间和精力，避免了为超过 10 亿台 PC 提供昂贵的安全补丁。运行在您的 PC 上的软件受到了 SAGE 的影响。
自 2008 年以来，SAGE 一直在平均 100 多台机器/内核上 24/7 全天候运行，自动模糊测试微软安全测试实验室中的数百个应用程序。这超过 300 个机器年，并且是有史以来任何 SMT（可满足性模理论）求解器的最大计算使用量，迄今已处理超过 10 亿个约束。
SAGE 在发现错误方面非常有效，以至于我们首次面临动态测试生成的“错误分类”问题。我们认为这种有效性来自于能够模糊测试大型应用程序（而不仅仅是像以前使用动态测试生成那样的小单元），这反过来又使我们能够发现由跨多个组件的问题引起的错误。由于 x86 二进制分析，SAGE 也易于部署，并且它是完全自动化的。SAGE 现在每天在微软的各个团队中使用。
结论
SAGE 在微软产生了显著的影响。它结合并扩展了多年来开发的程序分析、测试、验证、模型检查和自动化定理证明技术。
哪种方法在实践中最好——黑盒还是白盒模糊测试？两者都提供了不同的成本/精度权衡。黑盒简单、轻量、容易且快速，但可能产生有限的代码覆盖率。白盒更智能但更复杂。
哪种方法在发现错误方面更有效？这取决于情况。如果一个应用程序从未被模糊测试过，那么任何形式的模糊测试都可能发现错误，而简单的黑盒模糊测试是一个好的开始。然而，一旦那些容易发现的错误消失了，为了找到接下来的错误，模糊测试必须变得更智能。那时就该使用白盒模糊测试和/或用户提供的指导，例如，使用输入语法。
底线是什么？在实践中，两者都使用。我们在微软就是这样做的。
致谢
微软不同团队的许多人都为 SAGE 的成功做出了贡献。特别感谢 Ella Bounimova、Chris Marsh、Lei Fang、Stuart de Jong 和 Hunter Hudson。SAGE 基于 TruScan 团队（包括 Andrew Edwards 和 Jordan Tigani，以及 Evan Tice、David Grant 和 Vince Orgovan）以及 Z3 团队（包括 Nikolaj Bjorner 和 Leonardo de Moura，以及 Youssef Hamadi 和 Lucas Bordeaux）的工作，我们对此表示感谢。如果没有 Windows 安全测试团队（包括 Nick Bartmon、Eric Douglas、Dustin Duran、Elmar Langholz 和 Dave Weston）以及 Office 安全测试团队（包括 Tom Gallagher、Eric Jarvi 和 Octavian Timofte）完成的工作，SAGE 将无法实现如此大规模的部署和使用。我们还要感谢我们的 MSEC 同事 Dan Margolis、Matt Miller 和 Lars Opstad。SAGE 还受益于许多才华横溢的实习研究员的贡献，他们是 Dennis Jeffries、Adam Kiezun、Bassem Elkarablieh、Marius Nita、Cindy Rubio-Gonzalez、Johannes Kinder、Daniel Luchaup、Nathan Rittenhouse、Mehdi Bouaziz 和 Ankur Taly。我们感谢我们的经理对这个项目的支持和反馈。我们还要感谢微软的所有其他 SAGE 用户。
参考文献
1. Bhansali, S., Chen, W., De Jong, S., Edwards, A., Drinic, M. 2006. Framework for instruction-level tracing and analysis of programs. In Second International Conference on Virtual Execution Environments.
2. de Moura, L., Bjorner, N. 2008. Z3: an efficient SMT solver. In Proceedings of TACAS (Tools and Algorithms for the Construction and Analysis of Systems), volume 4963 of Lecture Notes in Computer Science: 337-340. Springer-Verlag.
3, Forrester, J. E., Miller, B. P. 2000. An empirical study of the robustness of Windows NT applications using random testing. In Proceedings of the 4th Usenix Windows System Symposium, Seattle (August).
4. Godefroid, P., Klarlund, N., Sen, K. 2005. DART: Directed Automated Random Testing. In Proceedings of PLDI (Programming Language Design and Implementation): 213-223.
5. Godefroid, P., Levin, M. Y., Molnar, D. 2008. Automated whitebox fuzz testing. In Proceedings of NDSS (Network and Distributed Systems Security): 151-166.
6. Howard, M. 2007. Lessons learned from the animated cursor security bug; http://blogs.msdn.com/sdl/
7. Howard, M., Lipner, S. 2006. The Security Development Lifecycle. Microsoft Press.
8. Narayanasamy, S.,Wang, Z., Tigani, J., Edwards, A., Calder, B. 2007. Automatically classifying benign and harmful data races using replay analysis. In Programming Languages Design and Implementation (PLDI).
9 Sotirov, A. 2007. Windows animated cursor stack overflow vulnerability; http://www.determina.com/
喜欢它，讨厌它？请告诉我们
PATRICE GODEFROID 是微软研究院的首席研究员。他分别于 1989 年和 1994 年在比利时列日大学获得电气工程（计算机科学选修）学士学位和计算机科学博士学位。从 1994 年到 2006 年，他在贝尔实验室工作。他的研究兴趣包括程序规范、分析、测试和验证。 [email protected]。
MICHAEL Y. LEVIN 是 Windows Azure 工程基础设施团队的首席开发经理，他在该团队领导一个团队开发 Windows Azure 监控和诊断服务。他的其他兴趣包括分布式系统中的自动化测试生成、异常检测、数据挖掘和可扩展调试。他获得了宾夕法尼亚大学的计算机科学博士学位。 [email protected]。
DAVID MOLNAR 是微软研究院的研究员，他的研究兴趣集中在软件安全、电子隐私和密码学。他于 2009 年在加州大学伯克利分校获得博士学位，与 David Wagner 共事。 [email protected]。
© 2012 1542-7730/12/0100 $10.00
最初发表于 Queue vol. 10, no. 1—
在 数字图书馆 中评论这篇文章
更多相关文章
Jinnan Guo, Peter Pietzuch, Andrew Paverd, Kapil Vaswani - 使用保密联邦学习的可信人工智能
安全性、隐私性、问责制、透明度和公平性原则是现代人工智能法规的基石。经典的 FL 设计非常强调安全性和隐私性，但以牺牲透明度和问责制为代价。CFL 通过将 FL 与 TEE 和承诺相结合，弥补了这一差距。此外，CFL 还带来了其他理想的安全特性，例如基于代码的访问控制、模型机密性和推理期间对模型的保护。保密计算的最新进展（如保密容器和保密 GPU）意味着现有的 FL 框架可以无缝扩展以支持 CFL，且开销较低。
Raluca Ada Popa - 保密计算还是密码学计算？
通过 MPC/同态加密与硬件飞地进行安全计算，在部署、安全性和性能方面存在权衡。关于性能，这在很大程度上取决于您想到的工作负载。对于简单的工作负载（如简单的求和、低阶多项式或简单的机器学习任务），这两种方法都可以在实践中使用，但对于复杂的计算（如复杂的 SQL 分析或训练大型机器学习模型），目前只有硬件飞地方法在许多实际部署场景中足够实用。
Matthew A. Johnson, Stavros Volos, Ken Gordon, Sean T. Allen, Christoph M. Wintersteiger, Sylvan Clebsch, John Starks, Manuel Costa - 保密容器组
此处提供的实验表明，Parma（在 Azure 容器实例上驱动保密容器的架构）增加的额外性能开销不到底层 TEE 增加的开销的百分之一。重要的是，Parma 确保了容器组所有可达状态的安全不变性，并以证明报告为根基。这允许外部第三方与容器安全地通信，从而实现各种需要保密访问安全数据的容器化工作流程。公司获得了在云中运行最机密工作流程的优势，而无需在其安全要求上妥协。
Charles Garcia-Tobin, Mark Knight - 使用 Arm CCA 提升安全性
保密计算具有巨大的潜力，可以通过将监管系统从 TCB 中移除来提高通用计算平台的安全性，从而减小 TCB 的大小、攻击面以及安全架构师必须考虑的攻击向量。保密计算需要平台硬件和软件方面的创新，但这些创新有可能增强对计算的信任，尤其是在由第三方拥有或控制的设备上。保密计算的早期消费者将需要对他们选择信任的平台做出自己的决定。
© 保留所有权利。