前言
程序分析技术在安全研究中有广泛的应用。例如，之前我们分享过的SLAKE、DirtyCred和AEM等研究都普遍使用了多种程序分析技术，能够将许多人工分析工作自动化，有着非常不错的成果。就我所看到的而言，无论是漏洞挖掘、ExP自动生成（AEG），还是寻找符合某种条件的漏洞利用辅助对象、验证某种防御绕过手段的有效性的场景，有了程序分析技术，都将如虎添翼。
因此，带着安全研究方面的需求和从论文中了解到的一些模糊概念，我将开始学习由南京大学李樾、谭添两位老师开设的“软件分析”课程。虽然该课程主要面向的是南京大学学生，但是老师和同学们已经把相关资源分享在了互联网上，任何人都可以学习。再一次体会到互联网的开放和分享精神！
该课程的相关资源列举如下：
- 课程官方网站：http://tai-e.pascal-lab.net
- 课程主页：http://tai-e.pascal-lab.net/lectures.html
- 课程作业仓库：https://github.com/pascal-lab/Tai-e-assignments
- B站视频：https://www.bilibili.com/video/BV1b7411K7P4/
- OJ平台：https://oj.pascal-lab.net/problem
第一节课的内容比较简单，但是李樾老师讲得非常引人入胜。这里简单归纳梳理一下吧。
课程大纲
“课程”项的超链接是我的笔记。
实验大纲
“实验”项的超链接是我的笔记。
| 序号 | 实验 | 序号 | 实验 |
|---|---|---|---|
| A1 | Live Variable Analysis and Iterative Solver | A5 | Context-Insensitive Pointer/Alias Analysis |
| A2 | Constant Propagation and Worklist Solver | A6 | Context-Sensitive Pointer/Alias Analysis |
| A3 | Dead Code Detection | A7 | Alias-Aware Interprocedural Constant propagation |
| A4 | CHA and Interprocedural Constant Propagation | A8 | Taint Analysis |
实验之间的关系如下图所示：
程序分析的意义
学习需要既见树木又见森林。老师给出了程序分析在编程语言研究领域中的位置，如下图所示：
本课程所说的程序分析，指的是在不运行程序的前提下实现分析，也就是静态分析。后面很多时候，“程序分析”和“静态分析”两个词可能会混用。
当下，程序分析的研究背景是：过去十多年，程序语言核心部分几乎没有变化，但是程序在不断变大变复杂（语用环境）。与此同时，相应的挑战是：如何确保大规模复杂程序的可靠性、安全性以及其他品质？
为什么需要静态程序分析呢？因为静态分析可以帮助提高程序可靠性、安全性、编译优化能力，并能够帮助人类理解程序（如IDE的智能提示功能）。
本课将静态分析定义如下：
Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P.
例如，我们想在运行前知道程序P是否可能存在信息泄露漏洞、是否会对空指针解引用等。
Sound & Complete
然而，可计算理论中的莱斯定理证明，递归可枚举语言的所有非平凡性质都是不可判定的。莱斯定理的规范定义如下（摘自维基百科）：
$P$是所有图灵可计算函数构成的集合，$S$是$P$的一个非空真子集，即：$\emptyset \neq S \subsetneq P$。
将图灵机以某种方式编码，使得每一个$n \in \mathbb{N}$都唯一对应一个图灵机$M_{n}$。
则：集合$C(S)=\{n | M_{n}计算的函数在集合S中\}$是不可判定的。
目前我们接触到的编程语言基本都是递归可枚举语言。所谓的“非平凡性质”可以简单理解为是那些有趣、有价值的性质，比如前面我们提到的是否存在信息泄露漏洞等。也就是说，不存在完美的静态分析来确定程序$P$是否满足某个非平凡性质。
所谓完美的静态分析指的是既sound又complete的分析。对于一次分析来说，sound可以理解为可能比较宽松、存在误报，complete则是比较严格、但可能存在漏报的情况。而理论上的完美和真实则介于sound和complete之间，它们三者的关系可以用集合来抽象表示：
另外，sound的结果可以称为over-approximate，complete的结果也可以称为under-approximate。尽管完美的分析并不存在，但是有用的分析是存在的，这通常需要在某种程度上牺牲soundness或completeness中的一个。例如，牺牲一定soundness，则会产生漏报（false negatives）；牺牲一定completeness，则会产生误报（false positives）。
通常情况下，我们总是选择牺牲completeness，保全soundness。宁可有误报，也不漏掉一个正确结果。Soundness对编译器优化、程序验证等领域十分重要。
下面是一个简单的例子：
if (input) x = 1; else x = 0;
// x = ?
对于这行代码，下面是两种不同表述的分析结果：
- 当input为true时，x等于1；当input为false时，x等于0。
- x等于1或0。
这两个分析都是sound的。区别在于，前者precise，但expensive；后者imprecise，但cheap。静态分析通常需要尽力确保soundness，并在precision和speed之间做取舍。
Abstraction & Over-approximation
大多数静态分析可以用这两个词概括：abstraction和over-approximation，后者又包含transfer functions和control flows。
在这里老师举了一个例子来讲解：给定一个程序，确定其中所有变量的符号。Abstraction是指将变量从concrete domain映射到abstract domain，方便后续处理。Abstract domain就是符号集合。由于在程序中，变量很可能是不确定的（unknown）或非法、未定义（undefined）的，因此abstract domain包含五类符号：$+ - \Omicron \top \bot$，其中$\top$表示unknown，$\bot$表示undefined。这种映射如下图所示：
静态分析中over-approximation部分的transfer functions定义了怎样在abstract values上对程序语句求值。Transfer functions通常根据要分析的问题和程序语句相关的语义确定。对于算数运算，相关的transfer functions可以由算术运算规则和特性生成，例如（下图中左侧是transfer functions，右侧是在abstract domain上的运算结果）：
Over-approximation部分的control flows则指的是，在实际场景中进行控制流相关的静态分析时，由于无法枚举所有路径，我们通常采用flow merging（一种over-approximation的方式）来处理。
总结与思考
第一节课相对简单，但是很有意思。继续往后，看看程序分析是怎么玩的吧！