F. Model checking software at compile time(11)

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.