F. Model checking software at compile time

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

Appearsin:Proceedingsofthe1stIEEE&IFIPInternationalSymposiumonTheoreticalAspectsofSoftwareEngineering,

cIEEEJune6–8,2007,Shanghai,China.Copyright

ModelCheckingSoftwareatCompileTime

AnsgarFehnker,RalfHuuck,PatrickJayet,MichelLussenburg,andFelixRauchNationalICTAustraliaLtd.UniversityofNewSouthWales

LockedBag6016,SydneyNSW1466,stname@.au

Abstract

Softwarehasbeenunderscrutinybytheveri cationcommunityfromvariousanglesintherecentpast.Therearetwomajoralgorithmicapproachestoensurethecor-rectnessofandtoeliminatebugsfromsuchsystems:soft-waremodelcheckingandstaticanalysis.Thoseapproachesaretypicallycomplementary.Inthispaperweuseamodelcheckingapproachtosolvestaticanalysisproblems.Thisnotonlyavoidsthescalabilityandabstractionissuestypi-callyassociatedwithmodelchecking,itallowsforspecify-ingnewpropertiesinaconciseandelegantway,scaleswelltolargecodebases,andthebuilt-inoptimizationsofmod-ernmodelcheckersenablescalabilityalsointermsofnum-bersofpropertiestobechecked.Inparticular,wepresentGoanna,the rstC/C++staticsourcecodeanalyzerusingtheoff-the-shelfmodelcheckerNuSMV,andwedemonstrateGoanna’ssuitabilityfordevelopermachinesbyevaluatingitsrun-timeperformance,memoryconsumptionandscala-bilityusingthesourcecodeofOpenSSLasatestbed.

1Introduction

Theapplicationofformalveri cationtechniquestosoft-wareishard.Whilefullfunctionalcorrectnesscanbeshownbyproof-basedmethodssuchasinteractivetheorem-proving,theeffortishigh—i.e.,thereissubstantialexpertmanpowerneededoveranextendedperiodoftime.Thisisnotalwayspractical.Drivers,forinstance,havetypi-callyshortdevelopmenttimesastheyneedtobesuppliedintimewiththehardwarerelease.Also,ongoingcodechangeshavetobetakencareof,creatingthedemandforautomatedanalysistoolsworkingatcompilationtime.

Modelchecking[8,25]andstaticanalysis[21,23]areautomatedtechniquespromisingtoensure(limited)correct-nessorto ndbugsinsoftware.Softwaremodelcheckingtypicallyoperatesonthesemanticlevelofaprogram.Thecommonapproachisto nda nitestateabstractionandto

1

modelcheckthisabstraction.Iftheabstractionistoocoarseitwillbefurtherre ned.Findingtherightlevelofabstrac-tionischallengingandthesubjectofmuchresearch.With-outuserinteraction,softwaremodelcheckingapproachesareoftennotmatureenoughyettocopewithreallifecodeef ciently[26,22].

Staticanalysis,ontheotherhand,worksonthesyntac-ticleveloftheprogram.Assuch,any niteprogramanditscontrol owgraphresultsina nitestatesystemandis,therefore,suitableforalgorithmicanalysis.Whilesta-ticanalysisisknowntoscalewelltolargecodebases,itislimitedbythenumberofpropertiestobecheckedandthede nitionofnewpropertiesisoftencumbersome[13].Incontrast,modelcheckingallowsforaconvenientandoftenconcisespeci cationofprogrampropertiesandoptimiza-tionsinthecheckertechnologymakesitlessaffectedbythenumberofpropertiescheckedwithinthesamemodel.

Inthisworkwepresentanapproachthatcombinesthebestofbothworldsbyusingtheoff-the-shelfmodelcheckerNuSMV[6]anditsspeci cationlanguagetode neandcheckstaticanalysistypepropertiesonlargeC/C++pro-grams.Thisallowsforaconciseand exiblespeci cationofpropertiesandananalysisscalablebothinthesizeofthecodebaseaswellasthenumberofpropertiesanalyzed.Contribution.Wedemonstratethatmodelcheckingisapracticalandscalablesolutiontosolvestaticanalysisproblems.WedemonstratethepracticalitybypresentingamethodofencodingC/C++programanalysisasmodelcheckingproblemsfortheNuSMVmodelchecker.WeimplementtheproposedencodinginourprototypetoolGoannaandpresentitsarchitecture.Moreover,wedemon-stratethatGoannaiscompetitivewithrespecttorun-timeperformance,memoryconsumptionandscalability.

Theabilitytodirectlyusealltheoptimizationsbuiltintomodernmodelcheckers,automaticallyobtainacounterex-ampletraceincaseofapropertyviolation,andaddmoresemantic-basedsoftwaremodelcheckingtechniquesinthe

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

futuremakestheproposedapproachaviablealternativetoexistingtechnology.

Theremainderofthispaperisorganizedasfollows:InSection2wediscussanumberofrelatedapproachesinthisarea.InSection3wegiveapresentationofourapproachandillustratethisbyanextendedexampleinSection4.WegiveadetailedruntimeevaluationofourapproachbycheckingthesourcecodeofOpenSSLandpresentapre-liminaryevaluationonprecisioninSection5.InSection6,wediscusscurrentlimitationsofourtool,ideasforfutureworkandourconclusions.

2RelatedWork

