高级静态分析符合基于合约的编程

高级静态分析工具正在成为许多专业程序员工具包的标准部分。同时，越来越重视基于契约的编程，其中明确的前置条件、后置条件和其他契约被添加到源代码中，以帮助增强软件安全性和安全性，因为嵌入式系统变得越来越复杂和相互依赖。当这两种趋势相遇时，就会出现一些有趣的机会。特别是，某些高级静态分析工具开始直接识别合约，有些甚至通过从现有代码中推断出合约来帮助程序员创建合约。对高级静态分析的回顾有助于为讨论基于契约的编程奠定基础。

回顾高级静态分析

较新的静态分析工具不再简单地执行编码指南，而是深入研究程序结构的语义，有效地模拟运行时可能发生的情况，以检测逻辑不一致或安全漏洞。这些工具通常基于编译器技术，使用高级数据流分析来确定程序可能出错的地方，方法是跟踪变量在运行时可能具有的值，然后检查这些值是否都被程序正确处理以及是否可能被污染数据在被信任之前经过适当的审查。在代码实际上安全可靠但工具的价值跟踪或污点跟踪不够精确的地方，此类工具仍然存在产生误报（实际上是误报）的挑战。尽管如此，

图 1 说明了静态分析器如何使用数据流分析来跟踪变量（例如Count ）的可能值，并确定这些值中的任何一个是否可能在以后的某个时间点导致问题。正在显示表格的值，然后是平均值。这里的经典“错误”是忽略表为空的可能性，从而导致可能的被零除错误。

图 1：高级流量分析示例

在这个例子中，为了避免被零除，程序员已经包含了一个表有至少一个元素的断言（即“ Table‘Length 》= 1） ”。但是，需要进行一些数据流分析来验证Float（Count）在除法“ Sum / Float（Count） ”中是否非零。这需要静态分析器将Float（Count）的值链接到Count的值，将Count的最终值链接到由Table’Range确定的循环迭代次数，并将该数字链接到Table‘Length（X’Range 表示“X‘First 。. X’Last”，而 X‘Length 表示“（如果 X’First 》 X‘Last then 0 else X’Last – X‘First + 1）”）。对程序员来说容易的事情可以为静态分析器做更多的工作。

那么静态分析器对“ pragma Assert（Table’Length 》= 1） ”做了什么？这就是分析器不同的地方，这取决于他们是采用自下而上还是自上而下的策略来发现跨越过程边界的错误，以及他们如何将这一点与基于合同的编程概念相结合。

基于合同的编程适合的地方

基于契约的编程（除其他外）是使用前置条件和后置条件来表达对组成程序的功能和过程（即子程序）的输入和输出（分别）的期望。

在图 1 的示例中，程序员的意图显然是“ Table‘Length 》= 1 ”作为该过程的先决条件。不幸的是，这个Assert隐藏在过程的代码中，而不是很容易被调用者看到。在 Eiffel［1］ 或 Ada 2012［2］ 等语言中，前置条件和后置条件是语法的一部分，或者在 C# 或 Java 等语言中使用 Spec#［3］ 或 Java 建模语言 （JML）［4］ 等扩展，程序员对Display_Table过程的表输入的意图可以使用显式前置条件来表达。例如，在 Ada 2012 中，此过程的规范可以写成：

过程 Display_Table（Table： Float_Array） 与 Pre =》 Table’Length 》= 1;

这为Display_Table过程指定了方面Pre（“前提条件”的缩写），因此它对调用者可见并有效地成为Display_Table上的合同，这表明只要Table的长度至少为 1，Display_Table就可以执行它的正确工作。

静态分析：检查和推断合约

现在回到图 1 中的 pragma Assert。如果没有明确的合同要求调用者确保Table‘Length 》= 1，静态分析器可能会正确地抱怨，因为没有什么可以阻止调用者传入零长度表。但是，许多静态分析器使用不同的策略。他们不是立即抱怨Assert，而是依靠更多的全局检查来确定是否存在真正的问题，并且仅在有一个通过零长度表的调用时才抱怨。如前所述，这些全局的、过程间的检查可以主要是自下而上的，也可以主要是自上而下的，如图 2 所示。

图 2：自上而下与自下而上的过程间静态分析

在自上而下的策略中，分析器从程序的入口点向下走，在每次调用时用实际参数代替形式，直到识别出每个子程序的每次调用，累积一组可能的实际值传入对于每个正式的。然后使用该值集来确定是否可能通过某些特定的调用链违反Assert 。

在自下而上的策略中，分析从程序的叶子（不进行调用的子程序）开始，分析每个子程序以确定它对其输入施加的要求。在此示例中，Assert（Table’Length 》= 1）被有效地转换为过程的隐式前提条件。静态分析器本质上是在为每个子程序推断未声明的合约，然后将其传播到每个调用点，其中前提条件成为调用点实际参数的隐式断言。这个过程一直持续到更高级别的子程序，直到最终整个程序都被分析完。

随着程序变得越来越大，自下而上的方法可以比自上而下的方法更好地扩展，但它取决于推断潜在的复杂合同，包括条件先决条件，其中一个输入的先决条件可能取决于另一个输入的值。例如，对于以“ if X 》 0 then Assert（Y 》 0） ”开头的过程，推断的前提条件应该是“ X 》 0 ==》 Y 》 0 ”。两种通过自下而上分析推断合约的高级静态分析工具是 AdaCore 的 CodePeer 工具，它分析 Ada 源代码，以及 Microsoft Research 的 Clousot 工具，它分析 .NET 程序。

随着明确的前置条件和后置条件开始出现在程序中，使用像 Ada 2012 这样的语言，这些合同和高级静态分析工具的功能之间出现了新的协同作用。显式契约可以简化程序间分析，因为程序员已经完成了艰苦的工作。该工具可以简单地检查显式前提条件，而不必在调用中传播。在子程序中，该工具可以使用前置条件作为可能输入值的精确描述，而无需猜测程序员的意图。

显式契约还可以帮助其他希望使用子程序的程序员，因为它们充当机器可检查的注释和直接嵌入代码中的低级需求。但它们只有在程序员编写它们时才有帮助。由于一些高级静态分析工具可以从源代码中推断出合约，它们可以提供自动将它们插入源代码。Clousot之类的工具允许程序员“祝福”推断的合约，使其成为源代码的永久部分。

未来：一边编程一边证明

静态分析和基于合同的编程之间的协同作用可能允许更快地采用这两种技术。随着这两者的集成，一种新的编程方法可能会出现，程序员的助手会在创建源代码时帮助推断和检查合同。随着程序的编写，安全性得到了证明，就像文本编辑器中的拼写检查器可以确保不会出现拼写错误的单词一样。随着这些技术的成熟，我们可以希望不安全、不安全的程序将不再是常态，而是从一开始就内置安全性和安全性，并附带代码的机器可检查、人类可读的合约。书面。CodePeer和 Clousot等工具展示了一些可能性。

审核编辑：郭婷