技术分享 | 浅谈程序分析

编程语言Lab

华为编程语言实验室官方账号，致力于编程语言前沿技术的研究。

原文来自微信公众号： 编程语言Lab - 浅谈程序分析
搜索关注编程语言Lab 公众号： HW-PLLab 获取编程语言更多技术内容
添加小助手微信 pl_lab_001 进入编程语言交流群与同道中人碰撞思维火花

孙军新加坡管理大学教授，研究方向为：形式化方法、软件工程、安全等，爱好：爬山、攀岩等。

如果读者想了解更多有关 程序分析 相关的技术内容，欢迎加入 编程语言技术社区 SIG-程序分析 。

加入方式：文末有小助手微信，添加并备注加入 SIG-程序分析。

# 引言 #

程序分析 是以某种语言书写的程序为对象，对其内部的运作流程进行分析，自动分析计算程序的正确性以及高效性等属性的过程。

虽然经过了几十年的发展，程序分析仍是一个持续热门的研究领域。由于现代软件的复杂性，大型程序的正确性、性能和安全性等都面临新的挑战，所以程序分析技术不只在学术界被大批学者研究，近些年来也越来越受到企业界的青睐。随着大型软件企业逐渐意识到程序分析的重要性，投入做程序分析的公司也越来越多，如 Microsoft、Google、Apple、Facebook 和华为等都有研发团队从事程序分析工作，以及我们熟知的 Coverity、Semmle 等，此外，国内也涌现出很多做程序分析相关的企业如思码逸 Merico、鸿渐 RedRocket、鉴释 Xcalibyte、源伞 SourceBrella 等。

程序分析主要关注两大方面：

程序优化 侧重于提高程序的性能，通过对程序中关键函数的跟踪或者运行时信息的统计，找到系统性能的瓶颈，从而采取进一步行动对程序进行优化，同时减少资源使用。
程序正确性 侧重于确保程序执行它应该做的事情，帮助开发者找出错误代码的位置。（本文以程序正确性的分析为主）

自图灵祖师爷开天辟地以来，怎么保证程序的正确性就一直是一个老大难问题。无数大牛们尝试了各种方法来解决这个问题，结局是各种幻灭。但与此同时，这也造就了现在各种程序分析技术以及产品百花齐放的局面。本文就几种常见程序分析技术及其由来进行了简单的介绍，希望能帮助大家对程序分析有一个初步的了解。

# 程序分析很难! #

计算机发展早期，程序很简单，程序的正确性需求（specification）也很简单，因此，程序的正确性常常显而易见，或者很容易被手动证明。

自然而然地，大家就产生了一种幻觉，可能我们只需要说明我们想要满足什么样的需求，就可以根据需求自动地生成一个程序。如果这样可行的话，程序员的工作无疑将变得轻松无比。换句话讲，我们希望找到一个万能的程序。即， 给定任意的需求，这个程序都能自动的生成一个特定的程序来满足需求。

这个问题在不同的设定下被反复地定义与研究，吸引了无数大神级的计算机科学家曾尝试解决这个问题，包括 Turing、Church、Buchi、Landweber、Pnueli、Clarke 等等。结论是，除了某些意义非常有限的设定，这个问题是 不可判定的 [1]。换句话说， 不存在这样一个万能程序 。当然，更积极一点的说法是， 程序员无可替代 ，程序员需要不停地工作来为特定的用户需求开发特定的程序，软件行业继而蓬勃发展。

然而，毫无保留地信任程序员是要付出代价的。很快，历史证明了程序员编写的程序常常有意或者无意地包含了各种错误、安全漏洞或者后门。

计算机科学家们退而求其次，开始研究如何验证程序员编写的程序的正确性。我们的问题变成了： 给定一个特定的程序和一个特定的需求（例如，没有某种特定的漏洞），我们能不能有工具可以自动的判断这个程序是不是满足需求。 这个问题同样被证明是 不可判定的 。我们只能依赖各种不完备的方法来尽可能找到程序的错误，或者在有限的情况下证明程序的正确性。

程序分析的方法自此百花齐放。

# 知道什么是程序正确性很难！

我们不仅放弃了保证程序正确的梦想，同时也在“正确性”的定义上节节败退。

在上个世纪，理想主义的计算机科学家们天真地认为，正确的编程方式应该是程序员先逻辑精确地表达程序的正确性需求（即 specification），然后再根据该正确性需求来实现程序，最后说明为什么该程序正确。

比如 Dijkstra 在 1969 年很自信地说过 [2]，