Thebasicideasofsolvingstaticanalysisproblemsbymodelcheckingwere rstdevelopedbySteffenandSchmidt[28,27].Theirmainfocusisondevelopingasafeapproximationoftheprogram’sbehaviourand,there-fore,checkingforasafesubsetofCTL,i.e.,quali edsafetyproperties.ThedrawbacksofthisapproacharethatsafeapproximationsofrealC/C++programsincludingpointerarithmeticareeitherhardtocomputeortoocoarse,leadingtounnecessaryover-approximations.

Wehaveastrongerfocusontheeffectivenessoftheanalysisandabandoninsomecasessoundnessasde nedbySteffen.Thismeans,wetreatprogramspurelyasasetofsyntacticobjectsontheprogram’sCFGandallowtocheckanyCTLpropertyonthatlevel.Whileouranalysisissoundonthissyntacticlevelitisnotnecessarilyasoundabstrac-tionoftheprogram’ssemantics.However,thisapproachhasbeenfollowedbyothers(e.g.,[12,11])andprovestobewell-suitedforcheckingreal-lifesystems.

AsimilarapproachtoourscanbefoundintheUnotool[17]anditslaterdevelopmentintoOrion[11].Theanalysisisalsodonebymodelcheckingonasyntacticlevel.However,theauthorsdonotuseanoff-the-shelfmodelchecker,butimplementmodelcheckingtechniques.Orioniscurrentlymorelimitedtocheckingforthreeproperties:uninitialisedvariables,nil-pointerdereferencesandout-of-boundsarrayindexing.Thetoolcurrentlyhasastrongfo-cusonachievingagoodsignaltonoiseratiobyincorpo-ratingsymbolicsolvertechniques.Goannafocusesonawiderrangeofproperties,withfutureplanstoincludeuser-de nedrulesandembeddedassembly.Itwillbeinterestingtocomparefutureversionsofbothtools.

Relatedtoourphilosophyis,e.g.,theworkinthestaticanalysiscommunitydonebyEngleretal.[12].Theauthorsusemeta-levelcompilation(MC)whichallowssystemim-plementorstobuildtheirownapplication-speci ccompilerextensionsbasedontheMetallanguage.Thoseextensionsareusedasspeci cationsforsearchingtheabstractsyntaxtree,control owanddata owgraph.Theapproachhasbeenfurtherdevelopedintoacommercialproduct[10].

2

Thereareothercommercialstaticanalysistools,e.g.[14,19,15,20]which,however,mostlydonotsupportspeci -cationlanguagessuchasMetalorCTL.Thislimitstheirapplicabilityforsystemdevelopment.

Asemanticmodelcheckingapproachtosoftwarever-i cationisrealisedinSLAM[1]anditssuccessorSDV,atoolusedtoverifydevicedrivers.SLAMisasuiteoftoolsforcounterexample-guidedabstractionre nement.SLAMstartswithacoarseBooleanprogramabstractionthatissubsequentlyre nedgivenpredicatesdiscoveredfromcounterexamplesintheabstraction,untilanabstrac-tionisfoundthatsatis estheproperty.Othertoolsthatim-plementcounterexample-guidedabstractionre nementareBlast[16]andMagic[4].

AtoolforboundedmodelcheckingofANSI-Ccodewaspresentedin[7].Thistool,calledCMBC,canbeusedtoverifysafetyproperties,andalsotoverifyanANSI-Cmodelofacircuitagainstaspeci cationinahardwarede-scriptionlanguagesuchasVerilog.Thetoolunrollsthepro-gramandcheckswithaSAT-solverifthereexistsanerrortraceuptothegivendepth.CMBCisparticularlyusefulfordebuggingsinceitcan ndallerrorsuptoacertaindepthquickly.

TheEauClairetool[5]makesuseofautomatictheoremproving.ItisanextendedstaticcheckerforC,basedontheearlierideasin[18].ThetooltranslatesCcodeintoasetofguardedcommandswhichwillthenbetransformedintoveri cationconditions.Theseveri cationconditionsarecheckedautomaticallybytheSimplifytheoremprover.Basedonabstractinterpretation[9]arethePoly-Space[24]andAstr´ee[3]staticanalyzers.Theyaimatprovingtheabsenceofrun-timeerrorsinprogramswrit-tenintheC/C++programminglanguages.Astr´eeanalyzesstructuredCprograms,withoutdynamicmemoryalloca-tionorrecursion.Abstractinterpretationisparticularlywellsuitedforarrayboundcheckingandalike,asitprovidesasemanticframeworktocapturedomainsandtheoperationsonthem,butsuffersfromhighcomputationalcostsresult-inginmuchlongeranalysistimes.

3SyntacticSoftwareModelChecking

Inthissectionwepresentdetailsofhowtoencodestaticanalysispropertiesbymodelcheckinginapracticalway.ThegoalistodeterminesyntacticpropertiesofC/C++pro-gramsrangingfromuninitializedvariablestonullpointerdereferences.GivenaprogramPandapropertyφthetaskofcheckingwhetherPsatis esφ,i.e.,P|=φ,isreducedtocheckingPs|=φswherePsisa nitesyntacticrepre-sentationofPandφsasyntacticencodingofφ.

Althoughweusemodelcheckingforouranalysis,thetypeofpropertiesweareaddressingaresimilartothoseinstaticanalysis.Forinstance,wecheckwhetheravariablev

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

isinitialized,butnot,e.g.,whethervholdsthecorrectcom-putationresultbytheendoftheprogramexecution.Thelatteroftenrequiresmoreinformationabouttheprogram’ssemantics.

Asmodelcheckingistheanalysisofalabeledgraph(aKripkestructureoveratomicpropositions)withrespecttosomeformula,typicallyintemporallogic,wehavetode-velop:

1.Atemporallogicformulaexpressingthedesiredprop-erty.2.AgraphrepresentingtheC/C++program,labeledwithpropositionsrelevanttoevaluatetheproperty.3.Atranslationtoamodelchecker.

Inthefollowingwedescribeourapproachtoapath-sensitive,intra-proceduralanalysisintheorderofthedif-ferentstepsabove.Throughouttheremainderofthispaperwewilluseabsenceofuninitializedvariablesasanexam-pleproperty,becauseitissimpleincomparisontootherpropertiesthatwecheck,butserveswelltodemonstrateourapproach.

3.2ModelConstruction

Toconstructamodelfromtheprogram,werequireaformalnotionofanabstractsyntaxtree(AST)andalabeledgraph.Wede nealabeledgraph/treeandanattributedtreeasfollows.

De nitionAlabeledgraph(L,E,µL)overthealphabetΣLisa niteanddirectedgraph,whereLisasetofnodes,E L×Lisanedgerelationbetweenthenodes,andµL:L→ΣLisanodelabelingfunction.

AlabeledtreeisalabeledgraphT=(L,E,µL)ifithasasinglerootnoderoot(T)forwhichwehavethefollowing:Foreachnodel∈Lthereexistsexactlyonepathfromtheroottothenode,i.e.exactlyonesequencel0,...,ln,suchthatl0=root(T),ln=l,and(li 1,li)∈E,fori=1,...,n.

Anattributedtree(L,E,µL,µE)overthealphabetsΣLandΣEisalabeledtreewherethereisanadditionallabel-ingfunctionµA:L→ΣA,assigningattributestonodes.Giventwonodesl1andl2ofalabeledtree(L,E,µL),wecalll1theparentofl2andl2thechildif(l1,l2)∈E.Ifthereexistsa(non-empty)pathfroml1tol2,l1iscalledancestorofl2,andl2isadescendantofl1.

AnASTcanbeseenasanattributedtreewherethenodesarelabeledwithprogramstatementsand(sub)expressionswhiletheattributesdescribetheroleofanode’sbranch.E.g.,theconstructinFigure3(a)showspartofanASTforanif-thenbranching.Theattributesdescribewhetherthesubtreeistheif-branch,thecondition,orthenextinstruc-tionofitsparentnode.Thelabelsthendescribethekindofstatementorexpressionoftheconditionorthestatementfollowingtheif-then.

FromtheASTwecanconstructinastraightforwardmannerthecontrol owgraph(CFG).NotethataCFGdoestypicallynotcontainalltheinformationavailableintheAST,onlythecontrolstructuredowntothelevelofstatements,butnotthestructureofexpressions,types,andconstantvalues.

ACFGisagraph,terweaddlabelsmakingitalabeledgraph.WedenotethelabeledCFGofanASTTbyCFGT.Thelabelsrep-resentwhethercertainatomicpropositionsholdinanode.E.g.,ifaparticularvariableisassignedavalue,ifitisusedontheright-handsideofanassignment,orifitisderefer-encedandsoon.

Inourframework,theselabelsareassociatedwithtreepatternsontheAST.Wede nethesyntaxofaquerylan-guagetomatchtreepatternsasfollows:

P::= | |σE|σL|↓|↓ |P/P|P∪P|P[Q]Q::=P|label=σL|attr=σA|Q∧Q|Q∨Q3

3.1

TemporalLogicPropertiesoverPro-grams.

Undertheassumptionthatwecanidentifyatomicpropo-sitionsdeclx,usedxandassignedx,representingprogramlocationswhereavariablexisdeclared,used,orassignedavaluerespectively,wecanspecifythatthisvariableisal-waysinitializedbeforeitisusedasfollowsinCTL:

AGdeclx (A¬usedxWassignedx)

(1)

Thismeanswerequirethatonallprogrampathsifavari-ablexisdeclareditmustnotbeuseduntilithasavalueassignedoritwillnotbeusedatall.Weusetheweakun-tiloperatorWheretoincludethesecondpossibility.Thelattercanalsopointtounusedvariables,whichischeckedseparately.

Inthesamestylewecanexpressotherpropertiesoncor-rectpointerhandling,variableusageormemoryallocationanddeallocation.Moreover,itallowsspecifyingapplicationspeci cpropertiestohandlegeneralprogrammingguide-lines,API-speci crulesorevenhardware/softwareinter-facerulesfordrivers.

Intheremainderofthissectionwedescribehowtomapprogramstotransitionsystemslabeledwithatomicpropo-sitionssuchastheonesaboveandhowtoderivethelabelsthemselvesfromaprogram.

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

whereσL∈ΣLandσA∈ΣA.

Givenan(attributed)treeTandanodel,apatternde- nesasetofnodesinthesubtreerootedinl.Thepattern de nesthenodelitself, theemptyset,andpatternσAandσLchildrenlabeledσAorσLrespectively.Thepatterns↓and↓ standforthechildrenanddescendantsofl,/and∪forconcatenationandunion.Finally,patternP[Q] ltersallnodessatisfyingQ.

Thistreequerylanguageisthedownward,recursivefragmentofthelanguagede nedin[2].Wereferthereadertothispaperforformalsemanticsandadiscussiononex-pressiveness.Theonlydifferenceisthatweallowfortwotypesoflabels,whichhowever,doesnotaddexpressivity.Givenanatomicpropositionp,weassociateatreepat-ternPwithit.WelabeleverynodelthatmatchesP,intheASTTwithrespecttotherootnodeofT,withp.InthecasethatlisnotinCFGT,welabelitsclosestancestorinTwhichisinCFGT.

