网站后台管理界面下载西安高端模板建站
🔗 课程链接：李樾老师和谭天老师的：南京大学《软件分析》课程01（Introduction）_哔哩哔哩_bilibili
目录
一、静态程序分析介绍
1.1 PL and Static Analysis 程序语言和静态分析
1.2 为什么要学 Static Analysis?
1.3 什么是静态分析 ?
1.4 静态分析的特征和例子
1.4.1 sound and complete （no perfect static analysis）
1.4.2 false negatives or false positives (useful static analysis)
1.4.3 Static Analysis 例子 — Bird's Eye View
1.5 静态分析大致步骤—举个例子🌰
1.5.1 Abstraction（抽象）
1.5.2 Over-approximation(近似): Transfer Functions（转换函数）
1.5.3 Over-approximation(近似): Control Flow（控制流）
1.5.4 总结
一、静态程序分析介绍
1.1 PL and Static Analysis 程序语言和静态分析
PL (Programming Languages, 程序语言)
Static Analysis（静态分析）
如下图所示，PL可以分为三个主题：理论、环境和应用
- 理论：语言设计、语言的类型系统、形式语义和逻辑……
- 环境：编译、运行时系统……
- 应用：程序分析、程序验证、程序合成……
程序语言的分类：
- 命令形语言：C、Java
- 函数式语言：JavaScript、
- 逻辑式语言：一条条逻辑声明出来的语言
挑战：
这么多年来，语言的核心没有变，但是软件越来越复杂，如何保证大规模复杂程序的安全性、可靠性……？
1.2 为什么要学 Static Analysis?
从代码层面来看，静态分析可以做很多事情，后续也会详细讲到：
- 对程序可靠性Program Reliability
空指针引用 null pointer dereference， 内存泄漏 memory leak…… - 对安全性 Program Security
私有信息泄露 private infomation leak, 注入攻击injection attack…… - 编译优化 Compiler Optimization
死代码消除 Dead code elimination，code motion…… - 程序理解 Program Understanding
IDE call hierarchy, type indication……
对于程序员，静态分析可以帮助写更高质量的代码。
1.3 什么是静态分析 ?
Static analysis analyzes a program P to reason about its behaviors and
determines whether it satisfies some properties before running P.
静态分析(static analysis) 是在程序运行之前，分析其行为，确定它是是否能满足某些特性要求：
- 有没有一些程序泄露
- 有没有空指针引用异常?
- 所有的变量variable 用之前都初始化了吗？
- 所有的cast operation是安全的吗？
- v1和v2会不会指向相同的内存地址？
- 程序中的断言语句 assert 会失败吗？
- 死代码？
- ……
但是，根据Rice' Theorem（大米定理/莱斯定理），不存在一个方法可以给出一个确切的答案Yes or No，原文如下：
"Any non-trivial property of the behavior ofprograms in a r.e.language is undecidable."
这句话里的一些词：
- r.e.(recursively enumerable) = recognizable by a Turing-machine
r.e. language: 递归可枚举的语言（图灵机可识别的语言，可以理解为现代的编程语言，C 、JAVA） - non-trivial property：≈ 一些有趣/有价值的性质 ≈ 与动态运行时行为runtime behaviors相关的性质，就像前边列举的空指针、内存变量什么的。
- undecidable: 给不出确切答案
可以这么理解：
一个递归可枚举的语言（图灵机可识别的语言，可以理解为现代的编程语言，C 、JAVA），他的一些non-trivail property（与程序运行时行为相关的性质，例如是否有空指针、有没有内存泄漏）是不能确定的（例如不能准确地说有空指针或者没有）。
再学术一点的理解：
一个 完美的静态分析(perfect static analysis) 是满足 sound and complete 的（sound 和 comlete是 静态分析的两个特征，见1.4.1）.
大米定理就是在告诉我们，不存在完美的静态分析，可以准确地回答Truth，也就是不能同时满足sound 和 complete.
1.4 静态分析的特征和例子
为什么没有一个perfect的呢，因为一些情况其实不可避免，导致分析要么太“过”(sound)，要么太“保守”(complete)。
1.4.1 sound and complete （no perfect static analysis）
如图所示，complete和sound的关系：
- truth：是这个程序中理论上的所有的正确的答案
- complete：指的是，报出来的，都是对的，但是不全
- sound：包含了所有正确答案，
1.4.2 false negatives or false positives (useful static analysis)
既然没有perfect静态分析，为什么还要去研究呢？因为可以对一方妥协，由此就有了useful static analysis（有用的静态分析）。
Useful static analysis：
- Compromise soundness (false negatives，假阴性) : 妥协soundness，就是不sound，会产生漏报（错的没检测到）
- Compromise completeness(false positives，假阳性)：妥协completeness，不complete，会产生误报（对的说是错的）
在绝大Useful静态分析中，我们所研究的更多是妥协completeness：要求分析是 Sound 的，虽然并不全都准确（not fully-precise）（宁可错杀100不可放过一个），可以误报，但是不能漏。
soundness越好，分析就越好。
1.4.3 Static Analysis 例子 — Bird's Eye View
如下图，对左侧的代码进行分析的时候，产生的2个分析结果
这两个分析结果都是对的，没有产生漏报，都满足sound，且：
1 更准确但是昂贵；
2 不够准确但是cheep;
还有一些可能的分析结果如下:
3. x = 0, 1, 2, 3, 4
4. x = 1, 2, 3, 4
其中，3产生了误报，都是涵盖了所有情况，也是sound，是对的；都是4漏了0，是错误的。
一句话概括静态分析：
静态分析是在确保（or 尽量接近）soundness的同时，在分析精度(precision)和速度(speed)之间做一个平衡，这才是一个Useful 静态分析
在实际分析中，可能不存在真正的soundness的，例如java的反射机制、Java的动态类机制，都会影响到soundness，所以是“尽量接近”soundness。
1.5 静态分析大致步骤—举个例子🌰
从技术层面分析静态分析的大致步骤，用两个词来总结静态分析：
Static Analysis = Abstraction + Over-approximation以下通过一个例子来初步感受一下静态分析：
例如：要给一个程序的所有变量判断正负（+，0，-），需要以下两步：
- Abstraction
- Over-approximation
- Transfer functions
- Control flows
1.5.1 Abstraction（抽象）
- 抽象就是把具体的域值映射到抽象域里。
如下图，将左边的变量映射到右边不同的正负情况。抽象成不同的符号。
(unknown)：如果当前数值会因为变量改变而呈现为不同的状态
(undefined): 经过判断肯定不符合int定义的，例如一个除以0的数或者字符等。
1.5.2 Over-approximation(近似): Transfer Functions（转换函数）
在完成抽象之后，我们需要做的就是近似，其中一部就是用到转换函数，转换函数的作用可以概括为如下两句：
- 在静态分析中，转换函数定义了一种转换规则：如何评估关于抽象值的不同程序语句
- 根据“要分析的问题/目标”和不同程序中的“语义（semantics）”来进行评估。
针对于这个例子要分析的问题，转换的规则如下图所示：
利用以上规则，来评估一下具体的程序语句，如下：
- 对于变量c：我们找到了一个除以零的错误
- 对于变量p：y是负数，我们找到了一个负数索引的错误
- 对于变量q：因为a不确定是否为负数，而判定其为undefined，但其实a并不是负数，这里就是一个误报
通过判断符号，我们成功找到了两个错误 c 和 p，说明静态分析是很有用的useful，但是Over-approximation 的静态分析也产生了误报 ，假阳性 false positives。
1.5.3 Over-approximation(近似): Control Flow（控制流）
- 近似还要有控制流，也就是程序执行的流，要将所有流汇聚的地方，进行合并抽象 flow merging。
如下图左侧的程序片段转为右侧的控制流，然后判断符号，[ z = x + y ] 是汇聚的点，所以要枚举其所有分支，进行合并，即 [ y = ]
在静态分析中，如果程序很复杂，我们无法在实际应用中枚举所有的路径，分支流合flow merging （作为over-approximation 的一种方式）是常用的分支推断技术，提升了Soundness，也降低了Completeness，也导致了不可避免的误报问题。
1.5.4 总结
抽象就是将具体值，转为符号值。因为在Abstraction抽象过程中进行了值域空间的 降维抽象 ，所以在转换函数映射中，静态符号执行和动态实际实行的结果之间，是存在差异的，这是不可避免的。
近似就是将每个语句，和每个语句之间的关联进行抽象，化为图来说，就是每个节点，和每个节点之间的箭头
· transfer funtions 是对每个语句的近似；
· control flow 的近似就是 每个箭头 的近似
将每个语句，以及不同语句之间的箭头 都进行近似，就实现了对整个程序的近似。