Static Analysis 01 - Basic Knowledge
# 前言
;
# XXX
通常来讲,对于一个给定的程序 ,静态分析的任务是在实际执行程序 之前尝试分析 (analyzes) 和推理 (reason about) 其行为,以判断 是否满足一些 属性 (properties) 。一些简单的例子包括:
Does dereference any null pointers ?
Are all cast operations in are safe ?
Can and in point to the same memory location ?
Is the piece of code in dead (so it could be eliminated) ?
Does contain any private information leaks ?
...
# 基本概念
# 莱斯定理
TBD.
# Sound and Complete
根据 莱斯定理 (Rice's Theorem) ,不存在任何方法能够 准确地 判断一个程序 是否满足一个 non-trivial property ,即不能给出一个 exact answer :Yes or No 。
我们定义这样的方法为 perfect static analysis ,其含义是既 sound 又 complete :这里引入的两个术语是静态分析的重要的基本概念。
如下图所示,可以把 sound, complete 以及 truth 想象成集合之间的包含关系:
truth 包含了所有正确的程序行为,例如程序中包含 10 个空指针引用。
sound 背后的含义是 over-approximate ,例如声称程序中包含 15 个空指针引用(内含 truth 中的 10 个)。换句话说,所有的 truth 都在 sound 的报告范围之内。
complete 背后的含义是 under-approximate ,例如声称程序中包含 5 个空指针引用(是 truth 中的 10 个之中的某 5 个)。换句话说,所有的 complete 都是 truth 。
尽管不存在 perfect static analysis ,但是可以有 useful static analysis ——实际的静态分析算法通常会对 sound 或 complete 之一进行妥协:
compromise soundness :允许静态分析的结果不包含所有的 truth ,也就是说,这种分析是 not sound 的,会产生 漏报 (false negatives) 。
compromise completeness :允许静态分析的结果不都是 truth ,也就是说,这种分析是 not complete 的,会产生 误报 (false positives) 。
事实上,实际的静态分析算法大多数是 sound, not complete 的。这是由静态分析的实际应用目标所决定的,例如:
编译器优化
程序验证
……
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01