Example1Takeasanexampleanatomicpropositiondeclx,usedtolabeldeclarationsofvariablex.Thispropo-sitionisassociatedwithpattern↓ Decl[Var:x],i.e.itmatchesallnodes(descendantsoftherootnode)intheASTlabeledDecl,thathaveachildlabeledVar:x.ThosenodeswillthenbelabeledwithdeclxintheCFG.

Figure1.Modelcheckingapproachforstati-callyanalysingC/C++code.

3.3TranslationtoNuSMV

alabelisevaluatedtotrueiffithasbeenalabelintheoriginallabeledCFG.

CTLfisthesetofCTLpropertiesinNuSMVsyntax.InthesubsequentSection4wewillgiveanexampleoftheactualNuSMVcodewhichisasyntacticexpressionoftheabovemodel.

Inordertocheckourgeneratedmodelautomaticallywithrespecttothede nedproperties,wedevelopedatrans-lationtotheNuSMVmodelchecker.InthissectionwesketchhowtotranslatealabeledCFGandaCTLformulaintoasimpleNuSMVmodel.

ForagivenC/C++functionfwetranslatethecorre-spondinglabeledCFG(Lf,Ef,µf)intoasimpleNuSMVmodel,NuSMVf=(varf, f,Deff,CTLf),where varfisoneenumeratedtypevariableinNuSMVoverthesetoftypesl∈Lf.Enumeratedtypevariablesareimplementedef cientlyinNuSMVandguaranteeamuchsmallerstatespacethan,e.g.,usingonebooleanvariableforeachcontrollocation.

f={(l,Succ(l))|l∈Lf,Succ(l)={l‘|(l,l‘)∈Ef}}.Thismeans,theCFGtransitionrelationistrans-latedintoatransitionrelation,wherethetargetforeachtransitionisthesetoflocationswepossiblycanbranchto.ThisisaccordingtoNuSMV’ssyntaxanddoesnotchangetheoriginalCFGtransitionrelation.

Deff={de ne(p)={l|µf(l)=p,l∈Lf}|p∈Σf}.Whereeveryde ne(p)isaDEFINEdeclarationofpinNuSMV.Ade nedeclarationisaspaceef cientwaytodeclare,e.g.,thatapropositionalvariablepholdsexactlyinaparticularsetoflocations.Inourcase,that

4

3.4Architecture

ThearchitectureofourapproachisoutlinedinFigure1.GivenaC/C++program,theonlyinteractionneededfromtheuseristo

1.provideaCTLspeci cation,and

2.de netheatomicpropositionofthespeci cationintermsofqueriesasdescribedinSection3.2.ThetranslationofaprogramintotheCFG,thepat-ternmatching,thesubsequentlabeling,thetranslationtoNuSMV,aswellastheerrorreporting,areallfullyauto-matic.Thisreducestheburdenontheusertoaminimumandforgenericpre-de nedpropertiestozero.

4Example

Thissectionpresentsanexampletoillustratethepro-posedapproachofcombiningsyntacticcheckingwith

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

Figure3.Fragmentsof(a)theattributedabstractsyntaxtree(AST),and(b)theannotatedcontrol owgraph(CFG).

123456789101112

voidf(intx){inta,b;int*p;

p=(int*)

malloc(sizeof(int));*p=42;

if(x==0){free(p);a=*p;}

b=a+*p;}

modelchecking.ConsiderthecontrivedcodefragmentinFigure2,whichisobviously awed.Notonlydoesitcon-tainapotentialaccessofanuninitializedvariable(ainline11),butalsodereferencesapointerthathasalreadybeenfreed(pinline9),andassignsavaluetoavariablethatisneverusedafterwards(binline11).

WewillillustratethelabelingoftheASTandCFG,thegenerationofNuSMVcodethatimplementsthechecksandtheeaseofaddingpropertiestoGoanna.Again,wedemon-strateitinthecontextofuninitializedvariablesforthesakeofsimplicity.

4.1AnnotationofCFG

Figure2.Sourcecodeexample

Theprogramanalysisbuildsonanannotatedcontrol owgraph.Generatingthecontrol owgraph—withoutannotations—forthecodefragmentisstraightforward.AfragmentoftheASTisdepictedinFigure3(a)andthere-sultingCFGinFigure3(b).EachnodeislabeledwithanIDandalabel.TheIDsrefertoidenti ersintheintermedi-ateformatgeneratedbytheparserandareusedfortechnicalreasonsonly.TheattributesofnodesintheASTareusedtolabeltheedgewiththeparentnodeinFigure3(a).OnlynodesoncertainlevelsintheASTwillbeusedtobuildtheCFG,inthisexamplenodes59,63,72and78.5

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

TheatomicpropositionsthatareusedaslabelsontheCFGaregenerated,asmentionedbefore,intwosteps.Inthecaseofuninitializedvariableanalysis,theprocedurein-troducesthreelabelsforeachvariable.E.g.,thedeclarationofvariableainline2ofthecodefragment,forexample,leadstotheintroductionofthelabels:decla,usedaandassigneda.Eachoftheselabelswillbeanatomicproposi-tioninthemodelcheckingframework.

Next,wedescribetheassociatedtreepatternsforeachproposition.Propositiondecla,usedtolabeldeclarationsofvariablea,isassociatedwithpattern↓ Decl[Var:a].Onlynode26intheCFGmatchesthispattern,correspondingtothedeclarationinline2ofthesourcecode,andwillbela-belleddecla.