“After this decade, programming could be regarded as a public, mathematics-based activity of restructuring specifications into programs.” (十年之后，编程将变成一种基于数学的，把正确性需求翻译成程序的过程。）

然而并非如此。

假设“程序员会花时间把需求详细正式地写出来”已经被一而再，再而三地证明太傻太天真。刚开始的时候（也就是计算机科学家们还没有遭受现实的拷打的时候），很多 specification 语言被发明出来。比如 Oxford 的 Z 语言 [3]，Hoare 的 Communicating Sequential Processes (CSP) [4] 等等。计算机科学家们想象的是，只要我们设计的 specification 语言够直观够好用，程序员们自然就会用。毕竟，有了 specification，我们才能讨论程序正确性的问题啊。

然而并没有发生。

再后来，计算机科学家们扪心自问，为什么这么多这么好的 specification 语言都没有人用，难道是因为程序员们不愿意学一门新的语言？如果是这样，我们提供方法让程序员可以在他们常用的语言里写 specification 就好了嘛。

基于这样美好的想法，Meyer 提出了 Design-by-Contract（把程序的 specification 在程序里写成 code contract [5] [6] [7]），同时 Java Modeling Language (JML) [8] 和（基于 C# 的）SPEC# [9] 两个项目把 Meyer 的想法在主流的程序语言里几乎完美的实现了出来。

然而并没有用。

除了少数几个项目，程序员们并不愿意花额外的时间来写 specification，即使是基于是基于 Java 或者 C#。

计算机科学家们最后的挣扎包括断言（assertion, 即“尽量在相关的地方写一些简单的检查吧”）， 程序标注 （annotation, 即“这些标注挺有用的哈，要不相关的地方用一下啊”）， 测试驱动开发 （test-driven development, 即“要不先写几个测试用例吧，这样我们好检查对不对”）等等。

# 程序分析技术很多! #

Was mich nicht umbringt, macht mich stärker. by Friedrich Nietzsche

“打不倒我的让我更坚强”。

从好的方面讲，因为不存在一个完美的分析程序正确性的方法，各式各样的程序分析方法层出不穷。不只是每年各种学术会议上各种 “无限完美” 的程序分析方法香火不断，致力于软件质量的行业（包括许多知名公司）也得到蓬勃发展。

通过很多年的发展，程序分析的技术和方法日趋丰富。

程序分析技术可以大致分为两类。第一类是 静态程序分析 ，即在不执行程序的情况下进行程序分析。第二类是 动态程序分析 ，即通过运行程序或者在程序运行期间进行分析。当然，也有很多研究工作是关于 如何有效结合静态和动态程序分析 的。同时，因为通常无法拿到真正的程序正确性的需求，绝大多数的程序分析技术着重于分析 通用的程序正确性需求 ，比如如果有断言的话，我们尽量分析断言会不会被违背，再比如分析是否存在整数或者缓存溢出，再或者检测指针相关的安全漏洞等。

下面，我们蜻蜓点水地介绍一下常见的两种程序分析的方法（一种理想化的和一种相对实际的），让大家大概了解它们的优缺点。

# 自动定理证明

自动定理证明（Automated Theorem Proving） [10] 是自动推理和数学逻辑的一个子领域，用于通过计算机程序证明数学定理。

其主要思想是，用某种数学逻辑来表达程序语义，同时通过基于该数学逻辑的定理推导来证明（或者证伪）程序的正确性。自动定理证明就是从 Dijkstra 那里一脉相承的理想主义的做法。常见的被用于自动定理证明的逻辑包括: propositional logic, predicate logic, first-order logic,separation logic 等等。

和传统的（人工）定理证明相比，自动定理证明可以利用各种 proof assistant（比如 Coq [11] 或者 Isabelle [12] 等）来自动检查其证明的正确性。在有限的情况下，也可以针对某些程序实现全自动的正确性证明。

## 如何用逻辑表达

在自动定理证明的方法里，程序的正确性会被表达为对应逻辑的定理。举例来说，若我们想要证明下面程序的正确性，那么我们先要确定用什么逻辑来表达该程序正确性的要求。

float sumUp (float[] array, int length) {
  float result = 0.0;
  int i = 0 ;
  while (i < length) {
    result += array[i];
  return result;
}

假设我们希望证明的是：给定任意一个 float 的数组，函数 sumUp() 都会返回该数组里所有数的和。该要求虽然比较直观，但实际上有很多细节需要考虑。

比如，如果该程序运行起来不会终止（比如有无限循环），算不算正确的？如果不算，我们就需要证明该程序（在给定一个有限长的数组的情况下）永远会终止并且终止时保证返回值是该数组里所有数的和。

再比如说，我们知道浮点数相加和数学上的整数相加并不等价，那么我们就要回答我们证明的时候用的是 实数语义 还是 浮点数语义 。理论上我们当然希望用的是浮点数语义，但是因为浮点数语义本身的复杂性，基于浮点数语义的自动定理证明通常会很难，比如证明过程太慢或者干脆证明不出来。

## 举个栗子

为了简化说明，假设我们不关心该程序是不是永远会终止的问题，同时假设我们基于实数语义来证明。那么，我们可以把该程序的正确性要求用下面的形式（叫做 Hoare Logic [13]）来表达。

// precondition:
// {array != null && length>= 0 && array.length == length}
float sumUp (float[] array, int length) { ... }
// postcondition:
// {result == sum(array[j] for all j in 0..length)}

该程序正确性有两部分组成：

precondition 用以说明程序运行前我们假设满足的条件比如，在上面的例子里我们假设 array 不会是 null , length 为非负数，同时 array.length 和 length 等值。
postcondition 用以说明程序运行终止时必须满足的条件在该例子里我们用了一个辅助函数 sum() 来（非正式地）表达我们的要求。即，函数 sumUp() 的返回值 result 必须和 array 里所有数的和等值。

在这个例子里，我们用到的是 propositional logic（包含关于实数以及预定义函数的 proposition）。如果我们需要更复杂的正确性要求，那么我们可以考虑用更复杂的逻辑来表达。

比如，如果我们想要假设不存在另外一个程序可以不通过 array 来访问该数组（即不存在 array 的 aliasing，不然我们没法保证 array 不会在 sumUp 运行时被修改），那么我们可以用例如 Separation Logic [14] 来表达我们的要求。

自动定理证明工作的原理简单来说就是，通过一些已知正确的定理来不停的推导新的结论，直到推导出我们想要的结果。就上面的例子而言，Hoare Logic 对常见的程序语句提供了多个定理来帮助我们做推导。比如下面这个可以用来推导关于 if-then-else 的程序。

\dfrac{{B \wedge P} S {Q}\quad,\quad {\neg B \wedge P } T {Q}}{{P} \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif} {Q}} \\

上面的定理可做如下解读：

如果一个 if-then-else 里的 then 分支（即 S ）在同时满足 P 和 if 的判断条件 B 的情况下，运行结束时满足 Q ，
同时，该 if-then-else 里的 else 分支（即 T ）在满足 P 并且不满足 if 的判断条件 B 的情况下，运行结束时满足 Q ，
那么我们可以推出，该 if-then-else 语句在满足 P 的情况下运行结束时满足 Q 。

Hoare Logic 对每一种语句都提供了类似的定理。理论上，给定一个特定的程序，自动定理证明只需要根据不同的程序语句来运用相应的定理来不停地推导出新的结论即可。而实际上并没有那么容易，比如有些定理运用起来并没有那么容易，比如循环相关的定理需要 “无中生有” 循环不变量。

## 小结

定理证明的优势在于，我们可以在理论上证明复杂的（相对于其他方法而言）程序的正确性。当然，复杂的程序正确性的要求通常需要复杂的逻辑。

而定理证明的缺点是，现有的自动定理证明工具的自动化程序并没有我们想要的高。我们常常需要给自动定理证明工具提供额外的帮助，比如提供循环不变量，或者提供详细的如何一步一步来运用各种定理的步骤。

基于此原因，定理证明可以说并不适合作为一个常规的程序分析方法，除非允许投入相当大的成本。相对而言，定理证明比较适合用来证明某些特定的库（比如加密算法）或者核心代码（比如内核安全 policy）的实现的正确性。

# 抽象解释

抽象解释（Abstract Interpretation） 是一种简化程序语义从而更高效的进行程序分析的方法。

其核心思想是，如果我们对程序正确性的要求比较简单, 那么我们很可能不需要分析所有的程序语义来证明该程序的正确性。比如，我们如果只关心数组索引会不会越界，那么我们只需要分析作为数组索引的变量的可能取值范围就够了。

在运用抽象解释方法的时候，我们先要确定什么抽象域适合我们的程序正确性要求。

## 如何选择适合的抽象域

在抽象解释方法里，程序的正确性通常表达为 一个确定的抽象域里的断言 （assertion）。常见的抽象域包括：

污点（taint），仅关心变量是否受污染
区间（interval），仅关心变量的取值区间
difference-bound matrix，仅关心任意两个变量之前的差值

等等。以下面的程序为例，

//precondition: y is an array with 10001 elements
void f() {
1.  int x = 1;
2.  while (x < 10000) {
3.    x = x+1;
4.  y[x] = 1;