




已阅读5页,还剩47页未读, 继续免费阅读
版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
静态代码分析,梁广泰2011-05-25,提纲,动机程序静态分析(概念+实例)程序缺陷分析(科研工作),动机,云平台特点应用程序直接部署在云端服务器上,存在安全隐患直接操作破坏服务器文件系统 存在安全漏洞时,可提供黑客入口资源共享,动态分配单个应用的性能低下,会侵占其他应用的资源解决方案之一:在部署应用程序之前,对其进行静态代码分析:是否存在违禁调用?(非法文件访问)是否存在低效代码?(未借助StringBuilder对String进行大量拼接)是否存在安全漏洞?(SQL注入,跨站攻击,拒绝服务)是否存在恶意病毒?,提纲,动机程序静态分析(概念+实例)程序缺陷分析(科研工作),静态代码分析,定义:程序静态分析是在不执行程序的情况下对其进行分析的技术,简称为静态分析。对比:程序动态分析:需要实际执行程序 程序理解:静态分析这一术语一般用来形容自动化工具的分析,而人工分析则往往叫做程序理解用途:程序翻译/编译 (编译器),程序优化重构,软件缺陷检测等 过程:大多数情况下,静态分析的输入都是源程序代码或者中间码(如Java bytecode),只有极少数情况会使用目标代码;以特定形式输出分析结果,静态代码分析,Basic BlocksControl Flow GraphDataflow AnalysisLive Variable AnalysisReaching Definition AnalysisLattice Theory,Basic Blocks,A basic block is a maximal sequence of consecutive three-address instructions with the following properties:The 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.Basic blocks become the nodes of a flow graph, with edges indicating the order.,Basic Block Example,Leaders,i = 1j = 1t1 = 10 * it2 = t1 + jt3 = 8 * t2t4 = t3 - 88at4 = 0.0j = j + 1if j = 10 goto (3)i = i + 1if i = 10 goto (2)i = 1t5 = i - 1t6 = 88 * t5at6 = 1.0i = i + 1if i = 10 goto (13),Basic Blocks,Control-Flow Graphs,Control-flow graph:Node: an instruction or sequence of instructions (a basic block)Two instructions i, j in same basic blockiff execution of i guarantees execution of jDirected edge: potential flow of controlDistinguished start node Entry & ExitFirst & last instruction in program,Control-Flow Edges,Basic blocks = nodesEdges:Add directed edge between B1 and B2 if:Branch from last statement of B1 to first statement of B2 (B2 is a leader), orB2 immediately follows B1 in program order and B1 does not end with unconditional branch (goto)Definition of predecessor and successorB1 is a predecessor of B2B2 is a successor of B1,CFG Example,静态代码分析,Basic BlocksControl Flow GraphDataflow AnalysisLive Variable AnalysisReaching Definition AnalysisLattice Theory,Dataflow Analysis,Compile-Time Reasoning AboutRun-Time Values of Variables or ExpressionsAt Different Program PointsWhich assignment statements produced value of variable at this point?Which variables contain values that are no longer used after this program point?What is the range of possible values of variable at this program point? ,Program Points,One program point before each nodeOne program point after each nodeJoin point point with multiple predecessorsSplit point point with multiple successors,Live Variable Analysis,A variable v is live at point p if v is used along some path starting at p, and no definition of v along the path before the use.When 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?,Register allocation.If a variable is dead, can reassign its registerDead 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 CFG,Conceptual Idea of Analysis,start from exit and go backwards in CFGCompute liveness information from end to beginning of basic blocks,Liveness Example,a = x+y;t = a;c = a+x;x = 0,b = t+z;,c = y+1;,1100100,1110000,Assume a,b,c visible outside methodSo are live on exitAssume x,y,z,t not visibleRepresent Liveness Using Bit Vectororder is abcxyzt,1100111,1000111,1100100,0101110,a b c x y z t,a b c x y z t,a b c x y z t,Formalizing Analysis,Each basic block hasIN - set of variables live at start of blockOUT - set of variables live at end of blockUSE - set of variables with upwards exposed uses in block (use prior to definition)DEF - set of variables defined in block prior to useUSEx = z; x = x+1; = z (x not in USE)DEFx = z; x = x+1; y = 1; = x, yCompiler scans each basic block to derive USE and DEF sets,Algorithm,for all nodes n in N - Exit INn = emptyset;OUTExit = emptyset; INExit = useExit;Changed = N - Exit ;while (Changed != emptyset) choose a node n in 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 ;,静态代码分析 概念,Basic BlocksControl Flow GraphDataflow AnalysisLive Variable AnalysisReaching Definition AnalysisLattice Theory,Reaching Definitions,Concept of definition and usea = x+y is a definition of a is a use of x and yA definition reaches a use if value written by definition may be read by use,Reaching Definitions,Reaching Definitions and Constant Propagation,Is a use of a variable a constant?Check all reaching definitionsIf all assign variable to same constantThen use is in fact a constantCan replace variable with constant,Is a Constant in s = s+a*b?,Yes!On all reaching definitionsa = 4,Constant Propagation Transform,Yes!On all reaching definitionsa = 4,Computing Reaching Definitions,Compute with sets of definitionsrepresent sets using bit vectorseach definition has a position in bit vectorAt each basic block, computedefinitions that reach start of blockdefinitions that reach end of blockDo computation 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;,0000000,1110000,1110000,1111100,1111100,1111100,1111111,1111111,1111111,1 2 3 4 5 6 7,1 2 3 4 5 6 7,1 2 3 4 5 6 7,1 2 3 4 5 6 7,1 2 3 4 5 6 7,1 2 3 4 5 6 7,1110000,1111000,1110100,1111100,0101111,1111100,1111111,i n,1111111,return s,6: s = s + a*b;7: i = i + 1;,Formalizing Reaching Definitions,Each 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 blockGENs = s + a*b; i = i + 1; = 0000011KILLs = s + a*b; i = i + 1; = 1010000Compiler scans each basic block to derive GEN and KILL sets,Example,Forwards vs. backwards,A 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.A 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. Must,A may analysis is one that describes information that may possibly be true and, thus, computes an upper approximation.Examples of this are liveness and reaching definitions.Calculation: union operator.A 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.Calculation: intersection operator.,静态代码分析 概念,Basic BlocksControl Flow GraphDataflow AnalysisLive Variable AnalysisReaching Definition AnalysisLattice Theory,Basic Idea,Information about program represented using values from algebraic structure called latticeAnalysis produces lattice value for each program pointTwo flavors of analysisForward dataflow analysisBackward dataflow analysis,Partial Orders,Set PPartial order such that x,y,zPx x (reflexive)x y and y x implies x y (asymmetric)x y and y z implies x z(transitive)Can use partial order to defineUpper and lower boundsLeast upper boundGreatest lower bound,Upper Bounds,If S P thenxP is an upper bound of S if yS. y xxP is the least upper bound of S ifx 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 Sx y is the least upper bound of x,y,Lower Bounds,If S P thenxP is a lower bound of S if yS. x yxP is the greatest lower bound of S ifx 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 Sx y is the greatest lower bound of x,y,Covering,x y if x y and xy x is covered by y (y covers x) ifx y, andx z y implies x zConceptually, y covers x if there are no elements between x and y,Example,P = 000, 001, 010, 011, 100, 101, 110, 111(standard Boolean lattice, also called hypercube)x y if (x bitwise and y) = x,111,011,101,110,010,001,000,100,Hasse DiagramIf y covers xLine from y to xy above x in diagram,Lattices,If x y and x y exist for all x,yP, then P is a lattice.If S and S exist for all S P, then P is a complete lattice.All finite lattices are complete,Lattices,If x y and x y exist for all x,yP, then P is a lattice.If S and S exist for all S P, then P is a complete lattice.All finite lattices are completeExample of a lattice that is not completeIntegers IFor any x, yI, x y = max(x,y), x y = min(x,y)But I and I do not existI , is a complete lattice,Lattice Examples,LatticesNon-lattices,Semi-Lattice,Only one of the two binary operations (meet or join) existMeet-semilattice If x y exist for all x,yPJoin-semilattice If x y exist for all x,yP,Monotonic Function & Fixed point,Let L be a lattice. A function f : L L is monotonic ifx, y S : x y f (x) f (y)Let 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 A,Existence of Fixed Points,The height 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 :,Knaster-Tarski Fixed Point Theorem,Suppose (L, ) is a complete lattice, f: LL is a monotonic function.Then the fixed point m of f can be defined as,Calculating Fixed Point,The 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.The computation of a
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 2025安徽宣城市中心医院第一批次招聘22人模拟试卷附答案详解(模拟题)
- 2025福建省福州第十八中学招聘工作人员1人考前自测高频考点模拟试题及答案详解1套
- 2025江苏张家港市万通建设工程有限公司招聘2人考前自测高频考点模拟试题有完整答案详解
- 2025年甘肃省陇南事业单位招聘在哪查看考前自测高频考点模拟试题有答案详解
- 2025广东汕头市中心医院招聘编外人员57人考前自测高频考点模拟试题附答案详解(考试直接用)
- 2025年榆林华源电力有限责任公司招聘(5人)考前自测高频考点模拟试题及一套答案详解
- 2025年中国机械工业集团有限公司春季校园招聘笔试题库历年考点版附带答案详解
- 2025包头市白云鄂博矿区招聘区属国有企业工作人员模拟试卷及答案详解参考
- 2025年三明市供电服务有限公司招聘61人考前自测高频考点模拟试题及答案详解(夺冠)
- 2025年湖南衡阳市公安局警务辅助人员招聘120人模拟试卷及答案详解一套
- 烘焙与甜点制作
- T-CRHA 028-2023 成人住院患者静脉血栓栓塞症风险评估技术
- 地基事故案例分析
- 国家开放大学《财政与金融(农)》形考任务1-4参考答案
- 英语考级-a级词汇完整版
- 隧道钻爆法掘进施工安全操作规程
- 计算机网络技术专业介绍解析
- 圆锥式破碎机说明书样本
- 九年级英语 第二单元 教案 ·(全)·
- GB/T 37864-2019生物样本库质量和能力通用要求
- GA/T 952-2011法庭科学机动车发动机号码和车架号码检验规程
评论
0/150
提交评论