第九讲静态代码的可信性分析概述

1、静态代码的可信性分析概述静态代码的可信性分析概述 1/45高级软件工程高级软件工程静态代码的可信性分析概述静态代码的可信性分析概述 2/45高级软件工程高级软件工程机能完整机能完整?易生何病易生何病?什么性格什么性格?道德水准道德水准?从静态代码分析动态特性：从静态代码分析动态特性：静态代码的可信性分析概述静态代码的可信性分析概述 3/45高级软件工程高级软件工程主要考虑如何发现代码缺陷！主要考虑如何发现代码缺陷！需要首先知道：需要首先知道： 可能存在什么样的代码缺陷！可能存在什么样的代码缺陷！缺陷缺陷 与与 约束约束: 什么是对的（约束：什么是对的（约束：Constraint） 什么是不对的

2、（缺陷：什么是不对的（缺陷：Defect）静态代码的可信性分析概述静态代码的可信性分析概述 4/45高级软件工程高级软件工程不论不论 是是 人工人工 还是还是 自动自动都需要：都需要： 利用利用 已有的缺陷知识已有的缺陷知识 查找查找 某个特定程序某个特定程序静态代码的可信性分析概述静态代码的可信性分析概述 5/45高级软件工程高级软件工程内内 容容一、静态代码缺陷查找的角色一、静态代码缺陷查找的角色二、静态代码缺陷基本类别二、静态代码缺陷基本类别三、静态代码缺陷查找的主要方法三、静态代码缺陷查找的主要方法 四、静态代码缺陷查找的常见工具四、静态代码缺陷查找的常见工具五、理论基础：不动点五、理

3、论基础：不动点静态代码的可信性分析概述静态代码的可信性分析概述 6/45高级软件工程高级软件工程Product (Artifact)AnalyzingDesigningCodingCompilingDeployingDeveloping ProcessMaintaining静态分析静态分析动态测试动态测试模型检测模型检测在线监测在线监测V&V一、静态代码缺陷查找的角色一、静态代码缺陷查找的角色Review!静态代码的可信性分析概述静态代码的可信性分析概述 7/45高级软件工程高级软件工程l离线运行程序l应用最广泛的缺陷查找技术对功能性最有效工作量大：微软（半数的测试人员？）自动程度难以

4、提高l基本分类黑盒白盒许多缺陷靠运行很难暴露：死琐等许多缺陷靠运行很难暴露：死琐等静态代码的可信性分析概述静态代码的可信性分析概述 8/45高级软件工程高级软件工程l不运行程序(广义测试包含这类活动)l静态分析可以涉及更多的路径组合测试一次只能有一个执行轨迹l可以分析多种属性死琐？安全漏洞?性能属性?l源码？目标码？静态代码的可信性分析概述静态代码的可信性分析概述 9/45高级软件工程高级软件工程l当系统正在为用户提供服务时，一般不能当系统正在为用户提供服务时，一般不能进行测试：输入受限进行测试：输入受限l但可以进行检测，获取各种状态、事件但可以进行检测，获取各种状态、事件l进行分析，并可能据

5、此调整目标系统进行分析，并可能据此调整目标系统l尽量减少对系统的应用尽量减少对系统的应用l与静态分析结合？与静态分析结合？静态代码的可信性分析概述静态代码的可信性分析概述 10/45高级软件工程高级软件工程二、静态代码缺陷类别二、静态代码缺陷类别l与具体应用“无关”词法或者语法共性特性（共性特性（死锁、空指针、内存泄露、数组越界死锁、空指针、内存泄露、数组越界）公共库用法（公共库用法（顺序、参数、接口实现，容错，安全顺序、参数、接口实现，容错，安全）l与具体应用“相关”类型定义（操作格式，不含其它信息（信息隐藏）类型约束（类型约束（调用的顺序、参数值，接口实现调用的顺序、参数值，接口实现）需求

6、相关（正确）静态代码的可信性分析概述静态代码的可信性分析概述 11/45高级软件工程高级软件工程l与具体应用无关与具体应用无关词法或者语法：语言设计人员词法或者语法：语言设计人员 共性特性：共性特性： 基础知识基础知识 公共库用法：库开发人员（形成文挡）公共库用法：库开发人员（形成文挡） 用户整理用户整理(分析实现代码、分析使用代码分析实现代码、分析使用代码) l与具体应用相关与具体应用相关类型定义：类型定义： 应用设计人员应用设计人员类型约束：类型约束： 应用设计人员、编程人员应用设计人员、编程人员需求相关：需求相关： 用户用户静态代码的可信性分析概述静态代码的可信性分析概述 12/45高级

7、软件工程高级软件工程1、静态代码分析2、编译过程中的代码缺陷查找3、形式化分析方法4、缺陷模式匹配三、静态代码缺陷查找的主要方法三、静态代码缺陷查找的主要方法静态代码的可信性分析概述静态代码的可信性分析概述 13/45高级软件工程高级软件工程l静态代码缺陷查找属于静态代码分析的范畴l静态代码分析是在不运行代码的前提下，获取关于程序信息的过程l静态代码分析还可以用于获取设计结构理解代码功能演化代码1、静态代码分析、静态代码分析静态代码的可信性分析概述静态代码的可信性分析概述 14/45高级软件工程高级软件工程给定一个程序，可以问许多问题：给定一个程序，可以问许多问题： 对于某个输入，停机吗对于某

