符号执行技术可识别安全关键代码中的漏洞

多核处理器在安全关键型应用中越来越受欢迎，因为它们提供了显著的价格和性能改进。但是，为多核硬件编写多线程应用程序是出了名的困难，并可能导致灾难性故障。下面描述了用于识别问题（包括数据争用）的符号执行技术？最常见的并发缺陷之一？以及静态分析如何帮助开发人员找到并消除它们。

最大化性能对于军事嵌入式系统尤为重要，因为在日益数字化的战场上，人们越来越需要保持低成本，同时满足连接要求。随着制造商达到小型化和集成度提高所能达到的极限，提高性能的最佳方法是使用多核处理器。

缺点是，为了充分利用并行执行的许多内核，必须将软件编写为本质上是多线程的。为单核处理器编写为单线程的软件在多核处理器上执行时将实现很少或没有性能优势：必须重写或调整它以使用多线程。关键挑战是尽可能保持核心繁忙，同时确保它们正确协调对共享资源的访问。不幸的是，编写这样的代码比编写单线程代码要困难得多。当存在死锁或争用条件等缺陷时，它们可能会以难以诊断的方式表现出来。查找和消除并发 bug 的传统技术可能无效。

并发错误如此困难的核心原因之一是，当线程执行时，线程中的事件可以通过多种方式交错。随着线程或指令数量的增加，交错的数量呈指数级增长。如果线程 A 执行 M 条指令，线程 B 执行 N 条指令，则两个线程可能存在 N+MCN 交错。例如，给定两个平凡的线程，每个线程有 10 条指令，这些指令有 184，756 个可能的交错。即使使用非常小的程序，很明显也几乎不可能测试所有可能的组合。其次，即使可以识别导致故障的单个交错，也很难设置使用该特定交错的可重复测试用例，因为线程调度实际上是不确定的。因此，调试并发程序可能非常昂贵且耗时。争用条件是一类并发缺陷，很容易意外引入，并且很难通过常规测试消除。但是，程序员可以使用一些技术来查找和删除它们。

潜在的灾难性故障

与单线程代码相比，并发程序中可能会出现全新的缺陷类别，包括死锁、饥饿和争用条件。这些缺陷主要会导致开发过程中难以诊断和消除的神秘故障。我们合作过的一家航空电子制造商花了两个人年的时间应用传统的调试技术，努力找到间歇性软件故障的根本原因，结果证明这是一种竞争条件。有时后果可能很可怕——有史以来最臭名昭著的两个软件故障是由竞争条件引起的。Therac-25放射治疗机具有导致几名患者死亡的种族条件。同样，2003 年东北停电因竞争条件而加剧，导致误导性信息被传达给技术人员。

有几种不同类型的竞争条件。最常见和最隐蔽的形式之一 - 数据竞争 - 是涉及访问内存位置的竞争条件类。

当有两个或多个执行线程访问共享内存位置，至少一个线程正在更改该位置的数据，并且没有用于协调访问的显式机制时，就会发生数据争用。如果发生数据争用，则可能会使程序处于不一致状态。

考虑控制襟翼位置的航空电子代码。在正常情况下，襟翼处于飞行控制软件指示的位置，但飞行员可以通过按下控制面板上的按钮来覆盖该位置，在这种情况下，使用手动设置的位置。为了简单起见，假设程序中有两个线程：一个控制翻盖，另一个监视控制面板上元素的位置。还有一个名为 is_manual 的共享布尔变量，它对手动覆盖是否设置进行编码。摆动位置螺纹检查is_manual的值，如果为 true，则相应地设置位置。控制面板线程侦听按钮按下事件，如果按下替代按钮，它将is_manual设置为 true。图 1 显示了为实现此规范而可能编写的代码。此代码可能在大多数情况下都有效;但是，由于 is_manual 变量对两个线程共享的状态进行编码，因此它容易受到数据争用的影响，因为对它的访问不受锁保护。如果在飞行员按下超控按钮的确切时间执行襟翼定位代码，则程序可能会进入不一致的状态，并且将使用错误的襟翼位置。图 2 显示了这种情况是如何发生的。

