第八讲 静态代码质量分析技术

从静态代码分析动态特性： 机能完整? 易生何病? 什么性格? 道德水准?

主要考虑如何发现代码缺陷！ 缺陷 与 约束: 需要首先知道： 可能存在什么样的代码缺陷！ 什么是对的（约束：Constraint） 需要首先知道： 可能存在什么样的代码缺陷！ 缺陷 与 约束: 什么是对的（约束：Constraint） 什么是不对的（缺陷：Defect）

关于代码 你有什么样的先验知识？ 如何形式化描述这些知识？ 如何使用这些知识查找缺陷？ 不论 是 人工 还是 自动 都需要： 利用 已有的缺陷知识 查找 某个特定程序 关于代码 你有什么样的先验知识？ 如何形式化描述这些知识？ 如何使用这些知识查找缺陷？

内 容 一、静态代码缺陷查找的角色 二、静态代码缺陷基本类别 三、静态代码缺陷查找的主要方法 四、静态代码缺陷查找的常见工具 内 容 一、静态代码缺陷查找的角色 二、静态代码缺陷基本类别 三、静态代码缺陷查找的主要方法 四、静态代码缺陷查找的常见工具 五、理论基础：不动点

一、静态代码缺陷查找的角色 Review! 静态分析 动态测试 在线监测 V&V 模型检测 Product (Artifact) Developing Process Coding Maintaining Analyzing Designing Compiling Deploying

动态测试 离线运行程序 应用最广泛的缺陷查找技术 基本分类 对功能性最有效 工作量大：微软（半数的测试人员？） 自动程度难以提高 黑盒 白盒 许多缺陷靠运行很难暴露：死琐等

静态缺陷查找 不运行程序(广义测试包含这类活动) 静态分析可以涉及更多的路径组合 可以分析多种属性 源码？目标码？ 测试一次只能有一个执行轨迹 可以分析多种属性 死琐？安全漏洞?性能属性? 源码？目标码？

在线检测 当系统正在为用户提供服务时，一般不能进行测试：输入受限 但可以进行检测，获取各种状态、事件 进行分析，并可能据此调整目标系统 尽量减少对系统的应用 与静态分析结合？

二、静态代码缺陷类别 与具体应用“无关” 与具体应用“相关” 词法或者语法 共性特性（死锁、空指针、内存泄露、数组越界） 公共库用法（顺序、参数、接口实现，容错，安全） 与具体应用“相关” 类型定义（操作格式，不含其它信息（信息隐藏）） 类型约束（调用的顺序、参数值，接口实现） 需求相关（正确）

如何得到这些知识？ 与具体应用无关 与具体应用相关 词法或者语法：语言设计人员 共性特性： 基础知识 公共库用法：库开发人员（形成文挡） 共性特性： 基础知识 公共库用法：库开发人员（形成文挡） 用户整理(分析实现代码、分析使用代码) 与具体应用相关 类型定义： 应用设计人员 类型约束： 应用设计人员、编程人员 需求相关： 用户

三、静态代码缺陷查找的主要方法 1、静态代码分析 2、编译过程中的代码缺陷查找 3、形式化分析方法 4、缺陷模式匹配

1、静态代码分析 静态代码缺陷查找属于静态代码分析的范畴 静态代码分析是在不运行代码的前提下，获取关于程序信息的过程 静态代码分析还可以用于 获取设计结构 理解代码功能 演化代码 ……

给定一个程序，可以问许多问题： • 对于某个输入，停机吗? • 执行过程需要多少内存? • 对于某个输入的输出是什么? • 变量 x 被使用前是否已经初始化过了 • 变量 x 的值将来被读取吗? • 变量 x 的值是否一直大于0？ • 变量 x 的值取值范围是多少？ • 变量 x 的当前值是什么时候赋予的? • 指针p会是空吗?

Rice 定理 Rice’s 定理 (1953) 非正式地指出： 所有关于程序“行为”的问题是不可判定的(undecidable) 例如：能否判定如下变量 x 的值? x = 17; if (TM(j)) x = 18; 第 j 个图灵机的停机问题是不可判定的 x的值也就不能判定

主要途径包括： 在完备、准确解难以求得的情况下 只能追求部分、近似解 这 是现实的道路 也是十分有用的道路 类型检验 形式化方法 缺陷模式匹配

2、编译过程中的代码缺陷查找 最基本的代码分析 词法分析 语法分析 类型检验 抽象语法树 （AST） 语义分析？ 变量赋值、调用操作、类型变换 等