Propositionusedawilllabelnodesthatusethevari-ablea.Thesearenodeswhichareeither(i)labelledPlus,PostincorPreinc,andhaveachildlabelledVar:a,or(ii)nodeslabeledModifwitharighthand-sidechildVar:a.

Thecorresponding patternis↓(Plus∪Postinc∪Preinc∪...)[Var:a]↓Modif[Var:a[attr=”rhs”]].Node98inFigure3(a)matchesthispattern.However,thisnodeisnotpartoftheCFG.Hence,webacktracktothenearestances-torwhichispartoftheCFG,inthiscasenode72,andlabelituseda.Node72correspondstoline11inthecodefrag-ment.

Finally,forpropositionassignedawelookfornodesthatmodifyavariablewhichhavelabelssuchasModif,PostincorPreincandaleft-hand-sidesuccessorVar:a.Thiscorrespondstothepattern↓ (Modif∪Postinc∪Preinc)[Var:a[attr=”lhs”]].Node86willbelabeledassigneda,becauseitisthenearestancestorofanodethatmatchesthispattern.ThedescribedprocessresultsinthelabelledCFGdepictedinFigure3(b).

MODULEmain

VARlocation:{loc26,loc34,...,loc12}next(location)case

location=location=...

location=...esac

:=

loc26:{loc34};loc34:{loc39};

loc63:{loc78,loc72};

DEFINE

decla:=locationin{loc26};useda:=locationin{loc86};assigna:=locationin{loc72};SPECAGdecla=>(A usedaWassigna)

Figure4.NuSMVcode(fragment)

onwhichaisused,butnotassignedanyvaluebe-forehand.TheprototypetoolGoannawillwarntheuserwith:“Warning:Variable‘a’mightbeuninitialized”andautomaticallyproducesacoun-terexamplewiththesequenceoflinenumbers2,3,5,6,7,11.Notethatthisanalysispointstoapotentialbug.Thereareotherpropertiesthat,ifviolated,pointtode nitebugs.

4.3PropertyImplementationinGoanna

4.2ModelCheckingwithNuSMV

PartsoftheNuSMVcoderesultingfromthetranslationofthelabelledCFGareshowninFigure4.AsdescribedinSection3.3weintroduceoneenumeratedtypevariable,i.e.,location,rangingoverthecontrollocations(i.e.thenodesintheCFG),describethetransitionrelationasasetoftransitionsfromlocationstoasetoflocations,anduseDEFINEdeclarationstoassociatelabelstocertainloca-tions.Notethat,forclarityofpresentation,weusetheweakuntiloperandWintheCTLspeci cation,whichdoesnotex-istinNuSMVsyntax,butcanbeequallyexpressedthroughotherexistingoperators.

UsingNuSMVforcheckingproperty(1)(describedinSection3.1)ontheannotatedCFGnowrevealsaviolationoftheNuSMVspeci cationfromFigure4.GoannaautomaticallyexaminestheviolationreportedbyNuSMVandconcludesthatthereisanincorrectuseofvariablea—infact,thereisapathintheprogram

6

InordertoimplementsuchapropertyinourGoannatool,weonlyneedtoidentifythenodesofinterest(asde-scribedinSection4.1),describetheirrelationshipsinCTLformulasandprinttheseformulasinNuSMVsyntaxtoNuSMV’sinput le(asdescribedinSubsection4.2).AnimplementationofourexamplepropertyisshowninpseudocodeinFigure5.Inthecode,we rst ndthesetofallvariablesthataredeclaredinafunction,becausethesearetheonesthatneedtobecheckedforproperinitialization.Foreachofthesevariables,wethenprinttheCTLspeci -cationstotheNuSMVinput le(thefunctionNuSMV()simplyprintstexttoNuSMV’sinput le).Inthenextstep,foreveryvariableinthesetofdeclaredvariables,wesearchforthesetofnodesintheASTwherethevariableisassignedavalueandwhereitisused,respectively.ForthissearchweusethefunctionFindAST()thatidenti- esnodesintheASTaccordingtospeci cpatterns.Fi-nally,fromthesethreesets,wegetthecorrespondingsetsoflocationsoftherespectivenodesintheCFGbyusingthefunctionCFGlocations().Thatfunctiontranslates

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

#Findallvariablesdeclaredinafunction:

SetvarDecl=FindAST(type=var,label=decl);#Printspeci cationforeachdeclaredvariable:foreach$varinSetvarDecl{

NuSMV("SPECAGdecl_$var->

(A!used$varWassign$var);");

}

NuSMV("DEFINE");

foreach$varinSetvarDecl{

#Identifynodesthatuseorassign$var:

SetvarAssigned=FindAST(var=$var,attr=lhs,

label=Modif|Postinc|Preinc|...);SetvarUsed=FindAST(var=$var,attr=rhs,

label=Modif)

+FindAST(var=$var,label=Postinc|Preinc);#Outputlocationsofpropositions:

NuSMV("decl:=locationin{"

+CFGSetvarDecl)+"};");NuSMV("assigned$var:=locationin{"

+CFGSetvarAssigned)+"};");NuSMV("used:=locationin{"

+CFGSetvarUsed)+"};");}

5Evaluation

5.1

Implementation

OurimplementationiswritteninOCamlandweuseNuSMV2.3.1astheback-endmodelchecker.Thecurrentimplementationisaprototypeworkingonintra-proceduralanalysisandisnotyetoptimizedtowardsperformance.However,itprovidesthereaderwitha rstimpressionwithrespecttospeedandscalability.

