流年开花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