程序设计语言中的类型 某些具有相同/相似特性实例的集合 基本类型 自定义 静态类型化语言 强类型化语言 值的集合？操作的集合？ 整数、实数、枚举、字符、布尔 自定义 结构、抽象数据、面向对象 为什么要引入？便于理解？帮助人们发现错误！ 静态类型化语言 每个表达式在静态程序分析时都是确定的 强类型化语言 所有表达式的类型是一致的（可以在运行时检验） 实际编写代码时，这是被编译器检查出来的一类常见错误！

3、形式化的软件分析方法 形式化软件分析是一种基于数学的“自动化”技术：给出一个特定行为的精确描述，该技术可以“准确地”对软件的语义进行推理 主要的形式化方法包括： 模型检测(Model Checking) 抽象解释(Abstract Interpretation) 定理证明(Theorem Proving) 符号执行(Symbolic Execution)

模型检测 基于“有限状态自动机”理论 从代码中抽取有限状态转换系统模型，用来表示目标系统的行为 适合检验“并发”等时序方面的特性 对于值域等类型的分析比较困难 状态爆炸

抽象解释 一种基于“格”理论的框架 许多形式化分析方法都可以被涵盖其中 主要适合 数据流分析（Data Flow Analysis） 尤其是对循环、递归等 主要思想是对代码进行“近似”，将不可判定问题进行模拟

定理证明(Theorem Proving) 演绎方法（Deductive Methods） 基于Floyd/Hoare 逻辑 用如下形式表示程序的状态 {P} C {Q} C: 可执行代码 P: Pre-condition，执行前的状态属性 Q: Post-condition，执行后的状态属性 利用推理/证明机制解决 语句复合问题

符号执行 通过使用抽象的符号表示程序中变量的值来模拟程序的执行，克服了变量的值难以确定的问题 跟踪各路径上变量的可能取值，有可能发现细微的逻辑错误 程序较大时，可能的路径数目增长会很快。可以选取重要的路径进行分析

4、缺陷模式匹配 事先收集足够多的共性缺陷模式 用户仅输入待检测代码就可以 与”类型化”方法关系密切 比较实用 容易产生“误报”

四、缺陷查找工具 准确？ 缺陷知识哪里来 基本方法 漏报（False Negative, not Complete） 误报（False Positive, not Sound） 缺陷知识哪里来 程序自带 工具提供 基本方法 基于形式化 基于缺陷模式

基于形式化方法的主要工具 JPF 模型检测 Bandera Slam, BLAST, CMC ESC/Java ASTREE PREfix 模型检测(Model Checking) 定理证明(Theorem Proving) 抽象解释(Abstract Interpretation) 符号执行(Symbolic Execution)

基于缺陷模式的主要工具 Jlint 主要采用数据流分析技术，速度快 没有误报 FindBugs 内置较多的缺陷模式 有较好的应用（google） PMD 格式为主，可以灵活增加新缺陷模式 以抽象语法树为基础建立 Coverify 主要针对操作系统 …… CODA 正在开发中……

工具发展的特点 各自优势不同 综合使用多种分析方法 在准确度与时间开销上进行折中 集成？

新的编程范型？ 扩展类型思路 携带检验信息（头文件与配置文件） Java Annotation

五、理论基础：不动点 1、偏序 2、格 3、不动点

1、偏序(partial order) 一个偏序是一个数学结构: L = ( S, ⊑ ) 其中， S 是一个集合， ⊑ (小于等于) 是 S 上的一个二元关系，且满足如下条件： • 自反(Reflexivity): ∀x ∈ S : x ⊑ x • 传递(Transitivity): ∀x, y, z ∈ S : x ⊑ y ∧ y ⊑ z ⇒ x ⊑ z • 反对称(Anti-symmetry): ∀x, y ∈ S : x ⊑ y ∧ y ⊑ x ⇒ x = y

y ∈ S 是X的上界(upper bound), 记作 X ⊑ y, 如果： ∀x ∈ X : x ⊑ y 类似地： 假设 X ⊆ S. y ∈ S 是X的上界(upper bound), 记作 X ⊑ y, 如果： ∀x ∈ X : x ⊑ y 类似地： y ∈ S 是 X 的下界(lower bound), 记作 y ⊑ X, 如果： ∀x ∈ X : y ⊑ x 定义最小上界（least upper bound） ⊔X: X ⊑ ⊔X ∧ (∀y ∈ S : X ⊑ y ⇒ ⊔X ⊑ y) 定义最大下界 （greatest lower bound） ⊓X： ⊓X ⊑ X ∧ (∀y ∈ S : y ⊑ X ⇒ y ⊑ ⊓X)

