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

静态代码的可信性分析概述1/45高级软件工程第九讲静态代码的可信性分析概述静态代码的可信性分析概述2/45高级软件工程机能完整?易生何病?什么性格?道德水准?从静态代码分析动态特性：静态代码的可信性分析概述3/45高级软件工程主要考虑如何发现代码缺陷！需要首先知道：可能存在什么样的代码缺陷！缺陷与约束:什么是对的（约束：Constraint）什么是不对的（缺陷：Defect）静态代码的可信性分析概述4/45高级软件工程关于代码你有什么样的先验知识？如何形式化描述这些知识？如何使用这些知识查找缺陷？不论是人工还是自动都需要：利用已有的缺陷知识查找某个特定程序静态代码的可信性分析概述5/45高级软件工程内容一、静态代码缺陷查找的角色二、静态代码缺陷基本类别三、静态代码缺陷查找的主要方法四、静态代码缺陷查找的常见工具五、理论基础：不动点静态代码的可信性分析概述6/45高级软件工程Product(Artifact)AnalyzingDesigningCodingCompilingDeployingDevelopingProcessMaintaining静态分析动态测试模型检测在线监测V&V一、静态代码缺陷查找的角色Review!静态代码的可信性分析概述7/45高级软件工程动态测试离线运行程序应用最广泛的缺陷查找技术–对功能性最有效–工作量大：微软（半数的测试人员？）–自动程度难以提高基本分类–黑盒–白盒许多缺陷靠运行很难暴露：死琐等静态代码的可信性分析概述8/45高级软件工程静态缺陷查找不运行程序(广义测试包含这类活动)静态分析可以涉及更多的路径组合–测试一次只能有一个执行轨迹可以分析多种属性–死琐？安全漏洞?性能属性?源码？目标码？静态代码的可信性分析概述9/45高级软件工程在线检测当系统正在为用户提供服务时，一般不能进行测试：输入受限但可以进行检测，获取各种状态、事件进行分析，并可能据此调整目标系统尽量减少对系统的应用与静态分析结合？静态代码的可信性分析概述10/45高级软件工程二、静态代码缺陷类别与具体应用“无关”–词法或者语法–共性特性（死锁、空指针、内存泄露、数组越界）–公共库用法（顺序、参数、接口实现，容错，安全）与具体应用“相关”–类型定义（操作格式，不含其它信息（信息隐藏））–类型约束（调用的顺序、参数值，接口实现）–需求相关（正确）静态代码的可信性分析概述11/45高级软件工程与具体应用无关–词法或者语法：语言设计人员–共性特性：基础知识–公共库用法：库开发人员（形成文挡）用户整理(分析实现代码、分析使用代码)与具体应用相关–类型定义：应用设计人员–类型约束：应用设计人员、编程人员–需求相关：用户如何得到这些知识？静态代码的可信性分析概述12/45高级软件工程1、静态代码分析2、编译过程中的代码缺陷查找3、形式化分析方法4、缺陷模式匹配三、静态代码缺陷查找的主要方法静态代码的可信性分析概述13/45高级软件工程静态代码缺陷查找属于静态代码分析的范畴静态代码分析是在不运行代码的前提下，获取关于程序信息的过程静态代码分析还可以用于–获取设计结构–理解代码功能–演化代码–……1、静态代码分析静态代码的可信性分析概述14/45高级软件工程给定一个程序，可以问许多问题：•对于某个输入，停机吗?•执行过程需要多少内存?•对于某个输入的输出是什么?•变量x被使用前是否已经初始化过了•变量x的值将来被读取吗?•变量x的值是否一直大于0？•变量x的值取值范围是多少？•变量x的当前值是什么时候赋予的?•指针p会是空吗?静态代码的可信性分析概述15/45高级软件工程Rice定理Rice’s定理(1953)非正式地指出：所有关于程序“行为”的问题是不可判定的(undecidable)例如：能否判定如下变量x的值?x=17;if(TM(j))x=18;第j个图灵机的停机问题是不可判定的x的值也就不能判定静态代码的可信性分析概述16/45高级软件工程在完备、准确解难以求得的情况下只能追求部分、近似解这是现实的道路也是十分有用的道路主要途径包括：•类型检验•形式化方法•缺陷模式匹配静态代码的可信性分析概述17/45高级软件工程2、编译过程中的代码缺陷查找最基本的代码分析词法分析语法分析–抽象语法树（AST）类型检验–语义分析？–变量赋值、调用操作、类型变换等静态代码的可信性分析概述18/45高级软件工程程序设计语言中的类型某些具有相同/相似特性实例的集合–值的集合？操作的集合？基本类型–整数、实数、枚举、字符、布尔自定义–结构、抽象数据、面向对象–为什么要引入？便于理解？帮助人们发现错误！静态类型化语言–每个表达式在静态程序分析时都是确定的强类型化语言–所有表达式的类型是一致的（可以在运行时检验）实际编写代码时，这是被编译器检查出来的一类常见错误！静态代码的可信性分析概述19/45高级软件工程3、形式化的软件分析方法形式化软件分析是一种基于数学的“自动化”技术：给出一个特定行为的精确描述，该技术可以“准确地”对软件的语义进行推理主要的形式化方法包括：模型检测(ModelChecking)抽象解释(AbstractInterpretation)定理证明(TheoremProving)符号执行(SymbolicExecution)静态代码的可信性分析概述20/45高级软件工程基于“有限状态自动机”理论从代码中抽取有限状态转换系统模型，用来表示目标系统的行为适合检验“并发”等时序方面的特性对于值域等类型的分析比较困难–状态爆炸模型检测静态代码的可信性分析概述21/45高级软件工程抽象解释一种基于“格”理论的框架许多形式化分析方法都可以被涵盖其中主要适合数据流分析（DataFlowAnalysis）–尤其是对循环、递归等主要思想是对代码进行“近似”，将不可判定问题进行模拟静态代码的可信性分析概述22/45高级软件工程定理证明(TheoremProving)演绎方法（DeductiveMethods）基于Floyd/Hoare逻辑用如下形式表示程序的状态{P}C{Q}C:可执行代码P:Pre-condition，执行前的状态属性Q:Post-condition，执行后的状态属性利用推理/证明机制解决语句复合问题静态代码的可信性分析概述23/45高级软件工程符号执行通过使用抽象的符号表示程序中变量的值来模拟程序的执行，克服了变量的值难以确定的问题跟踪各路径上变量的可能取值，有可能发现细微的逻辑错误程序较大时，可能的路径数目增长会很快。可以选取重要的路径进行分析静态代码的可信性分析概述24/45高级软件工程4、缺陷模式匹配事先收集足够多的共性缺陷模式用户仅输入待检测代码就可以与”类型化”方法关系密切比较实用容易产生“误报”静态代码的可信性分析概述25/45高级软件工程四、缺陷查找工具准确？–漏报（FalseNegative,notComplete）–误报（FalsePositive,notSound）缺陷知识哪里来–程序自带–工具提供基本方法–基于形式化–基于缺陷模式静态代码的可信性分析概述26/45高级软件工程基于形式化方法的主要工具JPF模型检测BanderaSlam,BLAST,CMCESC/JavaASTREEPREfix定理证明(TheoremProving)模型检测(ModelChecking)抽象解释(AbstractInterpretation)符号执行(SymbolicExecution)静态代码的可信性分析概述27/45高级软件工程基于缺陷模式的主要工具Jlint主要采用数据流分析技术，速度快没有误报FindBugs内置较多的缺陷模式有较好的应用（google）PMD格式为主，可以灵活增加新缺陷模式以抽象语法树为基础建立Coverify主要针对操作系统……CODA正在开发中……静态代码的可信性分析概述28/45高级软件工程工具发展的特点各自优势不同综合使用多种分析方法在准确度与时间开销上进行折中集成？静态代码的可信性分析概述29/45高级软件工程新的编程范型？扩展类型思路携带检验信息（头文件与配置文件）–JavaAnnotation静态代码的可信性分析概述30/45高级软件工程五、理论基础：不动点1、偏序2、格3、不动点静态代码的可信性分析概述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=y1、偏序(partialorder)静态代码的可信性分析概述32/45高级软件工程假设X⊆S.y∈S是X的上界(upperbound),记作X⊑y,如果：∀x∈X:x⊑y类似地：y∈S是X的下界(lowerbound),记作y⊑X,如果：∀x∈X:y⊑x定义最小上界（leastupperbound）⊔X:X⊑⊔X∧(∀y∈S:X⊑y⇒⊔X⊑y)定义最大下界（greatestlowerbound）⊓X：⊓X⊑X∧(∀y∈S:y⊑X⇒y⊑⊓X)静态代码的可信性分析概述33/45高级软件工程2、格（Lattice）一个格是一个偏序集S，且满足：对于所有的子集X⊆S，⊔X与⊓X都存在一个格一定有：唯一的一个最大元素⊤(top)：⊤=⊔S唯一的一个最小元素⊥(bottom)：⊥=⊓S.由于最小上界和最大下界的唯一性，可以将求x和y的最小上界和最大下界定义为x和y的二元运算：最小上界:x⊔y最大下界:x⊓y为什么？静态代码的可信性分析概述34/45高级软件工程哪些是格?静态代码的可信性分析概述35/45高级软件工程对于任何一个有限集合A，可以定义一个格(2A,⊆),其中，⊥=∅,⊤=A,x⊔y=x∪y,x⊓y=x∩y格的高度是从⊥到⊤的最长路径。例如：上面幂集格的高度是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)=⊔fi(⊥)i0那么:f(fix(f))=fix(f)证明:1)⊥⊑f(⊥)2)f(⊥)⊑f2(⊥)3)⊥⊑f(⊥)⊑f2(⊥)⊑……4)L高度有限,因此对于某个k:fk(⊥)=fk+1(⊥)5)……静态代码的可信性分析概述38/45高级软件工程计算一个不动点的时间复杂度依赖于3个因素:•格的高度•计算f的代价;•测试等价的代价.一个不动点的计算可以表示为格中,从⊥开始向上搜索的过程静态代码的可信性分析概述39/45高级软件工程闭包性质(ClosureProperties)如果L1,L2,...,Ln是有限高度的格,那么乘积(product)为:L1×L2×...×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)=max{height(Li)}.静态代码的可信性分析概述41/45高级软件工程如果L是一个有限高度的格,那么lift(L)是:高度：height(lift(L))=height(L