1、静态代码分析静态代码分析梁广泰2011-05-25提纲提纲q动机动机q程序静态分析（概念程序静态分析（概念+实例）实例）q程序缺陷分析（科研工作）程序缺陷分析（科研工作）动机动机q云平台特点云平台特点 应用程序直接部署在云端服务器上，存在安全隐患应用程序直接部署在云端服务器上，存在安全隐患 直接操作破坏服务器文件系统直接操作破坏服务器文件系统 存在安全漏洞时，可提供黑客入口存在安全漏洞时，可提供黑客入口 资源共享，动态分配资源共享，动态分配 单个应用的性能低下，会侵占其他应用的资源单个应用的性能低下，会侵占其他应用的资源q解决方案之一：解决方案之一：在部署应用程序之前，对其进行静态代码分析：在
2、部署应用程序之前，对其进行静态代码分析：是否存在违禁调用？（非法文件访问）是否存在违禁调用？（非法文件访问）是否存在低效代码？（未借助是否存在低效代码？（未借助StringBuilder对对String进行大量进行大量拼接）拼接）是否存在安全漏洞？（是否存在安全漏洞？（SQL注入，跨站攻击，拒绝服务）注入，跨站攻击，拒绝服务）是否存在恶意病毒？是否存在恶意病毒？提纲提纲q动机动机q程序静态分析（概念程序静态分析（概念+实例）实例）q程序缺陷分析（科研工作）程序缺陷分析（科研工作）静态代码分析静态代码分析q定义：定义：程序静态分析是在不执行程序的情况下对其进行分析的技术，简称程序静态分析是在不执
3、行程序的情况下对其进行分析的技术，简称为静态分析。为静态分析。q对比：对比：程序动态分析：需要实际执行程序程序动态分析：需要实际执行程序 程序理解：静态分析这一术语一般用来形容自动化工具的分析，而程序理解：静态分析这一术语一般用来形容自动化工具的分析，而人工分析则往往叫做程序理解人工分析则往往叫做程序理解q用途：用途：程序翻译程序翻译/编译编译（编译器），程序优化重构，软件缺陷检测等（编译器），程序优化重构，软件缺陷检测等 q过程：过程：大多数情况下，静态分析的输入都是源程序代码或者中间码（如大多数情况下，静态分析的输入都是源程序代码或者中间码（如Java bytecode），只有极少数情况会
4、使用目标代码；以特定形式输），只有极少数情况会使用目标代码；以特定形式输出分析结果出分析结果静态代码分析静态代码分析 qBasic BlocksqControl Flow GraphqDataflow Analysis Live Variable Analysis Reaching Definition AnalysisqLattice Theory Basic BlocksqA basic block is a maximal sequence of consecutive three-address instructions with the following properties:Th
5、e flow of control can only enter the basic block thru the 1st instr.Control will leave the block without halting or branching,except possibly at the last instr.qBasic blocks become the nodes of a flow graph,with edges indicating the order.Basic Block ExampleLeaders1.i=12.j=13.t1=10*i4.t2=t1+j5.t3=8*
6、t26.t4=t3-887.at4=0.08.j=j+19.if j=10 goto(3)10.i=i+111.if i=10 goto(2)12.i=113.t5=i-114.t6=88*t515.at6=1.016.i=i+117.if i=10 goto(13)Basic BlocksControl-Flow GraphsqControl-flow graph:Node:an instruction or sequence of instructions(a basic block)Two instructions i,j in same basic blockiff execution
7、 of i guarantees execution of j Directed edge:potential flow of control Distinguished start node Entry&Exit First&last instruction in programControl-Flow EdgesqBasic blocks=nodesqEdges:Add directed edge between B1 and B2 if:Branch from last statement of B1 to first statement of B2(B2 is a leader),or
8、 B2 immediately follows B1 in program order and B1 does not end with unconditional branch(goto)Definition of predecessor and successor B1 is a predecessor of B2 B2 is a successor of B1CFG Example静态代码分析静态代码分析qBasic BlocksqControl Flow GraphqDataflow Analysis Live Variable Analysis Reaching Definition
9、 AnalysisqLattice Theory Dataflow AnalysisqCompile-Time Reasoning About Run-Time Values of Variables or ExpressionsqAt Different Program Points Which assignment statements produced value of variable at this point?Which variables contain values that are no longer used after this program point?What is
10、 the range of possible values of variable at this program point?Program Points One program point before each node One program point after each node Join point point with multiple predecessors Split point point with multiple successorsLive Variable AnalysisqA variable v is live at point p if v is use
11、d along some path starting at p,and no definition of v along the path before the use.qWhen is a variable v dead at point p?No use of v on any path from p to exit node,orIf all paths from p redefine v before using v.What Use is Liveness Information?qRegister allocation.If a variable is dead,can reass
12、ign its registerqDead code elimination.Eliminate assignments to variables not read later.But must not eliminate last assignment to variable(such as instance variable)visible outside CFG.Can eliminate other dead assignments.Handle by making all externally visible variables live on exit from CFGConcep
13、tual Idea of Analysisqstart from exit and go backwards in CFGqCompute liveness information from end to beginning of basic blocksLiveness Example a=x+y;t=a;c=a+x;x=0 b=t+z;c=y+1;11001001110000qAssume a,b,c visible outside methodqSo are live on exitqAssume x,y,z,t not visibleqRepresent Liveness Using
14、Bit Vectorqorder is abcxyzt1100111100011111001000101110a b c x y z ta b c x y z ta b c x y z tFormalizing AnalysisnEach basic block hasnIN-set of variables live at start of blocknOUT-set of variables live at end of blocknUSE-set of variables with upwards exposed uses in block(use prior to definition
15、)nDEF-set of variables defined in block prior to usenUSEx=z;x=x+1;=z (x not in USE)nDEFx=z;x=x+1;y=1;=x,ynCompiler scans each basic block to derive USE and DEF setsAlgorithmfor all nodes n in N-Exit INn=emptyset;OUTExit=emptyset;INExit=useExit;Changed=N-Exit;while(Changed!=emptyset)choose a node n i
16、n Changed;Changed=Changed-n;OUTn=emptyset;for all nodes s in successors(n)OUTn=OUTn U INp;INn=usen U(outn-defn);if(INn changed)for all nodes p in predecessors(n)Changed=Changed U p;静态代码分析静态代码分析 概念概念qBasic BlocksqControl Flow GraphqDataflow Analysis Live Variable Analysis Reaching Definition Analysis
17、qLattice Theory Reaching DefinitionsqConcept of definition and use a=x+y is a definition of a is a use of x and yqA definition reaches a use if value written by definition may be read by useReaching Definitions s=0;a=4;i=0;k=0 b=1;b=2;i ns=s+a*b;i=i+1;return sReaching Definitions and Constant Propag
18、ationqIs a use of a variable a constant?Check all reaching definitions If all assign variable to same constant Then use is in fact a constantqCan replace variable with constant s=0;a=4;i=0;k=0 b=1;b=2;i ns=s+a*b;i=i+1;return sYes!On all reaching definitionsa=4 s=0;a=4;i=0;k=0 b=1;b=2;i ns=s+4*b;i=i+
19、1;return sYes!On all reaching definitionsa=4 Computing Reaching DefinitionsqCompute with sets of definitions represent sets using bit vectors each definition has a position in bit vectorqAt each basic block,compute definitions that reach start of block definitions that reach end of blockqDo computat
20、ion by simulating execution of program until reach fixed point 1:s=0;2:a=4;3:i=0;k=0 4:b=1;5:b=2;0000000111000011100001111100111110011111001111111111111111111111 2 3 4 5 6 71 2 3 4 5 6 71 2 3 4 5 6 71 2 3 4 5 6 71 2 3 4 5 6 71 2 3 4 5 6 71110000111100011101001111100010111111111001111111i n1111111ret
21、urn s6:s=s+a*b;7:i=i+1;Formalizing Reaching DefinitionsqEach basic block hasIN-set of definitions that reach beginning of blockOUT-set of definitions that reach end of blockGEN-set of definitions generated in blockKILL-set of definitions killed in blockqGENs=s+a*b;i=i+1;=0000011qKILLs=s+a*b;i=i+1;=1
22、010000qCompiler scans each basic block to derive GEN and KILL setsExampleForwards vs.backwardsqA forwards analysis is one that for each program point computes information about the past behavior.Examples of this are available expressions and reaching definitions.Calculation:predecessors of CFG nodes
23、.qA backwards analysis is one that for each program point computes information about the future behavior.Examples of this are liveness and very busy expressions.Calculation:successors of CFG nodes.May vs.MustqA may analysis is one that describes information that may possibly be true and,thus,compute
24、s an upper approximation.Examples of this are liveness and reaching definitions.Calculation:union operator.qA must analysis is one that describes information that must definitely be true and,thus,computes a lower approximation.Examples of this are available expressions and very busy expressions.Calc
25、ulation:intersection operator.静态代码分析静态代码分析 概念概念qBasic BlocksqControl Flow GraphqDataflow Analysis Live Variable Analysis Reaching Definition AnalysisqLattice Theory Basic IdeaqInformation about program represented using values from algebraic structure called latticeqAnalysis produces lattice value f
26、or each program pointqTwo flavors of analysis Forward dataflow analysis Backward dataflow analysisPartial OrdersqSet PqPartial order such that x,y,z P x x(reflexive)x y and y x implies x y(asymmetric)x y and y z implies x z(transitive)qCan use partial order to define Upper and lower bounds Least upp
27、er bound Greatest lower boundUpper BoundsqIf S P then x P is an upper bound of S if y S.y x x P is the least upper bound of S if x is an upper bound of S,and x y for all upper bounds y of S -join,least upper bound(lub),supremum,sup S is the least upper bound of S x y is the least upper bound of x,yL
28、ower BoundsqIf S P then x P is a lower bound of S if y S.x y x P is the greatest lower bound of S if x is a lower bound of S,and y x for all lower bounds y of S -meet,greatest lower bound(glb),infimum,inf S is the greatest lower bound of S x y is the greatest lower bound of x,yCoveringqx y if x y an
29、d x y qx is covered by y(y covers x)if x y,and x z y implies x zqConceptually,y covers x if there are no elements between x and yExampleqP=000,001,010,011,100,101,110,111(standard Boolean lattice,also called hypercube)qx y if(x bitwise and y)=x111011101110010001000100Hasse Diagram If y covers x Line
30、 from y to x y above x in diagramLatticesqIf x y and x y exist for all x,y P,then P is a lattice.qIf S and S exist for all S P,then P is a complete lattice.qAll finite lattices are completeLatticesqIf x y and x y exist for all x,y P,then P is a lattice.qIf S and S exist for all S P,then P is a compl
31、ete lattice.qAll finite lattices are completeqExample of a lattice that is not completeIntegers IFor any x,y I,x y=max(x,y),x y=min(x,y)But I and I do not existI ,is a complete latticeLattice ExamplesqLatticesqNon-latticesSemi-LatticeqOnly one of the two binary operations(meet or join)exist Meet-sem
32、ilattice If x y exist for all x,y P Join-semilattice If x y exist for all x,y PMonotonic Function&Fixed pointqLet L be a lattice.A function f:L L is monotonic ifx,y S:x y f(x)f(y)qLet A be a set,f:A A a function,a A.If f(a)=a,then a is called a fixed point of f on AExistence of Fixed Points The heig
33、ht of a lattice is defined to be the length of the longest path from to In a complete lattice L with finite height,every monotonic function f:L L has a unique least fixed-point:0()iifKnaster-Tarski Fixed Point TheoremqSuppose(L,)is a complete lattice,f:LL is a monotonic function.qThen the fixed poin
34、t m of f can be defined asCalculating Fixed PointqThe time complexity of computing a fixed-point depends on three factors:The height of the lattice,since this provides a bound for i;The cost of computing f;The cost of testing equality.qThe computation of a fixed-point can be illustrated as a walk up
35、 the lattice starting at:Application to Dataflow AnalysisqDataflow information will be lattice values Transfer functions operate on lattice values Solution algorithm will generate increasing sequence of values at each program point Ascending chain condition will ensure terminationqWill use to combin
36、e values at control-flow join pointsTransfer FunctionsqTransfer function f:PP for each node in control flow graphqf models effect of the node on the program informationTransfer FunctionsEach dataflow analysis problem has a set F of transfer functions f:PP Identity function i F F must be closed under
37、 composition:f,g F.the function h=x.f(g(x)F Each f F must be monotone:x y implies f(x)f(y)Sometimes all f F are distributive:f(x y)=f(x)f(y)Distributivity implies monotonicity课程考核方式课程考核方式q作业（提交到课程平台作业（提交到课程平台http:/sase.seforge.org/q，并演示），并演示）+课程报告课程报告q作业选题：作业选题：代码注释提取，文档生成代码注释提取，文档生成 代码信息统计：总行数，代码行数，类数量，方法数，方法长度等代码信息统计：总行数，代码行数，类数量，方法数，方法长度等 Latex格式文档自动转成格式文档自动转成PDF 代码在线代码在线diff Executable Jar转换成带有特定转换成带有特定icon的的exe程序程序 代码各类缺陷检测：内存泄漏，空指针异常代码各类缺陷检测：内存泄漏，空指针异常 Test case 自动生成自动生成 脚本缺陷分析：脚本缺陷分析：Javascript，Python，Ruby，PHP C#代码缺陷分析代码缺陷分析 在线压缩，解压缩，加密，解密在线压缩，解压缩，加密，解密 Questions?Thank you!
