南京大学软件分析课程，这段时间可以把自己学习的内容总结一下。
0x01 PL and Static Analysis
08:05
开始，剪课件...
背景：将PL分了三个领域。 程序分析属于PL的应用领域。
- 在语言的框架下谈到程序分析就是静态分析。
0x02 Why We Need Static Analysis
17:40
应用背景:
Program Reliability
Program Security
Compiler Optimization
Program Understanding
静态分析是在编译时刻完成了对程序的分析
更深入地理解编程语言的语法、语义
写出更加可靠、更安全、更高效的程序
这一块自己也觉得之前写代码，感觉用不上自己学的理论知识。学了一些编译原理尤其是静态分析内容后，感觉把理论和实践打通了。再加上操作系统和组成原理。 写代码的时候逐渐知道编译器在干什么， 操作系统在干什么， 硬件在干什么...
0x03 Static Analysis
35:40
正式开始了...
- 静态分析： 在运行一个程序之前， 通过静态分析，了解程序一些行为和特征，
Truth是我们需要的结果机， 包含了所有可能的分析结果
- Sound：Overapproximate， 包含了所有的Truth
- Complete: Underapproximate, 在Truth
比如找洞， Truth是所有的洞， 而Complete是Truth的子集， 报出来的没有假的(无误报)。而Sound是包含了所有的Truth，但是会有误报。(这是设计时的目标方向， 实际使用时，大部分工具，既有误报，又有漏报)
我们的目标是设计一个useful static analysis，在上图画一个结果集的圈， 我们需要妥协一方(看应用场景)。 妥协Sound，就是要让Sound妥协， 让Sound缩小，就会造成生漏报(false negatives)，这种分析是Compromise soundness。
同样的， 妥协Complete， 就是要不产生误报(false positives)。 这种分析是Compromise completeness的。
这两种设计方案随目的不同，在需要的场景下，都算是useful static analysis。
Soundness is
criticalto a collection of import(static analysis) applications such as commpiler optimization and program verification.(编译优化和程序验证soundness尤为重要)这里说一个静态分析，soundness是重要的，也就是complete妥协。可以产生误报， 可以不那么准确。
也就是说sound的分析会包含分析中所有的情形。(全面之后才能得到正确的结论)
从静态分析角度， sound就可以理解为正确的
Static Analysis: ensure(or get close to) soundness, while making good trade-offs between analysis precision and analysis speed.(在保证正确性的前提下，做精度和速度的平衡)
0x04 Example about Static Analysis
71:00
Two Words to Conclude Static Analysis: Abstraction+ Over-approximation
一个check, 探测每一个变量的符号。
- Abstraction： 将真实值转化为抽象值(abstract values)
- Over-approximation: Transfer Functions
Transfer Functions define how to evaluate different program statements on abstract values.(对每一个语句的抽象值制定转化规则)
Transfer functions are defined according to "analysis problem" and the "semantics" of different program statements.（根据分析目标和每一句话的语义制定转移函数）
现在，有了抽象值， 有了转化函数， 可以进行静态分析。
其中， a可正可负，p 中y做索引错， q中a做索引， 保证soundness， 可能错。
c 除零错误
p negative array index
q 误报
为了保证soundness，要求所有控制流的汇聚的点，都需要做merge。 Flow-Merge作为默认的一种Over-approximation方式。
每一个语句， 与control flow 构成了真正的程序。 将两者抽象，就讲整个程序抽象了。