图1：访问共享变量的两个线程中的代码

图2：导致数据争用的指令交错

这个例子巧妙地说明了数据争用的一个属性，这使得它们难以诊断：损坏的症状可能只有在数据争用发生很久之后才能观察到。在这种情况下，只有当飞行员注意到飞机没有按预期响应时，才会注意到使用错误的襟翼位置的事实。

人们普遍认为，数据竞争的某些实例是良性的，可以容忍。然而，现在毫无疑问，这很少是真的。C 标准［4］ 明确指出，编译器可以假设没有数据争用，因此优化器可以并且确实进行了对提高单线程代码性能有效的转换，但在存在明显良性的竞争条件时引入了错误。这些都是微妙的影响——即使是经验丰富的程序员也经常对它们感到惊讶。（有关完整的解释和几个令人信服的示例，请参阅参考文献 ［1］。因此，为了实现高水平的保证并避免灾难性故障，查找并删除所有数据争用非常重要。

消除并发缺陷

鉴于并发缺陷，尤其是数据争用，风险很大，因此使用多种技术来消除它们非常重要。由于不确定性，传统的动态测试不太适合发现许多并发缺陷。通过测试数百次的程序以后可能会在具有完全相同输入的相同环境中失败，因为该错误可能对时间非常敏感。寻求高保证的工程师如果要消除并发缺陷，就必须转向其他技术。

静态分析工具提供了一种查找此类错误的方法。测试和静态分析之间的主要区别在于，它针对给定的一组输入测试程序的特定执行，而静态分析查找适用于所有可能执行和所有输入的属性。（在实践中，静态分析工具进行近似以获得可接受的性能和精度，因此达不到这个理想模型。尽管如此，它们确实涵盖了比传统测试更多的情况。

粗略地说，静态分析工具的工作原理是创建程序模型并对该模型进行符号执行，在此过程中查找错误条件。例如，GrammaTech的CodeSonar静态分析工具通过创建哪些锁由哪些线程持有的映射，并通过推理可能导致对共享变量的不同步访问的可能交错来查找数据竞争。使用类似的技术发现死锁和其他并发缺陷（包括锁管理不善）。

自定义并发构造：案例研究

当程序使用标准方法来管理并发时，标准缺陷检测技术最有用。大多数工具识别并推理标准库（如POSIX线程库）或专有接口（如VxWorks）的特殊属性。但是，许多系统使用自定义技术来管理并发性。

例如，与我们合作的另一家制造商在使用自定义抢占式多线程软件接口的平台上构建了一个安全关键型设备。在此设计中，一个关键约束是，必须使用适当的保护构造保护可以从多个优先级线程访问的所有数据实例。在使用静态分析之前，验证是否遵守此约束需要花费人工月的手动分析时间。为了降低成本，他们通过转向静态分析来寻求解决方案。现代高级静态分析工具的一个重要特性是它们是可扩展的：它们提供了一个带有抽象的 API，可以方便地实现自定义静态分析算法。使用 CodeSonar 的 API，他们能够编写一个解决方案，该解决方案利用现有分析核心使用的算法来查找代码中违反设计约束的位置。生成的工具作为插件实现，能够自动查找违反关键约束的情况，所有这些都只需一小部分成本和比以前少得多的时间。

多核权衡

转向多核处理器设计有令人信服的理由，但风险在于这样做可能会在软件中引入并发缺陷。这些很容易引入 - 即使是看似无辜的代码也可能隐藏令人讨厌的多线程错误 - 并且众所周知，当它们发生时很难诊断和消除。仅靠传统的测试技术不足以确保高质量的软件，这主要是因为高度的非确定性。使用使用符号执行的高级静态分析工具是一种可以提供帮助的方法，因为此类工具可以推理代码执行的所有可能方式。这些工具可以在使用标准多线程库的代码中发现数据争用和死锁等缺陷，甚至可以适应使用非标准并发构造的设计。

审核编辑：郭婷