2、格（Lattice） 一个格是一个偏序集 S，且满足： 对于所有的子集 X ⊆ S， ⊔X 与 ⊓X 都存在 一个格一定有： 唯一的一个最大元素 ⊤ (top) ：⊤ = ⊔S 唯一的一个最小元素⊥(bottom)：⊥ = ⊓S. 由于最小上界和最大下界的唯一性，可以将求 x 和 y 的最小上界和最大下界定义为 x 和 y 的二元运算： 最小上界: x ⊔ y 最大下界: x ⊓ y 为什么？

哪些是格?

对于任何一个有限集合 A，可以定义一个格 (2A,⊆), 其中， ⊥ = ∅, ⊤ = A, x ⊔ y = x ∪ y, x ⊓ y = x ∩ y 格的高度是从⊥ 到 ⊤ 的最长路径。 例如：上面幂集格的高度是4。 一般地：格 (2A,⊆) 的高度是 |A|.

3、不动点（Fixed-Points） 一个函数 f : L → L 是单调的 (monotone), 当: ∀x, y ∈ S : x ⊑ y ⇒ f(x) ⊑ f(y) 单调函数不一定是递增的: 常量函数也是单调的 多个单调函数的复合仍然是单调函数 如果将 ⊔ 与 ⊓ 看作函数,则它们都是单调的

对于一个高度有限的格 L 每个单调函数 f 有唯一的一个最小不动点: fix (f) = ⊔ f i (⊥) i0 那么: f (fix (f)) = fix (f) 证明: 1) ⊥ ⊑ f (⊥) 2) f (⊥) ⊑ f 2 (⊥) 3) ⊥ ⊑ f (⊥) ⊑ f 2 (⊥) ⊑ …… 4) L 高度有限, 因此对于某个 k: f k (⊥) = f k+1 (⊥) 5) ……

计算一个不动点的时间复杂度依赖于 3 个因素: • 格的高度 • 计算 f 的代价; • 测试等价的代价. 一个不动点的计算可以表示为格中,从 ⊥ 开始向上搜索的过程

闭包性质(Closure Properties) 如果 L1,L2, . . . ,Ln 是有限高度的格,那么乘积( product)为: L1 × L2 × . . . × Ln = {(x1, x2, . . . , xn) | xi ∈ Li} 其中 ⊑ 是逐点对应的. ⊔ 与 ⊓ 可以被逐点计算 height (L1 × . . . ×Ln) = height (L1) + . . . + height (Ln)

L1 + L2 + . . . + Ln = {(i, xi) | xi ∈ Li\{⊥,⊤}} ∪ {⊥,⊤} 和操作: L1 + L2 + . . . + Ln = {(i, xi) | xi ∈ Li\{⊥,⊤}} ∪ {⊥,⊤} (i, x) ⊑ (j, y) 当且仅当: i = j 且 x ⊑ y. height (L1 + . . . + Ln) = max{height (Li)}.

如果 L 是一个有限高度的格, 那么 lift (L) 是: 高度： height (lift (L)) = height (L) + 1.

如果 A 是一个有限集合，那么 flat (A) : ⊤ a1 a2 … an ⊥ 是一个高度为2的格

A |→ L = {[a1 |→ x1, . . . , an |→ xn] | xi ∈ L} 有限高度的映射格 （map lattice） 定义为: A |→ L = {[a1 |→ x1, . . . , an |→ xn] | xi ∈ L} height (A |→ L) = |A| · height (L).

F(x1, . . . , xn) = (F1(x1, . . . , xn), . . . , Fn(x1, . . . , xn)) 如何利用不动点求解等式系统(systems of equations)? 假设 L 是一个高度有限的格,一个等式系统的形式为: x1 = F1(x1, . . . , xn) x2 = F2(x1, . . . , xn) ... xn = Fn(x1, . . . , xn) xi 是变量 Fi : Ln → L 是单调函数集合 每个这样的系统有一个唯一的最小解,且是函数 F 的最小不动点. F : Ln → Ln defined by: F(x1, . . . , xn) = (F1(x1, . . . , xn), . . . , Fn(x1, . . . , xn))

我们还可以类似地求解不等式: x1 ⊑ F1(x1, . . . , xn) x2 ⊑ F2(x1, . . . , xn) ... xn ⊑ Fn(x1, . . . , xn) 通过观察: x ⊑ y 等价于 x = x ⊓ y 这样，上述不等式可以转换为: x1 = x1 ⊓ F1(x1, . . . , xn) x2 = x2 ⊓ F2(x1, . . . , xn) xn = xn ⊓ Fn(x1, . . . , xn) 这是一个与前面类似的单调函数等式系统 Why?