Atthecurrentstage,wehave15differentchecksim-plemented.Thesecheckscoverthecorrectusageofmal-loc/freeoperations,useandinitializationofvariables,po-tentialnull-pointerdereferences,memoryleaksanddeadcode.TheCTLpropertyistypicallyonetotwolinesintheprogramandthedescriptionqueryforeachatomicproposi-tionisaround velineswhencoveringalotofexceptions.Thisisstillrathershortcomparedtostandardstaticanalysisframeworksormetacompilation[12].

5.2EvaluationPrinciples

Figure5.PseudocodetocreateaNuSMVcodefragmentforthe“uninitializedvari-ables”property

ASTnodestoCFGnodesand,ifrequired,backtrackstothenearestancestornodethathasacorrespondingnodeintheCFG.ThenweprintthelocationstoNuSMV’sinput le.Notethatthecodedoesnothavetodescribehowthecheckisimplemented.InGoanna,weonlydescribethechecksthatneedtobedone—theimplementationofthechecksislefttoNuSMV.

Thismightseemlikeheavymachinerytocheckforuninitializedvariables.However,duringanalysisthisprop-ertyischeckedforallvariablesatonce.Furthermore,hav-ingthisframeworkinplaceenablesustode neothersyn-tacticpropertieseasily—e.g.,propertiesforinappropriateuseofdereferencedpointers,orunusedvariables.ApplyingGoannatothesourcecodeexampleshowninFigure2willwarnthatthevalueassignedtovariablebinline11isneverused,thatvariablebisneverusedatall(onaright-handside),thatvariableamightbeuseduninitialized,andthatpointerpisdereferencedafterbeingfreed.

7

Weevaluateourapproachregardingrun-timeperfor-mance,memoryusage,andscalability.Therun-timeofthetoolshouldbereasonablylowandintegratewellintothede-velopmentprocess,e.g.itshouldbewithinthesameorderofmagnitudeasthecompiletime.Theruntimeshouldscalewellwithincreasingprogramsizeandnumberofproperties.Also,thememoryusagemustbewithintheresourcelimitsofatypicaldevelopermachineorbuildserver.

ToevaluateGoanna’sspeedandmemoryusage,weap-plyittoalargerreal-worldopen-sourceprojectofrealisticsize:TheOpenSSL1toolkitimplementingtheSecureSock-etsLayer(SSL)andTransportLayerSecurity(TLS)proto-cols(260kLoC).WebuildOpenSSLforaDebianLinux3.1environmentwithgcc3.3.5.OurhardwareplatformfortheexperimentsisaDELLPowerEdgeSC1425server,withanIntelXeonprocessorrunningat3.4GHz,2MiBL2cacheand1.5GiBDDR-2400MHzECCmemory.

5.3

Run-timePerformanceandMemoryUsage

First,welookatsomeoverallperformancenumbers.Wemeasurethewall-clockcompiletimeandcompareitwithGoanna’stotalanalysistime.Furthermore,wemeasurethemaximuminternalmemoryconsumptionofourtoolaswellasNuSMV’smemoryconsumptionduringtheanalysis.Theresultsforonepropertyandforall15propertiesareshowninTable1.Itshowsthattheoverallanalysistimeiswellwithinthesameorderofmagnitudeasthecompile

1/

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

OpenSSL(15properties)[min:sec]

3:07[min:sec]

6:19

[MB]35.4

[min:sec]

5:54

[MB]17.9

[min:sec][MB]

12:1353.3

piletime,run-timeandmaximummemoryusageforGoannaandNuSMVseparately,

andforthewholetoolchainin

total.

807060

807060

Run time [s]

Run time [s]

504030201000

500

1000

1500

2000

2500

3000

Input file size [LoC]

50403020100

500

1000

1500

2000

2500

3000

Input file size [LoC]

Figure6.Run-timesofNuSMVwithrespecttosizeofinputsource les.

Figure7.Run-timesofthewholeGoannatoolchainwithrespecttosizeofinputsource les.

time.Infact,itistwiceaslongasthecompilationforonepropertyandfourtimesaslongfor15properties.

Moreover,fortheanalysiswithall15properties,outof602source les,only3.6%tooklongerthan2secondstoanalyzeand99.2%ofall leswereanalyzedinlessthan5seconds.ThetimespentinNuSMVismostlynegligiblewith98.7%ofall lesbeinganalyzedinlessthen2seconds.Theoveralldistributionoftheruntimewithrespecttothe lesizeisshowninFigure6forNuSMVandinFig-ure7fortheoverallanalysistime.Notethatthecomplexityoftheanalysis—andhenceitsruntime—doesnotperfectlycorrelatewiththe lesize,butthe lesizeiseasilyunder-standableandtypicallyameasureofinteresttothedevel-oper.Infact,thecomplexityofourcurrentimplementationismostlydependentonthenumberofvariablesandthesizeoftheCFG.

Thememoryconsumptionforoneaswellasfor15prop-ertieshasbeenconsiderablylowwith35.3and53.3MB,respectively.This tswellintothestandardmemoryofastate-of-the-artmachine,makingthisapproachwellsuitedtobeintegratedintothestandardbuildprocessonadevel-oper’sdesktop

machine.

8

