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

机能完整易生何病什么性格道德水准从静态代码分析动态特性:主要考虑如何发现代码缺陷!
需要首先知道:可能存在什么样的代码缺陷!
缺陷与约束:什么是对的(约束:Constraint)什么是不对的(缺陷:Defect)关于代码你有什么样的先验知识如何形式化描述这些知识如何使用这些知识查找缺陷不论是人工还是自动都需要:利用已有的缺陷知识查找某个特定程序内容一、静态代码缺陷查找的角色二、静态代码缺陷基本类别三、静态代码缺陷查找的主要方法四、静态代码缺陷查找的常见工具五、理论基础:不动点Product(Artifact)AnalyzingDesigningCodingCompilingDeployingDevelopingProcessMaintaining静态分析动态测试模型检测在线监测V&V一、静态代码缺陷查找的角色Review!
动态测试离线运行程序应用最广泛的缺陷查找技术对功能性最有效工作量大:微软(半数的测试人员)自动程度难以提高基本分类黑盒白盒许多缺陷靠运行很难暴露:死琐等静态缺陷查找不运行程序(广义测试包含这类活动)静态分析可以涉及更多的路径组合测试一次只能有一个执行轨迹可以分析多种属性死琐安全漏洞性能属性源码目标码在线检测当系统正在为用户提供服务时,一般不能进行测试:输入受限但可以进行检测,获取各种状态、事件进行分析,并可能据此调整目标系统尽量减少对系统的应用与静态分析结合二、静态代码缺陷类别与具体应用"无关"词法或者语法共性特性(死锁、空指针、内存泄露、数组越界)公共库用法(顺序、参数、接口实现,容错,安全)与具体应用"相关"类型定义(操作格式,不含其它信息(信息隐藏))类型约束(调用的顺序、参数值,接口实现)需求相关(正确)与具体应用无关词法或者语法:语言设计人员共性特性:基础知识公共库用法:库开发人员(形成文挡)用户整理(分析实现代码、分析使用代码)与具体应用相关类型定义:应用设计人员类型约束:应用设计人员、编程人员需求相关:用户如何得到这些知识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、形式化的软件分析方法形式化软件分析是一种基于数学的"自动化"技术:给出一个特定行为的精确描述,该技术可以"准确地"对软件的语义进行推理主要的形式化方法包括:模型检测(ModelChecking)抽象解释(AbstractInterpretation)定理证明(TheoremProving)符号执行(SymbolicExecution)基于"有限状态自动机"理论从代码中抽取有限状态转换系统模型,用来表示目标系统的行为适合检验"并发"等时序方面的特性对于值域等类型的分析比较困难状态爆炸模型检测抽象解释一种基于"格"理论的框架许多形式化分析方法都可以被涵盖其中主要适合数据流分析(DataFlowAnalysis)尤其是对循环、递归等主要思想是对代码进行"近似",将不可判定问题进行模拟定理证明(TheoremProving)演绎方法(DeductiveMethods)基于Floyd/Hoare逻辑用如下形式表示程序的状态{P}C{Q}C:可执行代码P:Pre-condition,执行前的状态属性Q:Post-condition,执行后的状态属性利用推理/证明机制解决语句复合问题符号执行通过使用抽象的符号表示程序中变量的值来模拟程序的执行,克服了变量的值难以确定的问题跟踪各路径上变量的可能取值,有可能发现细微的逻辑错误程序较大时,可能的路径数目增长会很快.
可以选取重要的路径进行分析4、缺陷模式匹配事先收集足够多的共性缺陷模式用户仅输入待检测代码就可以与"类型化"方法关系密切比较实用容易产生"误报"四、缺陷查找工具准确漏报(FalseNegative,notComplete)误报(FalsePositive,notSound)缺陷知识哪里来程序自带工具提供基本方法基于形式化基于缺陷模式基于形式化方法的主要工具JPF模型检测BanderaSlam,BLAST,CMCESC/JavaASTREEPREfix定理证明(TheoremProving)模型检测(ModelChecking)抽象解释(AbstractInterpretation)符号执行(SymbolicExecution)基于缺陷模式的主要工具Jlint主要采用数据流分析技术,速度快没有误报FindBugs内置较多的缺陷模式有较好的应用(google)PMD格式为主,可以灵活增加新缺陷模式以抽象语法树为基础建立Coverify主要针对操作系统……CODA正在开发中……工具发展的特点各自优势不同综合使用多种分析方法在准确度与时间开销上进行折中集成新的编程范型扩展类型思路携带检验信息(头文件与配置文件)JavaAnnotation五、理论基础:不动点1、偏序2、格3、不动点一个偏序是一个数学结构:L=(S,)其中,S是一个集合,(小于等于)是S上的一个二元关系,且满足如下条件:自反(Reflexivity)x∈S:xx传递(Transitivity):x,y,z∈S:xy∧yzxz反对称(Anti-symmetry):x,y∈S:xy∧yxx=y1、偏序(partialorder)假设XS.
y∈S是X的上界(upperbound),记作Xy,如果:x∈X:xy类似地:y∈S是X的下界(lowerbound),记作yX,如果:x∈X:yx定义最小上界(leastupperbound)X:XX∧(y∈S:XyXy)定义最大下界(greatestlowerbound)X:XX∧(y∈S:yXyX)2、格(Lattice)一个格是一个偏序集S,且满足:对于所有的子集XS,X与X都存在一个格一定有:唯一的一个最大元素(top):=S唯一的一个最小元素⊥(bottom):⊥=S.
由于最小上界和最大下界的唯一性,可以将求x和y的最小上界和最大下界定义为x和y的二元运算:最小上界:xy最大下界:xy为什么哪些是格对于任何一个有限集合A,可以定义一个格(2A,),其中,A,xy=x∪y,xy=x∩y格的高度是从⊥到的最长路径.
例如:上面幂集格的高度是4.
一般地:格(2A,)的高度是|A|.
3、不动点(Fixed-Points)一个函数f:L→L是单调的(monotone),当:x,y∈S:xyf(x)f(y)单调函数不一定是递增的:常量函数也是单调的多个单调函数的复合仍然是单调函数如果将与看作函数,则它们都是单调的对于一个高度有限的格L每个单调函数f有唯一的一个最小不动点:fix(f)=fii0那么:f(fix(f))=fix(f)证明:1)⊥f(⊥)2)f(⊥)f2(⊥)3)⊥f(⊥)f2(⊥)……4)L高度有限,因此对于某个k:fk(⊥)=fk+1(⊥)5)……计算一个不动点的时间复杂度依赖于3个因素:格的高度计算f的代价;测试等价的代价.
一个不动点的计算可以表示为格中,从⊥开始向上搜索的过程闭包性质(ClosureProperties)如果L1,L2,Ln是有限高度的格,那么乘积(product)为:L1*L2Ln={(x1,x2,xn)|xi∈Li}其中是逐点对应的.
与可以被逐点计算height(L1Ln)=height(L1)height(Ln)和操作:L1+L2Ln={(i,xi)|xi∈Li\i,x)(j,y)当且仅当:i=j且xy.
height(L1Ln)=max{height(Li)}.
如果L是一个有限高度的格,那么lift(L)是:高度:height(lift(L))=height(L)+1.
如果A是一个有限集合,那么flat(A):a1a2…an⊥是一个高度为2的格有限高度的映射格(maplattice)定义为:A|→L={[a1|→x1,an|→xn]|xi∈L}height(A|→L)=|A|·height(L).
如何利用不动点求解等式系统(systemsofequations)假设L是一个高度有限的格,一个等式系统的形式为:x1=F1(x1,xn)x2=F2(x1,xn).
.
.
xn=Fn(x1,xn)xi是变量Fi:Ln→L是单调函数集合每个这样的系统有一个唯一的最小解,且是函数F的最小不动点.
F:Ln→Lndefinedby:F(x1,xn)=(F1(x1,xn)Fn(x1,xn))我们还可以类似地求解不等式:x1F1(x1,xn)x2F2(x1,xn).
.
.
xnFn(x1,xn)通过观察:xy等价于x=xy这样,上述不等式可以转换为:x1=x1F1(x1,xn)x2=x2F2(x1,xn).
.
.
xn=xnFn(x1,xn)这是一个与前面类似的单调函数等式系统