前言

静态程序分析（static program analysis），是一种方法或者技术用来在执行一个程序之前对该程序的行为和某些感兴趣的属性进行分析的手段。比如判断：1，是否存在私有信息泄露？2，是否存在对空指针的间接引用？3，强制类型转换是否安全？4，两个变量是否可以指向同一块内存？5，断言语句是否成功？6，是否存在死代码需要进行消除？

Static Analysis

Rice’s Theorem

“Any non-trivial property of the behavior of programs in a r.e. language is undecidable.”（r.e. (recursively enumerable) = recognizable by a Turing-machine）–Rice’s Theorem

也就是说，对于那些上面提到的 non-trivial 属性，并不能准确判断程序是否满足这些属性。所以为了得到一些东西，就应该舍弃一些别的东西。

Sound & Complete

假设一个程序存在7处地方和我们感兴趣的某种属性有关，我们想通过静态分析方法找出它们：如果一个静态分析方法具有 Sound 属性时，指的是它常常会报出 N>=7 处结果（绝对包含有正确的7处），在其中有几处地方是我们不感兴趣的，属于静态分析方法判断时产生了失误，称其为误报（false-positive）；如果一个静态分析方法具有 Sound 属性时，指的是它常常会报出 N<=7 处结果（是正确的7处的子集），这N处地方都是我们想要的结果，但是还有几处地方静态分析并没有找到，这也属于静态分析方法判断时产生了失误，称其为漏报（false-negative）。前者称其为过近似（Over-approximate），后者称之为 Under-approximate。
little_ant_ 一般采用的静态分析方法都是牺牲掉 Complete ,保留 Sound 。这样得到结果虽然会有误报，但是这个结果中包含有所有的正确结果。即 Sound but not fully-precise static analysis 。

Sound 示例

对于下面的代码：其中类 B 和 C 是 A 的子类，代码中有两条路径可以到达 B b’ = (B) a.fld; little_ant_
对于 UnSound 的情况下，只会判断某一条路径（取决具体实现）比如仅仅判断蓝色路径，认为这段代码是正确的。而在 Sound 的情况下，是要对两条路径都要进行判断的，因为不确定程序执行流具体会走哪条路径，对蓝色路径判断的结果为正确，对绿色路径判断的结果为错误，对于语句 B b’ = (B) a.fld; 是否能够执行成功并不能得到一个确切的结论。我们认为前者得到的结论是不安全的，而后者得到的结论是安全的。

在静态分析中，下面的代码执行完毕之后 a 的值为多少？

	if(input)
		a=1;
	else
		a=0;

答案是 a=1 or a=0，也可以精确的描述为：当 input 为真时，a=1；input 为假时，a=0。

小结

Static Analysis: ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed.

抽象和过近似（Abstraction + Over-approximate）

静态分析示例

问题：判断对于某个给定的程序中所有变量的符号。（+、- 或者 0）

下面分两步来描述静态分析处理该问题的步骤：

抽象

即对程序中出现的具体的值进行抽象。如下所示：左侧为具体的语句，右侧为抽象的结果

      v=10；       那么 v 对应的符号为正(+)。
      v=-9；        那么 v 对应的符号为负(-)。
      v=0；         那么 v 对应的符号为0(O)。
      v=e?1:-1；那么 v 对应的符号为不知道(T)。（不清楚 e 的值为真或假）
      v=e/0；      那么 v 对应的符号为未定义(⊥)。（除0是一个未定义的运算）

过近似

在将程序中的语句抽象完之后，然后在抽象后的结果上进行过近似操作

转换函数（Transfer Functions）

转换函数是定义如何在抽象值上对不同的程序语句进行评估，至于评估什么要根据程序中语句的语义和我们要分析的问题来决定。接下来以下面这个图片进行说明：
little_ant_
左侧是转换函数，或者说是转换公式会更加确切点。包括有正数+负数=不知道；任何数/0=未定义等等。转换函数所表示的意义并不难理解。

右侧是一个程序中存在的具体语句，注意：对变量符号的判断是在已经抽象的基础上进行的。最后得到了三处未定义的地方，第一处为除0，第二处的数组下标为负值，第三处的数组下标可能为负值。其中第三处的未定义是误报，因为在程序的具体执行中，我们可以轻易的计算出 a 的值为9，在实际执行中并不是负值，即语句是正确的。

控制流处理（Control Flow handling）

控制流处理通常处理：在程序存在分支的情况下，汇合点处变量的符号如何来判断。
little_ant_ 如上图所示：左边是具体的语句，从语句 x = 1 ; 开始程序进入到两个不同的路径里面，分支的汇合点为语句 z = x + y ; 。可以看到左边路径得到的y为正，而右边路径得到的y为负，那么得到汇合点处变量y的值为不确定(T)。

总结

这一部分简单介绍了静态分析的特点比如：不需要执行程序，总是需要保持 Sound 及其原因，保持 Sound 的结果导致容易产生误报。以及静态分析处理程序的两个重要步骤：抽象和过近似。后面会介绍静态分析中 IR 的生成和 CFG 的建建立。未完待续~

静态程序分析chapter1 - 概述和两个重要步骤

文章目录

前言