– 尤其是对循环、递归等
主要思想是对代码进行“近似”，将不可判 定问题进行模拟
高级软件工程
静态代码的可信性分析概述 22/45
定理证明(Theorem Proving)
演绎方法（Deductive Methods） 基于Floyd/Hoare 逻辑 用如下形式表示程序的状态
{P} C {Q} C: 可执行代码 P: Pre-condition，执行前的状态属性 Q: Post-condition，执行后的状态属性 利用推理/证明机制解决 语句复合问题
高级软件工程
静态代码的可信性分析概述 12/45
三、静态代码缺陷查找的主要方法
1、静态代码分析 2、编译过程中的代码缺陷查找 3、形式化分析方法 4、缺陷模式匹配
高级软件工程
静态代码的可信性分析概述 13/45
1、静态代码分析
静态代码缺陷查找属于静态代码分析的范畴 静态代码分析是在不运行代码的前提下，获
– 抽象语法树 （AST）
类型检验
– 语义分析？ – 变量赋值、调用操作、类型变换 等
高级软件工程
静态代码的可信性分析概述 18/45
程序设计语言中的类型
某些具有相同/相似特性实例的集合
– 值的集合？操作的集合？
基本类型
– 整数、实数、枚举、字符、布尔
自定义
– 结构、抽象数据、面向对象 – 为什么要引入？便于理解？帮助人们发现错误！
例如：上面幂集格的高度是4。 一般地：格 (2A,⊆) 的高度是 |A|.
高级软件工程
静态代码的可信性分析概述 36/45
3、不动点（Fixed-Points）
一个函数 f : L → L 是单调的 (monotone), 当: ∀x, y ∈ S : x ⊑ y ⇒ f(x) ⊑ f(y)
单调函数不一定是递增的: 常量函数也是单调的
多个单调函数的复合仍然是单调函数 如果将 ⊔ 与 ⊓ 看作函数,则它们都是单调的
高级软件工程
静态代码的可信性分析概述 37/45
对于一个高度有限的格 L 每个单调函数 f 有唯一的一个最小不动点:
fix (f) = ⊔ f i (⊥) i0
取关于程序信息的过程
静态代码分析还可以用于
– 获取设计结构 – 理解代码功能 – 演化代码 – ……
高级软件工程
静态代码的可信性分析概述 14/45
给定一个程序，可以问许多问题：
• 对于某个输入，停机吗? • 执行过程需要多少内存? • 对于某个输入的输出是什么?
• 变量 x 被使用前是否已经初始化过了 • 变量 x 的值将来被读取吗? • 变量 x 的值是否一直大于0？ • 变量 x 的值取值范围是多少？ • 变量 x 的当前值是什么时候赋予的? • 指针p会是空吗?
主要的形式化方法包括：
模型检测(Model Checking) 抽象解释(Abstract Interpretation) 定理证明(Theorem Proving) 符号执行(Symbolic Execution)
高级软件工程
静态代码的可信性分析概述 20/45
模型检测
基于“有限状态自动机”理论
高级软件工程
静态代码的可信性分析概述 10/45
二、静态代码缺陷类别
与具体应用“无关”
– 词法或者语法 – 共性特性（死锁、空指针、内存泄露、数组越界） – 公共库用法（顺序、参数、接口实现，容错，安全）
与具体应用“相关”
– 类型定义（操作格式，不含其它信息（信息隐藏）） – 类型约束（调用的顺序、参数值，接口实现） – 需求相关（正确）
动态测试 在线监测
Product (Artifact)
Developing Process
Analyzing
Designing
Coding
Compiling Deploying Maintaining
高级软件工程
静态代码的可信性分析概述 7/45
动态测试
离线运行程序 应用最广泛的缺陷查找技术
高级软件工程
静态代码的可信性分析概述 5/45
内容
一、静态代码缺陷查找的角色 二、静态代码缺陷基本类别 三、静态代码缺陷查找的主要方法 四、静态代码缺陷查找的常见工具 五、理论基础：不动点
高级软件工程
静态代码的可信性分析概述 6/45
一、静态代码缺陷查找的角色 Review!
V&V
模型检测
静态分析
高级软件工程
静态代码的可信性分析概述 29/45
新的编程范型？
扩展类型思路 携带检验信息（头文件与配置文件）
– Java Annotation
高级软件工程
静态代码的可信性分析概述 30/45
五、理论基础：不动点
1、偏序 2、格 3、不动点
高级软件工程
静态代码的可信性分析概述 31/45
ASTREE PREfix
抽象解释(Abstract Interpretation) 符号执行(Symbolic Execution)
高级软件工程
静态代码的可信性分析概述 27/45
基于缺陷模式的主要工具
Jlint
主要采用数据流分析技术，速度快
没有误报
FindBugs 内置较多的缺陷模式
高级软件工程
静态代码的可信性分析概述 15/45
Rice 定理
Rice’s 定理 (1953) 非正式地指出： 所有关于程序“行为”的问题是不可判定的
(undecidable)
例如：能否判定如下变量 x 的值?
x = 17; if (TM(j)) x = 18;
第 j 个图灵机的停机问题是不可判定的
高级软件工程
静态代码的可信性分析概述 16/45
在完备、准确解难以求得的情况下
只能追求部分、近似解
这 是现实的道路
也是十分有用的道路
主要途径包括：
•类型检验 •形式化方法 •缺陷模式匹配
高级软件工程
静态代码的可信性分析概述 17/45
2、编译过程中的代码缺陷查找
最基本的代码分析 词法分析
语法分析
从代码中抽取有限状态转换系统模型， 用来表示目标系统的行为
适合检验“并发”等时序方面的特性 对于值域等类型的分析比较困难
– 状态爆炸
高级软件工程
静态代码的可信性分析概述 21/45
抽象解释
一种基于“格”理论的框架 许多形式化分析方法都可以被涵盖其中 主要适合 数据流分析（Data Flow Analysis）
4、缺陷模式匹配
事先收集足够多的共性缺陷模式 用户仅输入待检测代码就可以 与”类型化”方法关系密切 比较实用 容易产生“误报”
高级软件工程
静态代码的可信性分析概述 25/45
四、缺陷查找工具
准确？
– 漏报（False Negative, not Complete） – 误报（False Positive, not Sound）
高级软件工程
静态代码的可信性分析概述 1/45
第九讲
静态代码的可信性分析概述
高级软件工程
静态代码的可信性分析概述 2/45
从静态代码分析动态特性：
机能完整? 易生何病? 什么性格? 道德水准?
高级软件工程
静态代码的可信性分析概述 3/45
主要考虑如何发现代码缺陷！
需要首先知道： 可能存在什么样的代码缺陷！
1、偏序(partial order)
一个偏序是一个数学结构:
L = ( S, ⊑ ) 其中， S 是一个集合， ⊑ (小于等于) 是 S 上的一个二元关系， 且满足如下条件：
• 自反(Reflexivity):
∀x ∈ S : x ⊑ x
• 传递(Transitivity):
∀x, y, z ∈ S : x ⊑ y ∧ y ⊑ z ⇒ x ⊑ z
缺陷 与 约束:
什么是对的（约束：Constraint） 什么是不对的（缺陷：Defect）
高5
不论 是 人工 还是 自动
都需要： 利用 已有的缺陷知识 查找 某个特定程序
关于代码 你有什么样的先验知识？ 如何形式化描述这些知识？ 如何使用这些知识查找缺陷？
定义最小上界（least upper bound） ⊔X: X ⊑ ⊔X ∧ (∀y ∈ S : X ⊑ y ⇒ ⊔X ⊑ y)
定义最大下界 （greatest lower bound） ⊓X： ⊓X ⊑ X ∧ (∀y ∈ S : y ⊑ X ⇒ y ⊑ ⊓X)
高级软件工程
静态代码的可信性分析概述 33/45
高级软件工程
静态代码的可信性分析概述 34/45
哪些是格?
高级软件工程
静态代码的可信性分析概述 35/45
对于任何一个有限集合 A，可以定义一个格 (2A,⊆), 其 中， ⊥ = ∅, ⊤ = A, x ⊔ y = x ∪ y, x ⊓ y = x ∩ y
格的高度是从⊥ 到 ⊤ 的最长路径。
可以分析多种属性
– 死琐？安全漏洞?性能属性?
源码？目标码？
高级软件工程
静态代码的可信性分析概述 9/45
在线检测
当系统正在为用户提供服务时，一般不能 进行测试：输入受限
但可以进行检测，获取各种状态、事件 进行分析，并可能据此调整目标系统 尽量减少对系统的应用 与静态分析结合？
高级软件工程
静态代码的可信性分析概述 23/45
符号执行
通过使用抽象的符号表示程序中变量的 值来模拟程序的执行，克服了变量的值 难以确定的问题
跟踪各路径上变量的可能取值，有可能 发现细微的逻辑错误
程序较大时，可能的路径数目增长会很 快。可以选取重要的路径进行分析