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

第九讲静态代码的可信性分析概述,机能完整?易生何病?什么性格?道德水准?,从静态代码分析动态特性：,主要考虑如何发现代码缺陷！需要首先知道：可能存在什么样的代码缺陷！缺陷与约束:什么是对的（约束：Constraint）什么是不对的（缺陷：Defect）,关于代码你有什么样的先验知识？如何形式化描述这些知识？如何使用这些知识查找缺陷？,不论是人工还是自动都需要：利用已有的缺陷知识查找某个特定程序,内容,一、静态代码缺陷查找的角色二、静态代码缺陷基本类别三、静态代码缺陷查找的主要方法四、静态代码缺陷查找的常见工具五、理论基础：不动点,Analyzing,Designing,Coding,Compiling,Deploying,DevelopingProcess,Maintaining,静态分析,动态测试,模型检测,在线监测,Vif(TM(j)x=18;第j个图灵机的停机问题是不可判定的x的值也就不能判定,在完备、准确解难以求得的情况下只能追求部分、近似解这是现实的道路也是十分有用的道路主要途径包括：类型检验形式化方法缺陷模式匹配,2、编译过程中的代码缺陷查找,最基本的代码分析词法分析语法分析抽象语法树（AST）类型检验语义分析？变量赋值、调用操作、类型变换等,程序设计语言中的类型,某些具有相同/相似特性实例的集合值的集合？操作的集合？基本类型整数、实数、枚举、字符、布尔自定义结构、抽象数据、面向对象为什么要引入？便于理解？帮助人们发现错误！静态类型化语言每个表达式在静态程序分析时都是确定的强类型化语言所有表达式的类型是一致的（可以在运行时检验）,实际编写代码时，这是被编译器检查出来的一类常见错误！,3、形式化的软件分析方法,形式化软件分析是一种基于数学的“自动化”技术：给出一个特定行为的精确描述，该技术可以“准确地”对软件的语义进行推理,主要的形式化方法包括：模型检测(ModelChecking)抽象解释(AbstractInterpretation)定理证明(TheoremProving)符号执行(SymbolicExecution),基于“有限状态自动机”理论从代码中抽取有限状态转换系统模型，用来表示目标系统的行为适合检验“并发”等时序方面的特性对于值域等类型的分析比较困难状态爆炸,模型检测,抽象解释,一种基于“格”理论的框架许多形式化分析方法都可以被涵盖其中主要适合数据流分析（DataFlowAnalysis）尤其是对循环、递归等主要思想是对代码进行“近似”，将不可判定问题进行模拟,定理证明(TheoremProving),演绎方法（DeductiveMethods）基于Floyd/Hoare逻辑用如下形式表示程序的状态PCQC:可执行代码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):xS:xx传递(Transitivity):x,y,zS:xyyzxz反对称(Anti-symmetry):x,yS:xyyxx=y,1、偏序(partialorder),假设XS.yS是X的上界(upperbound),记作Xy,如果：xX:xy类似地：yS是X的下界(lowerbound),记作yX,如果：xX:yx定义最小上界（leastupperbound）X:XX(yS:XyXy)定义最大下界（greatestlowerbound）X：XX(yS:yXyX),2、格（Lattice）,一个格是一个偏序集S，且满足：对于所有的子集XS，X与X都存在一个格一定有：唯一的一个最大元素(top)：=S唯一的一个最小元素(bottom)：=S.由于最小上界和最大下界的唯一性，可以将求x和y的最小上界和最大下界定义为x和y的二元运算：最小上界:xy最大下界:xy,为什么？,哪些是格?,对于任何一个有限集合A，可以定义一个格(2A,),其中，=,=A,xy=xy,xy=xy,格的高度是从到的最长路径。例如：上面幂集格的高度是4。一般地：格(2A,)的高度是|A|.,3、不动点（Fixed-Points）,一个函数f:LL是单调的(monotone),当:x,yS:xyf(x)f(y)单调函数不一定是递增的:常量函数也是单调的多个单调函数的复合仍然是单调函数如果将与看作函数,则它们都是单调的,对于一个高度有限的格L每个单调函数f有唯一的一个最小不动点:fix(f)=fi()i0那么: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)为:L1L2.Ln=(x1,x2,.,xn)|xiLi其中是逐点对应的.与可以被逐点计算height(L1.Ln)=height(L1)+.+height(Ln),和操作:L1+L2+.+Ln=(i,xi)|xiLi,(i,x)(j,y)当且仅当:i=j且xy.height(L1+.+Ln)=maxheight(Li).,如果L是一个有限高度的格,那么lift(L)是:,高度：height(lift(L)=height(L)+1.,如果A是一个有限集合，那么flat(A):,是一个高度为2的格,有限高度的映射格（maplattice）定义为:A|L=a1|x1,.,an|xn|xiLheight(A|L)=|A|height(L).,如何利用不动点求解等式系统(systemsofequations)?假设L是一个高度有限的格,一个等式系统的形式为:x1=F1(x1,.,xn)x2=F2(x1,.,xn).xn=Fn(x1,.,xn)xi是变量Fi:LnL是单调函数集合每个这样的系统有一个唯一的最小解,且是函数F的最小不动点.F:LnLndefinedby:F(x1,.,xn)=(F1(x1,.,x