Discussion.ThereareacoupleofpathologicalcaseswhereNuSMVtakesdisproportionallylongandsomewhereGoanna,i.e.,thetreematching,takesverylong.Therearetwosometimesinterrelatedreasonsforthis:Firstofall,Goanna’streematchingisimpactedbythenumberofvariablesinaprogram.Thecurrentimplementationrunsallmatchingoperationsforallpropertiesandallvariablesinseparateruns,creatingaratherlargeoverhead.Forpro-gramswithfewvariables,theimpactisnotsigni cant,how-ever,whenanalyzinghundredsofvariablesitisconsider-able.AnexampleofthiseffectcanbeseeninFigure7,wheretheoutlinerwith70secondsrun-timeiscausedbyasource lethathasalargenumberofvariables.Conse-quently,wehaveplanstooptimizethetreematchinginthefuture.

Secondly,NuSMVisimpactedbythenumberofvari-ablesandthecomplexityofthecontrolstructure.More-over,theBDDencodingplaysamajorrole.AsistypicalinBDD-basedmodelchecking,run-timesaresometimeshardtopredictand uctuatewildlywhenchangingthevariableorder.Anexplicitstatemodelcheckermightbemoresuit-

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

ablefortheanalysisandwewillexploretheoptioninthefuture.Thisenablestheintegrationofmodelcheckingintothestan-dardbuildprocess,increasingtheoverallsoftwarequality.Currentlimitationsandfuturework.TheGoannatoolisstillataprototypestage.Whileitisalreadyfastenoughforpracticaluse,itisfarfromoptimalandthereisstillmuchroomforsigni cantperformanceimprovements.Oneparticularaspectisourcurrentimplementationofthetreematchingalgorithmwhichtraversesthetreeforeachandeverysubpattern,creatingalargeunnecessaryoverhead.Anotherareathathasn’tbeenaddressedsofarispathpruningtoachieveahigherprecisionforrelaxedproperties.Weareplanningtotakeadvantageofthemodelcheckingapproachbyincludingmoresemantic-basedtechniques—suchaspredicateabstraction—toruleoutinfeasiblepathcombinations.

Finally,whileinprincipleourapproachextendstoclassicinter-proceduralanalysis,westillhavetodevelopheuristicstodealwiththecombinatorialblowupinordertokeeptheanalysistoasimilarspeedasitisforintra-proceduralanalysis.Weareintheprocessofcreatingatwo-passanalysisbymakinguseofsummarieswhichcanbegeneratedfromtheintra-proceduralstage.

AcknowledgementsWethankBernardBlackham,J¨orgBrauer,andSeanSeefriedformanyfruitfuldiscussionsandcomments.

NationalICTAustraliaisfundedbytheAustralianGovernment’sDepartmentofCommunications,Informa-tionTechnologyandtheArtsandtheAustralianResearchCouncilthroughBackingAustralia’sAbilityandtheICTResearchCentreofExcellenceprograms.

5.4ScalabilityandPrecision

Oneoftheencouragingresultsofourcasestudyisthatperformancescalesnicelywhenaddingmoreproperties.Infact,goingfromonepropertyto15propertiesonlydoublestheanalysistime.Withanoptimizedtreematching,weex-pecttofurtherimprovethisratio.

Therearetwomainreasonsforthis:Someofthelabelscreatedforcertainpropertiescanbereused.E.g.,thelabelforavariablexbeingdeclared(declx)mightbepartofsev-eralpropertiesandassuchcanbereused.Rightnow,weonlydothistoalimitedextendinGoanna.

TheotherreasonisthatNuSMVscaleswellwhenaddingmorelabels.Sincetheunderlyingcontrolstructureforonepropertyand15propertiesisthesame—onlythenumberoflabelsincreases—itisnotrequiredtorunNuSMVmoreoftenforalargernumberofproperties.Again,forreasonsoftheexactBDDencoding,itissometimesdif culttopre-ciselypredicthowlargeanincreaseinrun-timecanbeex-pectedbyaddingacertainnumberofproperties/labels.Theprecisionofouranalysisisverymuchdependentontheexactpropertyencoding.Someofourpropertiescomeintwo avors:Astrictversionandarelaxedversion.Thestrictversiontendstobeanunder-approximationofthepro-gram’sbehaviorandtherelaxedoneanover-approximation.Inthecaseofuninitializedvariables,thestrictversion agsaviolationifavariableisuninitializedonallpathsandtherelaxedversionreportsaviolationifthevariableisuninitial-izedonsomepath.Thedifferenceisinthepathquanti eroftheCTLformula(forall/existsapath).

Thestrictversionstypicallycreatezerofalsealarms,whiletherelaxedversionsarecomparabletootherstaticanalysistoolswhichdonotdoanyadditionalpathpruningorsimilartechniquestoremoveimpossiblepaths.

References

[1]T.BallandS.K.Rajamani.TheSLAMToolkit.InIntl.

Conf.onComputerAidedVeri cation(CAV’01),pages260–264,London,UK,2001.Springer-Verlag.

[2]M.Benedikt,W.Fan,andG.M.Kuper.Structuralproperties

ofxpathfragments.InICDT’03:Proceedingsofthe9thInternationalConferenceonDatabaseTheory,pages79–95,London,UK,2002.Springer-Verlag.

[3]B.Blanchet,P.Cousot,R.Cousot,J.Feret,L.Mauborgne,

A.Min´e;,D.Monniaux,andX.Rival.Designandimple-mentationofaspecial-purposestaticprogramanalyzerforsafety-criticalreal-timeembeddedsoftware.pages85–108,2002.

[4]S.Chaki,E.M.Clarke,A.Groce,andO.Strichman.Pred-icateAbstractionwithMinimumPredicates.InCHARME,pages19–34,2003.