8、个输入，停机吗? 执行过程需要多少内存执行过程需要多少内存? 对于某个输入的输出是什么对于某个输入的输出是什么? 变量 x 被使用前是否已经初始化过了 变量 x 的值将来被读取吗? 变量 x 的值是否一直大于0？ 变量 x 的值取值范围是多少？ 变量 x 的当前值是什么时候赋予的? 指针p会是空吗?静态代码的可信性分析概述静态代码的可信性分析概述 15/45高级软件工程高级软件工程Rices 定理定理 (1953) 非正式地指出：非正式地指出：所有关于程序所有关于程序“行为行为”的问题是不可判定的的问题是不可判定的(undecidable)例如：能否判定如下变量例如：能否判定如下变量 x 的值

9、的值?x = 17; if (TM(j) x = 18;第第 j 个图灵机的停机问题是不可判定的个图灵机的停机问题是不可判定的x的值也就不能判定的值也就不能判定静态代码的可信性分析概述静态代码的可信性分析概述 16/45高级软件工程高级软件工程在完备、准确解难以求得的情况下只能追求部分、近似解这 是现实的道路 也是十分有用的道路主要途径包括：类型检验形式化方法缺陷模式匹配静态代码的可信性分析概述静态代码的可信性分析概述 17/45高级软件工程高级软件工程最基本的代码分析l词法分析l语法分析抽象语法树 （AST）l类型检验语义分析？变量赋值、调用操作、类型变换 等静态代码的可信性分析概述静态代码

10、的可信性分析概述 18/45高级软件工程高级软件工程l某些具有相同某些具有相同/相似特性实例的集合相似特性实例的集合值的集合？操作的集合？值的集合？操作的集合？l基本类型基本类型整数、实数、枚举、字符、布尔整数、实数、枚举、字符、布尔l自定义自定义结构、抽象数据、面向对象结构、抽象数据、面向对象为什么要引入？便于理解？为什么要引入？便于理解？帮助人们发现错误！帮助人们发现错误！l静态类型化语言静态类型化语言每个表达式在静态程序分析时都是确定的每个表达式在静态程序分析时都是确定的l强类型化语言强类型化语言所有表达式的类型是一致的（可以在运行时检验）所有表达式的类型是一致的（可以在运行时检验）实际

11、编写代码时，这是被编译器检查出来的一类常见错误！实际编写代码时，这是被编译器检查出来的一类常见错误！静态代码的可信性分析概述静态代码的可信性分析概述 19/45高级软件工程高级软件工程形式化软件分析是一种基于数学的“自动化”技术：给出一个特定行为的精确描述，该技术可以“准确地”对软件的语义进行推理(Model Checking)抽象解释(Abstract Interpretation)定理证明(Theorem Proving)符号执行(Symbolic Execution)静态代码的可信性分析概述静态代码的可信性分析概述 20/45高级软件工程高级软件工程l基于“有限状态自动机”理论l从代码中

12、抽取有限状态转换系统模型，用来表示目标系统的行为l适合检验“并发”等时序方面的特性l对于值域等类型的分析比较困难状态爆炸静态代码的可信性分析概述静态代码的可信性分析概述 21/45高级软件工程高级软件工程抽象解释抽象解释l一种基于“格”理论的框架l许多形式化分析方法都可以被涵盖其中l主要适合 数据流分析（Data Flow Analysis）尤其是对循环、递归等l主要思想是对代码进行“近似”，将不可判定问题进行模拟静态代码的可信性分析概述静态代码的可信性分析概述 22/45高级软件工程高级软件工程定理证明定理证明(Theorem Proving)l演绎方法（Deductive Methods）

13、l基于Floyd/Hoare 逻辑l用如下形式表示程序的状态P C Q C: 可执行代码 P: Pre-condition，执行前的状态属性 Q: Post-condition，执行后的状态属性l利用推理/证明机制解决 语句复合问题静态代码的可信性分析概述静态代码的可信性分析概述 23/45高级软件工程高级软件工程l通过使用抽象的符号表示程序中变量的值来模拟程序的执行，克服了变量的值难以确定的问题l跟踪各路径上变量的可能取值，有可能发现细微的逻辑错误l程序较大时，可能的路径数目增长会很快。可以选取重要的路径进行分析静态代码的可信性分析概述静态代码的可信性分析概述 24/45高级软件工程高级软件

14、工程l事先收集足够多的共性缺陷模式事先收集足够多的共性缺陷模式l用户仅输入待检测代码就可以用户仅输入待检测代码就可以l与与”类型化类型化”方法关系密切方法关系密切l比较实用比较实用l容易产生容易产生“误报误报”静态代码的可信性分析概述静态代码的可信性分析概述 25/45高级软件工程高级软件工程l准确？准确？漏报（漏报（False Negative, not Complete）误报（误报（False Positive, not Sound）l缺陷知识哪里来缺陷知识哪里来程序自带程序自带工具提供工具提供l基本方法基本方法基于形式化基于形式化基于缺陷模式基于缺陷模式静态代码的可信性分析概述静态代码的

15、可信性分析概述 26/45高级软件工程高级软件工程lJPF 模型检测lBandera lSlam, BLAST, CMClESC/JavalASTREElPREfix定理证明定理证明(Theorem Proving)模型检测模型检测(Model Checking)抽象解释抽象解释(Abstract Interpretation)符号执行符号执行(Symbolic Execution)静态代码的可信性分析概述静态代码的可信性分析概述 27/45高级软件工程高级软件工程lJlint 主要采用数据流分析技术，速度快 没有误报lFindBugs 内置较多的缺陷模式 有较好的应用（google）lPMD

16、 格式为主，可以灵活增加新缺陷模式 以抽象语法树为基础建立 lCoverify 主要针对操作系统lCODA 正在开发中静态代码的可信性分析概述静态代码的可信性分析概述 28/45高级软件工程高级软件工程l各自优势不同l综合使用多种分析方法l在准确度与时间开销上进行折中l集成？静态代码的可信性分析概述静态代码的可信性分析概述 29/45高级软件工程高级软件工程l扩展类型思路l携带检验信息（头文件与配置文件）Java Annotation静态代码的可信性分析概述静态代码的可信性分析概述 30/45高级软件工程高级软件工程五、理论基础：不动点五、理论基础：不动点1、偏序2、格3、不动点静态代码的可信

17、性分析概述静态代码的可信性分析概述 31/45高级软件工程高级软件工程一个偏序是一个数学结构一个偏序是一个数学结构: 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静态代码的可信性分析概述静态代码的可信性分析概述 32/45高级软件工程高级软件工程假设 X S

18、. 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)静态代码的可信性分析概述静态代码的可信性分析概述 33/45高级软件工程高级软件工程一个格是一个偏序集一个格是一个偏序集 S，且满足：，且满足： 对于所有的子集对于所有的子集 X S， X 与与 X 都存

