Introduction

本系列笔记的课程地址：南京大学《软件分析》课程2020 (opens new window)

什么是静态分析：静态分析在 PL 研究领域下的划分以及其背景和挑战

为什么需要静态分析？

1. 程序可靠性
2. 程序安全性
3. 编译优化
4. 程序的理解

静态分析和莱斯定理

• SA 会分析一个程序 P，去推导 P 的一些行为和 properties
  • 内存泄漏、空指针、强制类型转换的安全、数据竞争、断言失败、无效代码等...（下面的 non-trivial properties）
• 莱斯（Rice)定理：Any non-trivial property of the behavior of programs in a r.e. language is undecidable.
  • r.e. (recursively enumerable)递归可枚举 = recognizable by a Turing-machine 能被图灵机识别
  • non-trivial properties 一般指 我们关心的、和运行时行为有关的一些 properies
  • 简单来说就是，这些我们一般会去关心的一些运行时的行为问题，例如空指针、内存泄漏等，静态分析是不能给出一个完成精确的答案的。

Perfect static analysis 是不存在的

• 何为 Perfect ？
  • Truth：满足 Sound and Complete，包含的内容就是所有可能的错误
• Sound：包含了所有真实错误，但也可能包含了误报的错误，即 Overapproximate
• Complete：包含了的错误全是真实错误，但可能漏报，即 Underapproximate
• 关系图：

• 根据 Rice 定理，完美的静态分析是不存在的，但我们可以进行 useful 的静态分析
  • 两种选择：1. 妥协 Soundness 2. 妥协 Completeness
  • Compromise soundness 会造成 false negative（漏报）
  • Compromise completeness 会造成 false positive（误报）⭐️
    • 大部分下更追求 sound 的静态分析
    • sound 一般会更被优先考虑，例如在 bug 检测里，满足了 soundness 意味着能检测出更多 bug

Static Analysis — Bird’s Eye View

if (input) {
	x = 1;
} else {
	x = 0;
}
x = ?

对于 x = ? 的分析，下面有两种分析结果：

1. input 为 true，则 x = 1；input 为 false，则 x = 0

   • 特点：sound，precise，expensive

2. x = 1 or x = 0

   • 特点：sound，imprecise，cheap

• 这两种结果都满足了 sound，但精确度和生成代价不同，往往就是在 precision 和 speed 之间做 trade-off

Static Analysis(most)：Abstraction + Over-approximation

• Abstraction，以下面的例子为例，在静态分析中我们所关心的 domain 往往不是程序中的 domain，我们要对程序中的具体域的值映射到抽象域

• Over-approximate

  1. Transfer Function 定义了如何在抽象值上去评估程序语句，它是由 “分析问题” 和 ”不同程序语句的语义“ 所定义的。
  • eg：以上面的正负为例
  
  2. Control Flows
  
  • 但实际情况下枚举所有路径往往是不太可能的，所以我们一般默认采用 flow merging

需要掌握的重点

1. 静态分析和（动态）测试的区别？
2. 理解 soundness，completeness，false negatives 和 false postives
3. 为什么 soundness 在静态分析中是必需的？
4. 如何理解 abstraction 和 over-approximation