[5]B.Chess.Improvingcomputersecurityusingextendedsta-ticchecking.InSP’02:2002IEEESymposiumonSecurityandPrivacy,page160,Washington,DC,USA,2002.IEEEComputerSociety.

6FutureWorkandConclusions

Summary.Inthisworkwepresentedanapproachtousemodelcheckingforsolvingstaticanalysisproblems.More-over,weimplementedGoanna,the rsttoolthatusesanoff-the-shelfmodelcheckerasastaticanalysisengine.Thisbringsthetwoworldsofstaticanalysisandmodelcheckingonestepclosertogether.Webelievethatinthefuturethiswillenabletheintegrationofmoresemantic-basedsoftwaremodelcheckingtechniquesintostaticanalysiswhileretain-ingoneuniformframework.

Theapproachhasbeenshowntobescalabletoreal-lifesoftwareprojects.Weevaluatedourprototypetoolwithre-specttoOpenSSLandshowedthatmost lesareanalyzedinthesameorderofmagnitudeasthecompilationitself.

9

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

[6]A.Cimatti,E.Clarke,E.Giunchiglia,F.Giunchiglia,M.Pi-store,M.Roveri,R.Sebastiani,andA.Tacchella.NuSMVVersion2:AnOpenSourceToolforSymbolicModelCheck-ing.InIntl.Conf.onComputer-AidedVeri cation(CAV2002),volume2404ofLNCS.Springer,2002.

[7]E.Clarke,D.Kroening,andF.Lerda.Atoolforchecking

ANSI-Cprograms.InToolsandAlgorithmsfortheCon-structionandAnalysisofSystems(TACAS2004),volume2988ofLNCS,pages168–176.Springer,2004.

[8]E.M.ClarkeandE.A.Emerson.Designandsynthesis

ofsynchronizationskeletonsforbranchingtimetemporallogic.InD.Kozen,editor,LogicsofProgramsWorkshop,IBMWatsonResearchCenter,YorktownHeights,NewYork,May1981,volume131ofLNCS,pages52–71.Springer-Verlag,1982.

[9]P.CousotandR.Cousot.Systematicdesignofprogram

analysisframeworks.InConferenceRecordoftheSixthAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages269–282,SanAntonio,Texas,1979.ACMPress,NewYork,NY.

[10]Coverity.PreventforCandC++..[11]D.DamsandK.S.Namjoshi.Orion:High-precision

methodsforstaticerroranalysisofCandC++programs.BellLabsTechnicalMemorandumITD-04-45263Z,LucentTechnologies,2004.

[12]D.Engler,B.Chelf,A.Chou,andS.Hallem.Checkingsys-temrulesusingsystem-speci c,programmer-writtencom-pilerextensions.InProc.SymposiumonOperatingSystemsDesignandImplementation,SanDiego,CA,Oct.2000.[13]D.EnglerandM.Musuvathi.Staticanalysisversussoftware

modelcheckingforbug nding.InIntl.Conf.onVeri ca-tion,ModelCheckingandAbstractInterpretation(VMCAI’04),2004.

[14]GimpelSoftware.FlexelintforC/C++.

/html/ ex.htm.[15]GrammaTech.CodeSurfer.

/products/codesurfer/.

[16]T.A.Henzinger,R.Jhala,R.Majumdar,andK.L.McMil-lan.Abstractionsfromproofs.InPOPL,pages232–244,2004.

[17]G.Holzmann.Staticsourcecodecheckingforuser-de ned

properties.Pasadena,CA,USA,June2002.

[18]K.RustanM.Leino,JamesB.SaxeandR.Stata.Checking

Javaprogramsviaguardedcommands.TechnicalReport1999-002,PaloAlto,CA,1999.[19]Klocwork.K7.

/products/klocworkk7.asp.[20]Microsoft.Prefast.

/whdc/devtools/tools/PREfast.mspx.[21]S.Muchnick.AdvancedCompilerDesignandImplementa-tion.MorganKaufmannPublishers,1997.[22]J.M¨uhlbergandG.L¨uttgen.BLASTingLinuxcode.In

Proc.ofthe11thInternationalWorkshoponFormalMeth-odsforIndustrialCriticalSystems(FMICS06),volume4346ofLNCS,Toappear.

[23]F.Nielson,H.R.Nielson,andC.L.Hankin.Principlesof

ProgramAnalysis.Springer,1999.[24]PolySpace.PolySpaceforC++.

/cpp.htm.

[25]J.-P.QueilleandJ.Sifakis.Speci cationandveri ca-tionofconcurrentsystemsinCESAR.InM.Dezani-CiancagliniandU.Montanari,editors,Proc.Intl.Sympo-siumonProgramming,Turin,April6–8,1982,pages337–350.Springer-Verlag,1982.

[26]B.SchlichandS.Kowalewski.ModelcheckingCsource

codeforembeddedsystems.InProc.oftheIEEE/NASAWorkshoponLeveragingApplicationsofFormalMethods,Veri cation,andValidation.NASA/CP-2005-212788,Sept2005.

[27]D.A.Schmidt.Data owanalysisismodelcheckingof

abstractinterpretations.InACMSIGPLAN-SIGACTSympo-siumonPrinciplesofProgrammingLanguages(POPL’98),NewYork,NY,USA,1998.ACMPress.

[28]D.A.SchmidtandB.Steffen.Programanalysisasmodel

checkingofabstractinterpretations.InIntl.SymposiumonStaticAnalysis(SAS’98),pages351–380,London,UK,1998.Springer-Verlag.

10

本文来源：https://www.bwwdw.com/article/83mj.html