程序静态分析第一课

——该课程主要内容来自北京大学熊英飞老师的《软件分析技术》

事例一：飞机为了保证飞行安全，在很多设备上会设置冗余设备，一般来说都是一主二备三应急，一架飞机上同样功能的设备设施，会安装起码三套或更多来应付其中一套出故障而导致飞机飞行安全出问题。

事例二：以电控为例，高可靠度的工业系统一般会选择传感器 3 取 2 或 5 取 3 方式输入，什么是 3 取 2 呢？以平行方式连接三个一样的传感器，输入同一个数据处理设备。那么当其中任一个出现损坏时，该传感器就会出现异常，和其他两个传感器冲突。这时候处理设备会取另外 2 个传感器的数据，抛弃掉异常数据，从而保证数据准确。

为了高可靠性、安全性，我们要付出很多额外的成本和精力，为什么这些缺陷、异常或者故障无法避免？为什么这些设备系统无法保证完全可靠？

哥德尔不完备定理

一致性（consistency）：对于一个命题，你不能证明它既是真的也是假的。
完备性（completeness）： 对于任意一个命题，你要么可以证明它是对的，要么你可以证明它是错的。

第一定理
一个足够复杂的公理体系如果具备一致性，那么就不具备完备性。也就是说，完备性和一致性不可能同时获得。
大白话解释一下，就是说，一个没有矛盾的公理体系内，总有一些命题是说不清楚对还是错的。

第二定理
公理体系的一致性不能在这个公理体系内被推导出来。也就是说，不仅完备性和一致性有矛盾，即使是一致性本身，也不能在公理体系内得到证明。

哥德尔不完全性定理一举粉碎了数学家两千年来的信念，所有逻辑体系都存在有不能被证明或否定的命题。因此，所有逻辑体系都 “不完备”。
同理，我们可以推导出任何复杂的系统或设备或软件程序，都是不完备的，即无法保证完全可靠的，可能会存在问题的。既然问题一定存在，我们继续探究，是否存在一些方法，能让我们来判定这些问题的存在？

停机问题证明

判定问题（Decision Problem）：回答是/否的问题。
可判定问题（Decidable Problem）是指一个判定问题，该问题存在一个算法，使得对于该问题的每一个实例都能给出是/否的答案。
停机问题（英语：halting problem）是逻辑数学中可计算性理论的一个问题。通俗地说，停机问题就是判断任意一个程序是否能在有限的时间之内结束运行的问题。该问题等价于如下的判定问题：是否存在一个程序 A，对于任意输入的程序 B，能够判断 B 会在有限时间内结束或者死循环。图灵于 1936 年证明，不存在一个算法能回答停机问题。

假设存在停机问题判断算法：bool Halt(p), true 为停机，false 为死循环，p 表示特定程序。

void Evil() {
if (!Halt(Evil)) return;//停机
else while(1);//死循环
}

Halt(Evil) 的返回值是什么？
如果返回 true，表示停机，而实际 Evil() 是死循环状态。
如果返回 false，表示死循环，而实际 Evil() 是停机状态。

类似于理发师悖论：理发师给那些不给自己理发的人理发，那么理发师给自己理发么？
结论：不存在一个判定一切程序的程序，因为这个程序本身也是程序，即停机问题是一个不可判定问题。
所以，并不是所有的问题都是可以判定的，并且不管是用人去检查程序，还是用程序去检测程序，都无法保证找出所有的问题。
所以我们是不是就会放弃对问题的判定检测？不可能的。
正确的思路应该是，基于目前我们已知的现状，应该如何更好的发挥我们有限的能力去尽可能的找出更多的问题？

---

这里终于可以引出我们的课程：
如何利用程序去检测程序中的问题？
——程序静态分析
概念：
程序静态分析（program static analysis）是指在不运行代码的方式下，通过词法分析、语法分析、控制流、数据流分析等技术对程序代码进行扫描，验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术。

程序分析技术最早源自编译器优化，至今已经发展了几十年，在学术界已经有了数据流分析、过程间分析、指针分析、约束求解和符号执行等多个研究方向。但是由于专业知识的门槛太高，导致学术界的一些研究成果很难落地到工业界，这中间需要一大批既懂学术研究又懂工业界应用的人来作为传输的纽带。
这也是我开始写这个系列课程的原因，我希望大家在看完系列课程后，能够对学术界的专业知识有个整体的基本了解。如果恰巧有人非常有兴趣，可以一起来做更深入的探索，将学术界的研究吸收消化并输出到工业界中，也是一大幸事。

---

工业界的常规手段——通过统计获得启发式规则

目前工业界，即我们日常熟知的代码静态分析主要使用的方法。
例如针对 File.Open 的启发式规则：
如果被调用函数名为 java.io.File.Open，则假设该函数返回一个指向新内存位置的指针，并且不影响已有指向关系。

• 该规则不能保证正确
  • 如果用户用了不同的 JDK 实现
  • 如果用户自己的函数命名为 java.io.File.Open
  • 如果 Java 未来升级新版本引入了不同的行为
• 启发式规则通常不容易定义
  • File.Open 只是 JDK 的一个函数，人工为 JDK 所有函数建模需要大量时间
  • 对于涉及具体应用程序的未知量无法提前定义
  • 应用程序需求、软件设计上的约束
• 采用统计的方法获得启发式规则
  • 例 1：对于 File.Open 函数的大量执行进行统计，发现该函数始终不改变任何已有指向关系，于是认为该函数不改变指向关系。
  • 例 2：对于大量代码分析发现 99.9% 的情况下调用 File.Open() 之后都会调用 File.Close()，于是可以将该要求记录为一条设计约束，剩下 0.1% 的情况就是潜在 Bug。

目前市面上开源的静态扫描扫描工具，例如 PMD、Sonar、Lint 和阿里 P3C 等都是启发式规则的典型代表。

学术界的研究——近似求解 + 抽象

近似法：允许在得不到精确值的时候，给出不精确的答案。
原始判定问题：输出 “是” 或者 “否”， 近似求解判定问题：输出 “是”、“否” 或者 “不知道”。
求近似解基本原则——抽象，这个不做过多解释，我们用一个例子来帮助大家理解：

• 正 ={所有的正数}
• 零={0}
• 负= {所有的负数}

正 + 负=？
解决方案：增加抽象符号表示 “不知道”——槑

• 槑= {所有整数}

我们来填写以下抽象后加法运算表：
| + | 正 | 负 | 零 | 槑 |
| -------- | -------- | -------- | --------- | --------- |
| 正 | 正 | 槑 | 正 | 槑 |
| 负 | 槑 | 负 | 负 | 槑 |
| 零 | 正 | 负 | 零 | 槑 |
| 槑 | 槑 | 槑 | 槑 | 槑 |

基于这种抽象，如果我们在代码中遇到了变量运算和赋值，就可以给出一个大概的判断，使整个程序具有一定的可分析性。

同理，我们把程序进行不同程度的抽象，然后求出近似解，就是程序分析。
基于抽象的程序分析有以下四大类：

1. 数据流分析
   • 如何对分支、循环等控制结构进行抽象
2. 过程间分析
   • 如何对函数调用关系进行抽象
3. 指针分析
   • 如何对堆上的指向结构进行抽象
4. 约束求解和符号执行
   • 如何确定某条路径的可执行性

看到这里是不是觉得依然很难理解程序怎么抽象的？
没关系，我们会在后续的文章中依次详细讲解这四类程序分析。

延伸问题思考：
问题 1：测试人员能否找出软件中所有的 BUG？
问题 2：人工智能驾驶技术能否彻底避免车祸？