静态代码分析PPT课件.ppt

静态代码分析 梁广泰2011 05 25 提纲 动机程序静态分析 概念 实例 程序缺陷分析 科研工作 动机 云平台特点应用程序直接部署在云端服务器上 存在安全隐患直接操作破坏服务器文件系统存在安全漏洞时 可提供黑客入口资源共享 动态分配单个应用的性能低下 会侵占其他应用的资源解决方案之一 在部署应用程序之前 对其进行静态代码分析 是否存在违禁调用 非法文件访问 是否存在低效代码 未借助StringBuilder对String进行大量拼接 是否存在安全漏洞 SQL注入 跨站攻击 拒绝服务 是否存在恶意病毒 提纲 动机程序静态分析 概念 实例 程序缺陷分析 科研工作 静态代码分析 定义 程序静态分析是在不执行程序的情况下对其进行分析的技术 简称为静态分析 对比 程序动态分析 需要实际执行程序程序理解 静态分析这一术语一般用来形容自动化工具的分析 而人工分析则往往叫做程序理解用途 程序翻译 编译 编译器 程序优化重构 软件缺陷检测等过程 大多数情况下 静态分析的输入都是源程序代码或者中间码 如Javabytecode 只有极少数情况会使用目标代码 以特定形式输出分析结果 静态代码分析 BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory BasicBlocks Abasicblockisamaximalsequenceofconsecutivethree addressinstructionswiththefollowingproperties Theflowofcontrolcanonlyenterthebasicblockthruthe1stinstr Controlwillleavetheblockwithouthaltingorbranching exceptpossiblyatthelastinstr Basicblocksbecomethenodesofaflowgraph withedgesindicatingtheorder BasicBlockExample Leaders i 1j 1t1 10 it2 t1 jt3 8 t2t4 t3 88a t4 0 0j j 1ifj 10goto 3 i i 1ifi 10goto 2 i 1t5 i 1t6 88 t5a t6 1 0i i 1ifi 10goto 13 BasicBlocks Control FlowGraphs Control flowgraph Node aninstructionorsequenceofinstructions abasicblock Twoinstructionsi jinsamebasicblockiffexecutionofiguaranteesexecutionofjDirectededge potentialflowofcontrolDistinguishedstartnodeEntry ExitFirst lastinstructioninprogram Control FlowEdges Basicblocks nodesEdges AdddirectededgebetweenB1andB2if BranchfromlaststatementofB1tofirststatementofB2 B2isaleader orB2immediatelyfollowsB1inprogramorderandB1doesnotendwithunconditionalbranch goto DefinitionofpredecessorandsuccessorB1isapredecessorofB2B2isasuccessorofB1 CFGExample 静态代码分析 BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory DataflowAnalysis Compile TimeReasoningAboutRun TimeValuesofVariablesorExpressionsAtDifferentProgramPointsWhichassignmentstatementsproducedvalueofvariableatthispoint Whichvariablescontainvaluesthatarenolongerusedafterthisprogrampoint Whatistherangeofpossiblevaluesofvariableatthisprogrampoint ProgramPoints OneprogrampointbeforeeachnodeOneprogrampointaftereachnodeJoinpoint pointwithmultiplepredecessorsSplitpoint pointwithmultiplesuccessors LiveVariableAnalysis Avariablevisliveatpointpifvisusedalongsomepathstartingatp andnodefinitionofvalongthepathbeforetheuse Whenisavariablevdeadatpointp Nouseofvonanypathfromptoexitnode orIfallpathsfrompredefinevbeforeusingv WhatUseisLivenessInformation Registerallocation Ifavariableisdead canreassignitsregisterDeadcodeelimination Eliminateassignmentstovariablesnotreadlater Butmustnoteliminatelastassignmenttovariable suchasinstancevariable visibleoutsideCFG Caneliminateotherdeadassignments HandlebymakingallexternallyvisiblevariablesliveonexitfromCFG ConceptualIdeaofAnalysis startfromexitandgobackwardsinCFGComputelivenessinformationfromendtobeginningofbasicblocks LivenessExample a x y t a c a x x 0 b t z c y 1 1100100 1110000 Assumea b cvisibleoutsidemethodSoareliveonexitAssumex y z tnotvisibleRepresentLivenessUsingBitVectororderisabcxyzt 1100111 1000111 1100100 0101110 abcxyzt abcxyzt abcxyzt FormalizingAnalysis EachbasicblockhasIN setofvariablesliveatstartofblockOUT setofvariablesliveatendofblockUSE setofvariableswithupwardsexposedusesinblock usepriortodefinition DEF setofvariablesdefinedinblockpriortouseUSE x z x x 1 z xnotinUSE DEF x z x x 1 y 1 x y CompilerscanseachbasicblocktoderiveUSEandDEFsets Algorithm forallnodesninN Exit IN n emptyset OUT Exit emptyset IN Exit use Exit Changed N Exit while Changed emptyset chooseanodeninChanged Changed Changed n OUT n emptyset forallnodessinsuccessors n OUT n OUT n UIN p IN n use n U out n def n if IN n changed forallnodespinpredecessors n Changed ChangedU p 静态代码分析 概念 BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory ReachingDefinitions Conceptofdefinitionandusea x yisadefinitionofaisauseofxandyAdefinitionreachesauseifvaluewrittenbydefinitionmaybereadbyuse ReachingDefinitions ReachingDefinitionsandConstantPropagation Isauseofavariableaconstant CheckallreachingdefinitionsIfallassignvariabletosameconstantThenuseisinfactaconstantCanreplacevariablewithconstant IsaConstantins s a b Yes Onallreachingdefinitionsa 4 ConstantPropagationTransform Yes Onallreachingdefinitionsa 4 2020 3 19 27 ComputingReachingDefinitions ComputewithsetsofdefinitionsrepresentsetsusingbitvectorseachdefinitionhasapositioninbitvectorAteachbasicblock computedefinitionsthatreachstartofblockdefinitionsthatreachendofblockDocomputationbysimulatingexecutionofprogramuntilreachfixedpoint 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 1234567 1234567 1234567 1234567 1234567 1234567 1110000 1111000 1110100 1111100 0101111 1111100 1111111 i n 1111111 returns 6 s s a b 7 i i 1 FormalizingReachingDefinitions EachbasicblockhasIN setofdefinitionsthatreachbeginningofblockOUT setofdefinitionsthatreachendofblockGEN setofdefinitionsgeneratedinblockKILL setofdefinitionskilledinblockGEN s s a b i i 1 0000011KILL s s a b i i 1 1010000CompilerscanseachbasicblocktoderiveGENandKILLsets Example Forwardsvs backwards Aforwardsanalysisisonethatforeachprogrampointcomputesinformationaboutthepastbehavior Examplesofthisareavailableexpressionsandreachingdefinitions Calculation predecessorsofCFGnodes Abackwardsanalysisisonethatforeachprogrampointcomputesinformationaboutthefuturebehavior Examplesofthisarelivenessandverybusyexpressions Calculation successorsofCFGnodes Mayvs Must Amayanalysisisonethatdescribesinformationthatmaypossiblybetrueand thus computesanupperapproximation Examplesofthisarelivenessandreachingdefinitions Calculation unionoperator Amustanalysisisonethatdescribesinformationthatmustdefinitelybetrueand thus computesalowerapproximation Examplesofthisareavailableexpressionsandverybusyexpressions Calculation intersectionoperator 静态代码分析 概念 BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory BasicIdea InformationaboutprogramrepresentedusingvaluesfromalgebraicstructurecalledlatticeAnalysisproduceslatticevalueforeachprogrampointTwoflavorsofanalysisForwarddataflowanalysisBackwarddataflowanalysis PartialOrders SetPPartialorder suchthat x y z Px x reflexive x yandy ximpliesx y asymmetric x yandy zimpliesx z transitive CanusepartialordertodefineUpperandlowerboundsLeastupperboundGreatestlowerbound UpperBounds IfS Pthenx PisanupperboundofSif y S y xx PistheleastupperboundofSifxisanupperboundofS andx yforallupperboundsyofS join leastupperbound lub supremum sup SistheleastupperboundofSx yistheleastupperboundof x y LowerBounds IfS Pthenx PisalowerboundofSif y S x yx PisthegreatestlowerboundofSifxisalowerboundofS andy xforalllowerboundsyofS meet greatestlowerbound glb infimum inf SisthegreatestlowerboundofSx yisthegreatestlowerboundof x y Covering x yifx yandx yxiscoveredbyy ycoversx ifx y andx z yimpliesx zConceptually ycoversxiftherearenoelementsbetweenxandy Example P 000 001 010 011 100 101 110 111 standardBooleanlattice alsocalledhypercube x yif xbitwiseandy x 111 011 101 110 010 001 000 100 HasseDiagramIfycoversxLinefromytoxyabovexindiagram Lattices Ifx yandx yexistforallx y P thenPisalattice If Sand SexistforallS P thenPisacompletelattice Allfinitelatticesarecomplete Lattices Ifx yandx yexistforallx y P thenPisalattice If Sand SexistforallS P thenPisacompletelattice AllfinitelatticesarecompleteExampleofalatticethatisnotcompleteIntegersIForanyx y I x y max x y x y min x y But Iand IdonotexistI isacompletelattice LatticeExamples LatticesNon lattices Semi Lattice Onlyoneofthetwobinaryoperations meetorjoin existMeet semilatticeIfx yexistforallx y PJoin semilatticeIfx yexistforallx y P MonotonicFunction Fixedpoint LetLbealattice Afunctionf L Lismonotonicif x y S x y f x f y LetAbeaset f A Aafunction a A Iff a a thenaiscalledafixedpointoffonA ExistenceofFixedPoints Theheightofalatticeisdefinedtobethelengthofthelongestpathfrom to InacompletelatticeLwithfiniteheight everymonotonicfunctionf L Lhasauniqueleastfixed point Knaster TarskiFixedPointTheorem Suppose L isacompletelattice f L Lisamonotonicfunction Thenthefixedpointmoffcanbedefinedas CalculatingFixedPoint Thetimecomplexityofcomputingafixed pointdependsonthreefactors Theheightofthelattice sincethisprovidesaboundfori Thecostofcomputingf Thecostoftestingequality Thecomputationofafixed pointcanbeillustratedasawalkupthelattices