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