19、在都存在一个格一定有： 唯一的一个最大元素 (top) ： = S 唯一的一个最小元素(bottom)： = S.由于最小上界和最大下界的唯一性，可以将求 x 和 y 的最小上界和最大下界定义为 x 和 y 的二元运算：最小上界: x y 最大下界: x y为什么？为什么？静态代码的可信性分析概述静态代码的可信性分析概述 34/45高级软件工程高级软件工程静态代码的可信性分析概述静态代码的可信性分析概述 35/45高级软件工程高级软件工程l对于任何一个有限集合 A，可以定义一个格 (2A,), 其中， = , = A, x y = x y, x y = x y 格的高度是从 到 的最长路径。例

20、如：上面幂集格的高度是4。一般地：格 (2A,) 的高度是 |A|.静态代码的可信性分析概述静态代码的可信性分析概述 36/45高级软件工程高级软件工程一个函数 f : L L 是单调的 (monotone), 当:x, y S : x y f(x) f(y)单调函数不一定是递增的:常量函数也是单调的多个单调函数的复合仍然是单调函数如果将 与 看作函数,则它们都是单调的静态代码的可信性分析概述静态代码的可信性分析概述 37/45高级软件工程高级软件工程对于一个高度有限的格 L 每个单调函数 f 有唯一的一个最小不动点: fix (f) = f i () i0那么: f (fix (f) = f

21、ix (f)证明: 1) f () 2) f () f 2 () 3) f () f 2 () 4) L 高度有限, 因此对于某个 k: f k () = f k+1 () 5) 静态代码的可信性分析概述静态代码的可信性分析概述 38/45高级软件工程高级软件工程计算一个不动点的时间复杂度依赖于 3 个因素: 格的高度 计算 f 的代价; 测试等价的代价.一个不动点的计算可以表示为格中,从 开始向上搜索的过程静态代码的可信性分析概述静态代码的可信性分析概述 39/45高级软件工程高级软件工程如果 L1,L2, . . . ,Ln 是有限高度的格,那么乘积( product)为为:L1 L2 .

22、 . . Ln = (x1, x2, . . . , xn) | xi Li其中 是逐点对应的. 与 可以被逐点计算height (L1 . . . Ln) = height (L1) + . . . + height (Ln)静态代码的可信性分析概述静态代码的可信性分析概述 40/45高级软件工程高级软件工程和操作:L1 + L2 + . . . + Ln = (i, xi) | xi Li, , (i, x) (j, y) 当且仅当: i = j 且 x y. height (L1 + . . . + Ln) = maxheight (Li).静态代码的可信性分析概述静态代码的可信性分析概述 41/45高级软件工程高级软件工程如果 L 是一个有限高度的格, 那么 lift (L) 是:高度： height (lift (L) = height (L) + 1.静态代码的可信性分析概述静态代码的可信性分析概述 42/45高级软件工程高级软件工程如果 A 是一个有限集合，那么 flat (A) :a1 a2 an 是一个高度为2的格静态代码的可信性分析概述静态代码