《第九讲静态代码的可信性分析概述》由会员分享，可在线阅读，更多相关《第九讲静态代码的可信性分析概述（45页珍藏版）》请在金锄头文库上搜索。
1、静态代码的可信性分析概述静态代码的可信性分析概述 1/45高级软件工程高级软件工程第九讲第九讲静态代码的可信性分析概述静态代码的可信性分析概述1静态代码的可信性分析概述静态代码的可信性分析概述 2/45高级软件工程高级软件工程机能完整机能完整?易生何病易生何病?什么性格什么性格?道德水准道德水准?从静态代码分析动态特性：从静态代码分析动态特性：2静态代码的可信性分析概述静态代码的可信性分析概述 3/45高级软件工程高级软件工程主要考虑如何发现代码缺陷！主要考虑如何发现代码缺陷！需要首先知道：需要首先知道： 可能存在什么样的代码缺陷！可能存在什么样的代码缺陷！缺陷缺陷 与与 约束约束: 什么是对
2、的（约束：什么是对的（约束：Constraint） 什么是不对的（缺陷：什么是不对的（缺陷：Defect）3静态代码的可信性分析概述静态代码的可信性分析概述 4/45高级软件工程高级软件工程关于代码关于代码你有什么样的先验知识？你有什么样的先验知识？如何形式化描述这些知识？如何形式化描述这些知识？如何使用这些知识查找缺陷？如何使用这些知识查找缺陷？不论不论 是是 人工人工 还是还是 自动自动都需要：都需要： 利用利用 已有的缺陷知识已有的缺陷知识 查找查找 某个特定程序某个特定程序4静态代码的可信性分析概述静态代码的可信性分析概述 5/45高级软件工程高级软件工程内内 容容一、静态代码缺陷查找
3、的角色一、静态代码缺陷查找的角色二、静态代码缺陷基本类别二、静态代码缺陷基本类别三、静态代码缺陷查找的主要方法三、静态代码缺陷查找的主要方法 四、静态代码缺陷查找的常见工具四、静态代码缺陷查找的常见工具五、理论基础：不动点五、理论基础：不动点5静态代码的可信性分析概述静态代码的可信性分析概述 6/45高级软件工程高级软件工程Product (Artifact)AnalyzingDesigningCodingCompilingDeployingDeveloping ProcessMaintaining静态分析静态分析动态测试动态测试模型检测模型检测在线监测在线监测V&V一、静态代码缺陷查找的角色
4、一、静态代码缺陷查找的角色Review!6静态代码的可信性分析概述静态代码的可信性分析概述 7/45高级软件工程高级软件工程 动态测试动态测试l离线运行程序l应用最广泛的缺陷查找技术对功能性最有效工作量大：微软（半数的测试人员？）自动程度难以提高l基本分类黑盒白盒许多缺陷靠运行很难暴露：死琐等许多缺陷靠运行很难暴露：死琐等7静态代码的可信性分析概述静态代码的可信性分析概述 8/45高级软件工程高级软件工程静态缺陷查找静态缺陷查找l不运行程序(广义测试包含这类活动)l静态分析可以涉及更多的路径组合测试一次只能有一个执行轨迹l可以分析多种属性死琐？安全漏洞?性能属性?l源码？目标码？8静态代码的可
5、信性分析概述静态代码的可信性分析概述 9/45高级软件工程高级软件工程在线检测在线检测l当系统正在为用户提供服务时，一般不能进当系统正在为用户提供服务时，一般不能进行测试：输入受限行测试：输入受限l但可以进行检测，获取各种状态、事件但可以进行检测，获取各种状态、事件l进行分析，并可能据此调整目标系统进行分析，并可能据此调整目标系统l尽量减少对系统的应用尽量减少对系统的应用l与静态分析结合？与静态分析结合？9静态代码的可信性分析概述静态代码的可信性分析概述 10/45高级软件工程高级软件工程二、静态代码缺陷类别二、静态代码缺陷类别l与具体应用“无关”词法或者语法共性特性（共性特性（死锁、空指针、
6、内存泄露、数组越界死锁、空指针、内存泄露、数组越界）公共库用法（公共库用法（顺序、参数、接口实现，容错，安全顺序、参数、接口实现，容错，安全）l与具体应用“相关”类型定义（操作格式，不含其它信息（信息隐藏）类型约束（类型约束（调用的顺序、参数值，接口实现调用的顺序、参数值，接口实现）需求相关（正确）10静态代码的可信性分析概述静态代码的可信性分析概述 11/45高级软件工程高级软件工程l与具体应用无关与具体应用无关词法或者语法：语言设计人员词法或者语法：语言设计人员 共性特性：共性特性： 基础知识基础知识 公共库用法：库开发人员（形成文挡）公共库用法：库开发人员（形成文挡） 用户整理用户整理(
7、分析实现代码、分析使用代码分析实现代码、分析使用代码) l与具体应用相关与具体应用相关类型定义：类型定义： 应用设计人员应用设计人员类型约束：类型约束： 应用设计人员、编程人员应用设计人员、编程人员需求相关：需求相关： 用户用户如何得到这些知识？如何得到这些知识？11静态代码的可信性分析概述静态代码的可信性分析概述 12/45高级软件工程高级软件工程1、静态代码分析2、编译过程中的代码缺陷查找3、形式化分析方法4、缺陷模式匹配三、静态代码缺陷查找的主要方法三、静态代码缺陷查找的主要方法12静态代码的可信性分析概述静态代码的可信性分析概述 13/45高级软件工程高级软件工程l静态代码缺陷查找属于
8、静态代码分析的范畴l静态代码分析是在不运行代码的前提下，获取关于程序信息的过程l静态代码分析还可以用于获取设计结构理解代码功能演化代码1、静态代码分析、静态代码分析13静态代码的可信性分析概述静态代码的可信性分析概述 14/45高级软件工程高级软件工程给定一个程序，可以问许多问题：给定一个程序，可以问许多问题： 对于某个输入，停机吗对于某个输入，停机吗? 执行过程需要多少内存执行过程需要多少内存? 对于某个输入的输出是什么对于某个输入的输出是什么? 变量 x 被使用前是否已经初始化过了 变量 x 的值将来被读取吗? 变量 x 的值是否一直大于0？ 变量 x 的值取值范围是多少？ 变量 x 的当
9、前值是什么时候赋予的? 指针p会是空吗?14静态代码的可信性分析概述静态代码的可信性分析概述 15/45高级软件工程高级软件工程Rice 定理定理Rices 定理定理 (1953) 非正式地指出：非正式地指出：所有关于程序所有关于程序“行为行为”的问题是不可判定的的问题是不可判定的(undecidable)例如：能否判定如下变量例如：能否判定如下变量 x 的值的值?x = 17; if (TM(j) x = 18;第第 j 个图灵机的停机问题是不可判定的个图灵机的停机问题是不可判定的x的值也就不能判定的值也就不能判定15静态代码的可信性分析概述静态代码的可信性分析概述 16/45高级软件工程高
10、级软件工程在完备、准确解难以求得的情况下只能追求部分、近似解这 是现实的道路 也是十分有用的道路主要途径包括：类型检验形式化方法缺陷模式匹配16静态代码的可信性分析概述静态代码的可信性分析概述 17/45高级软件工程高级软件工程2、编译过程中的代码缺陷查找、编译过程中的代码缺陷查找最基本的代码分析l词法分析l语法分析抽象语法树 （AST）l类型检验语义分析？变量赋值、调用操作、类型变换 等17静态代码的可信性分析概述静态代码的可信性分析概述 18/45高级软件工程高级软件工程程序设计语言中的类型程序设计语言中的类型l某些具有相同某些具有相同/相似特性实例的集合相似特性实例的集合值的集合？操作的
11、集合？值的集合？操作的集合？l基本类型基本类型整数、实数、枚举、字符、布尔整数、实数、枚举、字符、布尔l自定义自定义结构、抽象数据、面向对象结构、抽象数据、面向对象为什么要引入？便于理解？为什么要引入？便于理解？帮助人们发现错误！帮助人们发现错误！l静态类型化语言静态类型化语言每个表达式在静态程序分析时都是确定的每个表达式在静态程序分析时都是确定的l强类型化语言强类型化语言所有表达式的类型是一致的（可以在运行时检验）所有表达式的类型是一致的（可以在运行时检验）实际编写代码时，这是被编译器检查出来的一类常见错误！实际编写代码时，这是被编译器检查出来的一类常见错误！18静态代码的可信性分析概述静态
12、代码的可信性分析概述 19/45高级软件工程高级软件工程3、形式化的软件分析方法、形式化的软件分析方法形式化软件分析是一种基于数学的“自动化”技术：给出一个特定行为的精确描述，该技术可以“准确地”对软件的语义进行推理主要的形式化方法包括：主要的形式化方法包括：模型检测模型检测(Model Checking)抽象解释(Abstract Interpretation)定理证明(Theorem Proving)符号执行(Symbolic Execution)19静态代码的可信性分析概述静态代码的可信性分析概述 20/45高级软件工程高级软件工程l基于“有限状态自动机”理论l从代码中抽取有限状态转换系
13、统模型，用来表示目标系统的行为l适合检验“并发”等时序方面的特性l对于值域等类型的分析比较困难状态爆炸模型检测模型检测20静态代码的可信性分析概述静态代码的可信性分析概述 21/45高级软件工程高级软件工程抽象解释抽象解释l一种基于“格”理论的框架l许多形式化分析方法都可以被涵盖其中l主要适合 数据流分析（Data Flow Analysis）尤其是对循环、递归等l主要思想是对代码进行“近似”，将不可判定问题进行模拟21静态代码的可信性分析概述静态代码的可信性分析概述 22/45高级软件工程高级软件工程定理证明定理证明(Theorem Proving)l演绎方法（Deductive Metho
14、ds）l基于Floyd/Hoare 逻辑l用如下形式表示程序的状态P C Q C: 可执行代码 P: Pre-condition，执行前的状态属性 Q: Post-condition，执行后的状态属性l利用推理/证明机制解决 语句复合问题22静态代码的可信性分析概述静态代码的可信性分析概述 23/45高级软件工程高级软件工程符号执行符号执行l通过使用抽象的符号表示程序中变量的值来模拟程序的执行，克服了变量的值难以确定的问题l跟踪各路径上变量的可能取值，有可能发现细微的逻辑错误l程序较大时，可能的路径数目增长会很快。可以选取重要的路径进行分析23静态代码的可信性分析概述静态代码的可信性分析概述
15、24/45高级软件工程高级软件工程4、缺陷模式匹配、缺陷模式匹配l事先收集足够多的共性缺陷模式事先收集足够多的共性缺陷模式l用户仅输入待检测代码就可以用户仅输入待检测代码就可以l与与”类型化类型化”方法关系密切方法关系密切l比较实用比较实用l容易产生容易产生“误报误报”24静态代码的可信性分析概述静态代码的可信性分析概述 25/45高级软件工程高级软件工程四、缺陷查找工具四、缺陷查找工具l准确？准确？漏报（漏报（False Negative, not Complete）误报（误报（False Positive, not Sound）l缺陷知识哪里来缺陷知识哪里来程序自带程序自带工具提供工具提供
16、l基本方法基本方法基于形式化基于形式化基于缺陷模式基于缺陷模式25静态代码的可信性分析概述静态代码的可信性分析概述 26/45高级软件工程高级软件工程基于形式化方法的主要工具基于形式化方法的主要工具lJPF 模型检测lBandera lSlam, BLAST, CMClESC/JavalASTREElPREfix定理证明定理证明(Theorem Proving)模型检测模型检测(Model Checking)抽象解释抽象解释(Abstract Interpretation)符号执行符号执行(Symbolic Execution)26静态代码的可信性分析概述静态代码的可信性分析概述 27/45高
17、级软件工程高级软件工程基于缺陷模式的主要工具基于缺陷模式的主要工具lJlint 主要采用数据流分析技术，速度快 没有误报lFindBugs 内置较多的缺陷模式 有较好的应用（google）lPMD 格式为主，可以灵活增加新缺陷模式 以抽象语法树为基础建立 lCoverify 主要针对操作系统lCODA 正在开发中27静态代码的可信性分析概述静态代码的可信性分析概述 28/45高级软件工程高级软件工程工具发展的特点工具发展的特点l各自优势不同l综合使用多种分析方法l在准确度与时间开销上进行折中l集成？28静态代码的可信性分析概述静态代码的可信性分析概述 29/45高级软件工程高级软件工程新的编程
18、范型？新的编程范型？l扩展类型思路l携带检验信息（头文件与配置文件）Java Annotation29静态代码的可信性分析概述静态代码的可信性分析概述 30/45高级软件工程高级软件工程五、理论基础：不动点五、理论基础：不动点1、偏序2、格3、不动点30静态代码的可信性分析概述静态代码的可信性分析概述 31/45高级软件工程高级软件工程一个偏序是一个数学结构一个偏序是一个数学结构: L = ( S, )其中，其中， S 是一个集合，是一个集合， (小于等于小于等于) 是是 S 上的一个二元上的一个二元关系关系，且满足如下条件：且满足如下条件： 自反(Reflexivity): x S : x
19、x 传递(Transitivity): x, y, z S : x y y z x z 反对称(Anti-symmetry): x, y S : x y y x x = y1、偏序、偏序(partial order)31静态代码的可信性分析概述静态代码的可信性分析概述 32/45高级软件工程高级软件工程假设 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
20、X y)定义最大下界 （greatest lower bound） X： X X (y S : y X y X)32静态代码的可信性分析概述静态代码的可信性分析概述 33/45高级软件工程高级软件工程2、格（、格（Lattice）一个格是一个偏序集一个格是一个偏序集 S，且满足：，且满足： 对于所有的子集对于所有的子集 X S， X 与与 X 都存在都存在一个格一定有： 唯一的一个最大元素 (top) ： = S 唯一的一个最小元素(bottom)： = S.由于最小上界和最大下界的唯一性，可以将求 x 和 y 的最小上界和最大下界定义为 x 和 y 的二元运算：最小上界: x y 最大下界:
21、 x y为什么？为什么？33静态代码的可信性分析概述静态代码的可信性分析概述 34/45高级软件工程高级软件工程哪些是格哪些是格?34静态代码的可信性分析概述静态代码的可信性分析概述 35/45高级软件工程高级软件工程l对于任何一个有限集合 A，可以定义一个格 (2A,), 其中， = , = A, x y = x y, x y = x y 格的高度是从 到 的最长路径。例如：上面幂集格的高度是4。一般地：格 (2A,) 的高度是 |A|.35静态代码的可信性分析概述静态代码的可信性分析概述 36/45高级软件工程高级软件工程3、不动点（、不动点（Fixed-Points）一个函数 f : L
22、 L 是单调的 (monotone), 当:x, y S : x y f(x) f(y)单调函数不一定是递增的:常量函数也是单调的多个单调函数的复合仍然是单调函数如果将 与 看作函数,则它们都是单调的36静态代码的可信性分析概述静态代码的可信性分析概述 37/45高级软件工程高级软件工程对于一个高度有限的格 L 每个单调函数 f 有唯一的一个最小不动点: fix (f) = f i () i0那么: f (fix (f) = fix (f)证明: 1) f () 2) f () f 2 () 3) f () f 2 () 4) L 高度有限, 因此对于某个 k: f k () = f k+1
23、() 5) 37静态代码的可信性分析概述静态代码的可信性分析概述 38/45高级软件工程高级软件工程计算一个不动点的时间复杂度依赖于 3 个因素: 格的高度 计算 f 的代价; 测试等价的代价.一个不动点的计算可以表示为格中,从 开始向上搜索的过程38静态代码的可信性分析概述静态代码的可信性分析概述 39/45高级软件工程高级软件工程闭包性质闭包性质(Closure Properties)如果 L1,L2, . . . ,Ln 是有限高度的格,那么乘积( product)为为:L1 L2 . . . Ln = (x1, x2, . . . , xn) | xi Li其中 是逐点对应的. 与 可
24、以被逐点计算height (L1 . . . Ln) = height (L1) + . . . + height (Ln)39静态代码的可信性分析概述静态代码的可信性分析概述 40/45高级软件工程高级软件工程和操作:L1 + L2 + . . . + Ln = (i, xi) | xi Li, , (i, x) (j, y) 当且仅当: i = j 且 x y. height (L1 + . . . + Ln) = maxheight (Li).40静态代码的可信性分析概述静态代码的可信性分析概述 41/45高级软件工程高级软件工程如果 L 是一个有限高度的格, 那么 lift (L) 是
25、:高度： height (lift (L) = height (L) + 1.41静态代码的可信性分析概述静态代码的可信性分析概述 42/45高级软件工程高级软件工程如果 A 是一个有限集合，那么 flat (A) :a1 a2 an 是一个高度为2的格42静态代码的可信性分析概述静态代码的可信性分析概述 43/45高级软件工程高级软件工程有限高度的映射格 （map lattice） 定义为:A | L = a1 | x1, . . . , an | xn | xi Lheight (A | L) = |A| height (L).43静态代码的可信性分析概述静态代码的可信性分析概述 44/4
26、5高级软件工程高级软件工程如何利用不动点求解等式系统如何利用不动点求解等式系统(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,
27、 . . . , xn)44静态代码的可信性分析概述静态代码的可信性分析概述 45/45高级软件工程高级软件工程我们还可以类似地求解不等式我们还可以类似地求解不等式: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?45
