Proj THUDBFuzz Paper Reading: 北京大学软件分析课程2019，熊英飞, 01 intro

能否彻底避免软件中出现缺陷？

Testing shows the presence, not the absence of bugs -- Dijkstra
首先从整个图灵机的所有潜在程序来说，bug是不可能完全被找到的，
引入Hilberts Program，那么Hilber's Program是什么呢？
它是由德国数学家大卫希尔伯特在20世纪20年代提出，
目标是提出一个形式系统，能够覆盖现在所有的数学定理，并且满足如下条件：

1. 完备性：所有真命题都可以被证明
2. 一致性：一个命题要么是真，要么是假
3. 可判断性：存在算法来确定任意命题的真假

而哥德尔则证明了哥德尔不完备定理，主要内容是蕴含皮亚诺算数公理的一致系统必然是不完备的，可以理解为证明对任意表示自然数的系统，一定有定理不能被证明。
这与软件缺陷有什么关系呢？首先主流程序语言的语法使得程序语言能够表示任意自然数（我们考虑bigInteger类和一个近乎无限的内存），那么，假设有表达式T不能被证明是永远为true或者永远为false，对于如下的代码，就可能造成内存泄漏。

a=malloc()
if (T) free(a);
return;

一般程序员或者静态分析工具是明确在合法输入的情况下T都会为true才会写出这种代码的。
可是在什么情况下连程序员或者静态分析工具被证明绝不可能确定T到底是否为true呢？
引入停机问题，即判断是否存在算法H(P, I)可以判断对于程序P在输入I的情况下是否可停机。显然，程序本身也是一种数据，因此它可以作为输入。

void func(Program p) {
      if (H(p, p)=="halt") loop{};
      else return;//halt
}

显然func(p)的停机状态是H(p, p)简单取反，那么此时如果我们调用H(func, func)，其结果就应该是H(func,func)的取反，产生矛盾。
引入术语Decision Problem（判定问题），Decidable Problm(可判定问题），
因此，调用自身的取反就是一个简单的不可判定问题，它证明了我们如果考虑全部潜在的程序，连判断小小的内存泄漏都难以做到，只能给出警告，不能证明这就是bug。

练习

1. 如下程序分析问题是否可判定？给出证明。
   • 确定程序使用的变量是否多于50个
     - 解: 如果把全部潜在变量，即使没有执行到的变量也视作程序使用的变量，c语言这种完全是能确定的
     - 当然，对于允许 func(int n, array a)for(i = 0;i < n;i++){access(a[i])}而且把a[i]都看作独立变量的或者允许func(String..a){}就不能判断
     - PPT莱斯定理: 认为涉及程序本身所以不能定义
   • 给定程序，判断是否存在输入使得该程序抛出异常
     - 如果程序存在抛出异常这一行为，且该branch能够被执行到，也就是该branch accessible，那么就存在输入使得该程序抛出异常
     - 焦点变成了能否证明程序的异常所在error branch对应的条件是否为永假，又是godel不完备，不能证明
     - Rice定理：举一个性质为真的例子：进入就抛异常。举一个性质为假的例子：进入就退出，不抛异常的空程序，所以undecidable，进而无法判定
   • 给定程序和输入，判断程序是否会抛出异常
     - 停机问题
     - Rice定理：举一个性质为真的例子：进入就抛异常。举一个性质为假的例子：进入就退出，不抛异常的空程序，所以undecidable，进而无法判定
   • 给定无循环和函数调用的程序和特定输入，判断程序是否会抛出异常
     - 按照目前的指令集，似乎是可判定的
     - Rice定理不适用
   • 给定无循环和函数调用的程序，判断程序是否在某些输入上会抛出异常
     - 如果能够被理解为就是上面一问的加强版
   • 给定程序和输入，判断程序是否会在前50步执行中抛出异常（执行一条语句为一步）
     - 这应该与具体程序结构有关，有些程序可能50步还没能启动
     - 但是我认为执行50步就是个超棒的算法了
2. 到底有多少程序分析问题是不可判定的？
   • 无限？

Rice's Theorem

可以将任何程序视作一个输入到输出的partial function，定义平凡语义属性为永真或者永假的语义属性，这里语义属性与程序行为有关（例如，程序是否针对所有输入终止），而不是语法属性（例如，程序是否包含if-then-else语句）。如果某个属性是两个自动机中的任何一个都可能拥有或可能不拥有的，同时仍然实现完全相同的语言，则该属性是属于自动机的，而不是属于语言的，并且莱斯定理不适用。

证明

如果存在一个能够判断对于程序Prog在输入i时性质X能否成立的通用算法，那么就建立一个程序P'，P'需要先判断程序P''在输入i''会不会停机，如果会停机，那么就执行Prog，否则就不表现，所以为了解决P'在输入i时性质X会不会出现，就要先明确程序P''在输入i''时会不会停机，所以，判断性质X之前就必须要判断P''和i''能否停机了。那么，外层套一个输入为P''和i''的算法，它调用这一套流程就能判断P''和i''是否停机。
而停机问题是不可判断的（因为自己调用自己取反就会产生停机矛盾）所以这样一个判断性质X的通用判断器不存在。
注意如果性质X在空集，也就是不接受任何语言的自动机上能被满足，那么P''此时的程序P'无论P''在输入i''时会不会停机都会满足X性质，Reduce也就无法继续进行了。所以要特殊处理空集的情况，把此时的性质X取反，此时空集就不再满足性质X。不过要注意对性质X取反不等于对整个自动机的结果直接取反，因为对整个自动机的结果直接取反，就相当于把一些不合法输入变得合法了，所以在本应表现X性质现在却不表现的同时，还要把混进来的不合法输入reject，使其表现出X性质。

证明书面化1：

应用

https://gatecse.in/rices-theorem/

什么情况下可以检查停机？

程序不会调用停机判断算法本身的时候，当然可以检查停机。
但是，当程序要调用到停机判断算法本身的时候，就会状态爆炸。
因此，基于有限状态自动机抽象判断程序属性的技术在硬件领域已经被广泛应用，但是软件领域有自身调用的可能所以很少用。
软件领域只能够尽量近似，也就是处理性质X在类似输入i的情况下几乎都是真的，性质X在类似输入i的情况下几乎都是假的这种程序和输入，或者输出一个置信度比较高的判断。

健壮性

来源：程序分析技术最早源自编译器优化，而在编译器优化中，我们需要保证绝对不改变程序语义。

求近似解基本方法-抽象

例如判断加减乘除的结果是否为正数，可以将输入划分为正，0，负，将输出划分为正，0，负，槑（全体证书或者NaN)。
那么就能够划分如下图表，进而可以判断除了槑之外的所有情况下结果是否为正数

求近似解基本方法-搜索

直接遍历+剪枝得到所有程序分支的可能结果，并且明确每个分支是否满足性质P

课程内容

第一部分-抽象

1. 数据流分析
   • 如何抽象分支，循环等控制结构
2. 过程间分析
   • 如何对函数调用关系进行抽象
3. 指针分析
   • 如何对堆上的指向结构进行抽象
4. 抽象解释
   • 抽象的通用理论

第二部分-搜索

1. SAT
   • 基础可满足性问题
2. SMT
   • 通用可满足性问题
3. 霍尔逻辑
   • 表达程序规约的方法和相应推导方法
4. 符号执行
   • 基于约束求解的路径敏感分析

第三部分

1. 程序综合-如何让电脑自动编写程序
2. 缺陷定位-确定程序有bug后，如何定位bug
3. 缺陷修复

课程项目1 java指针分析系统
项目2-程序综合工具，能根据规约自动编写程序求解样例