Model-based analysis of configuration vulnerabilities

C.R.RamakrishnanandR.Sekar

cram,sekar@cs.sunysb.eduDepartmentofComputerScienceStateUniversityofNewYorkStonyBrook,NY11794.

Abstract

Vulnerabilityanalysisisconcernedwiththeproblemofidentifyingweaknessesincom-putersystemsthatcanbeexploitedtocompromisetheirsecurity.Inthispaperwedescribeanewapproachtovulnerabilityanalysisbasedonmodelchecking.Ourapproachinvolves:

Formalspecificationofdesiredsecurityproperties.Anexampleofsuchapropertyis“noordinaryusercanoverwritesystemlogfiles.”

Anabstractmodelofthesystemthatcapturesitssecurity-relatedbehaviors.Thismodelisobtainedbycomposingmodelsofsystemcomponentssuchasthefilesystem,privi-legedprocesses,etc.

Averificationprocedurethatcheckswhethertheabstractmodelsatisfiesthesecurityproperties,andifnot,producesexecutionsequences(alsocalledexploitscenarios)thatleadtoaviolationoftheseproperties.

Animportantbenefitofamodel-basedapproachisthatitcanbeusedtodetectknownandas-yet-unknownvulnerabilities.Thiscapabilitycontrastswithpreviousapproaches(suchasthoseusedinCOPSandSATAN)whichmainlyaddressknownvulnerabilities.

ThispaperdemonstratesourapproachbymodellingasimplifiedversionofaUNIX-basedsystem,andanalyzingthissystemusingmodel-checkingtechniquestoidentifynontrivialvul-nerabilities.Akeycontributionofthispaperistoshowthatsuchanautomatedanalysisisfeasibleinspiteofthefactthatthesystemmodelsareinfinite-statesystems.Ourtechniquesexploitsomeofthelatesttechniquesinmodel-checking,suchasconstraint-based(implicit)representationofstate-space,togetherwithdomain-specificoptimizationsthatareappropriateinthecontextofvulnerabilityanalysis.

Clearly,arealisticUNIXsystemismuchmorecomplexthantheonethatwehavemod-elledinthispaper.Nevertheless,webelievethatourresultsshowautomatedandsystematicvulnerabilityanalysisofrealisticsystemstobefeasibleinthenearfuture,asmodel-checkingtechniquescontinuetoimprove.

Keywords:Vulnerabilityanalysis,intrusiondetection,computersecurity,modelchecking,automatedverification.

1Introduction

Systemconfigurationvulnerabilitiescanbetracedbacktoclassicproblemsinsoftwareengineer-ing,suchasunexpectedinteractionsbetweendifferentsystemmodulesandviolationofhiddenassumptions.Forinstance,consideravulnerabilitythatexistedinearlyversionsofthefingerdservice.Inservicingaquery“fingeruser,”thisprogramneedstoreadafilenamed.planinthehomedirectoryofuser.Thefingerdservicerunswithrootprivileges,andintheearlierver-sionsofUNIXusedtoopenthe.planasroot.Inthepresenceofsymboliclinks,thiscreatesthefollowingvulnerability.Usercouldsymbolicallylinkafileashis/her.planevenifhasnoreadaccessto.Usercanthenreadbysimplyrunningfinger!Thisvulnerabilityarisesduetotheinteractionbetweenthewaythefingerserveroperatesandthewaysymboliclinksareimplemented.

Asasecondexample,considerthevulnerabilityinvolvingthemailnotificationprogramcomsat,whichwaitsforreportsofincomingmailforanyuserandprintsthefirstfewlinesofthemessageontheterminalonwhichtheuserislogged.Thisterminalisdeterminedfromthefile/etc/utmp,whichusedtobeconfiguredasworld-writable(sothatitcanbewrittentofromuserlevelatthetimeoflogin).Amalicioususercanmodify/etc/utmp,substituting/etc/passwdintheplaceoftheterminalthathe/sheisloggedon.Theusercanthensendmailtoselfcontainingalinethatstartswithroot::0:0:(whichmeansthatroothasanemptypassword).Uponreceivingthismail,comsatwilloverwritethepasswordfilewiththemessage.Theusercannowloginasrootwithoutprovidingapassword.

1.1OurApproach

Formalmethodsareagoodchoicetoaddresssoftwareengineeringproblemsthatariseduetounexpectedinteractionsamongsystemcomponents[9].Inthispaper,wedescribeanapproachforanalyzingsystemconfigurationvulnerabilitiesusingtechniquesdrawnfromformalmethodsresearch.Ourapproachinvolves:

Constructionofhigh-levelmodelsofsystemcomponents.Inordertodetectthekindofvul-nerabilitiesdescribedabove,wewouldstartwithabstractmodelsthatcapturethebehaviorofUNIXfilesystem,comsatandmailerprograms,andamodelofuserbehavior.Currently,wearedevelopingtheseabstractmodelsmanually.Infuture,weexpectthatthemodelex-tractionprocesswillbemachine-assisted,employingprogramanalysistechniques.Formalstatementofdesiredsecurity-relevantpropertiesofthecompositesystem.Vulner-abilitiescanbeviewedas“flaws”insystemconfigurationthatcanbeexploitedtoviolatecertainsecurityobjectivesoftheoverallsystem.Todetectvulnerabilities,weneedaformalstatementofsuchsecurityproperties.Oneexampleofapropertyisthatnoordinaryusercanoverwritesystemlogfiles.Anotherexampleisthatthepasswordfilecannotbemodifiedexceptbyasuperuser,orbyusingapasswordchangingprogram.

Automatedanalysisofsystemmodeltocheckdeviationfromdesiredsecurityproperties.Configurationvulnerabilitiescanbeidentifiedbyanalyzingtheoverallsystembehavior(ob-

tainedbycomposingthemodelsdevelopedabove),anddeterminingifitviolatesthedesiredsecurityproperties.Weusemodel-checking[6,7,16]forthisanalysis.Animportantbenefitofmodelcheckingisthatwhenapropertyisviolated,amodelcheckerprovidesacounterex-amplethatshowshowthepropertyisviolated.

ThispaperdemonstratesourapproachbymodellingasimplifiedversionofaUNIX-basedsystem,anddiscoveringnontrivialconfigurationvulnerabilitiesinthissystemthroughautomatedanalysis.Clearly,arealisticUNIXsystemismuchmorecomplexthantheonethatwehavemodelledinthispaper.Nevertheless,webelievethatourresultsshowthatautomatedanalysisofrealisticsystemsarefeasibleinthenearfuture,especiallysincefastertechniquesformodel-checkingarebeingdeveloped.

Althoughtheuseofmodel-checkinghasbeenexaminedinrelatedcontextssuchasverificationofcryptographicprotocolsandnetworkvulnerabilities[20],oursisthefirstattemptatusingmodel-checkingforsystemconfigurationvulnerabilityanalysis.Oneoftheprincipaldifficultiesinthiscontextisthatsystemmodelstendtopossessaninfinitenumberofstates.Thisisbecauseweneedtomodelsuchaspectsofthesystemasfilenamesand(nested)directorystructures,withtheabilitytocreateordestroyaninfinitenumberoffiles.Traditionalmodel-checkingtechniques(suchasthoseemployedin[20])arelimitedtofinite-statemodelsonly.

Akeycontributionofthispaperistoshowthatnontrivialvulnerabilitiescanbediscoveredusingautomatedmodel-basedanalysis,inspiteofthefactthatthesystemmodelsareinfinite-state.Itshowsthatknowntechniquessuchasmodelabstractionandconstraint-basedrepresentationscanbeemployedtotackletheinfinite-statemodel-checkingproblemsthatariseinvulnerabilityanalysis.

Therestofthispaperisstructuredasfollows.InSection1.2,wedescribepreviousapproachesforvulnerabilityanalysisandsummarizethemainadvantagesofamodel-basedapproach.InSection2,wedescribeourapproachformodellingasimplifiedsubsetofUNIX.OuranalysistechniqueisdescribedinSection3.TheresultsofthisanalysisarepresentedinSection4.Finally,concludingremarksappearinSection5.

1.2RelatedWork

Researchinvulnerabilityanalysishasfocusedprimarilyonidentificationofconfigurationerrorssuchasimproperfilepermissionsettings.Existingworks[2,11,23]employasetofrulesthatenumerateknowncausesforvulnerabilities.Wecalltheseworkscollectivelyrule-based.WidelyusedtoolssuchasCOPSandSATANsearchforoccurrencesofsuchknownvulnerabilities[11].However,thegenerationoftherulesreliesonexpertknowledgeaboutinteractionsamongmanycomponentsofthesystem.Fewexpertshaveacompleteunderstandingoftheinteractionsamongallcomponentsofamoderncomputersystem.Issuessuchasraceconditions,manypossibleinterleavings,hiddenassumptionsetc.[3]makeitveryhardforhumanstocomeupwithallsuchrules.

Amodel-basedapproachdoesnotsufferfromthesedisadvantages.Humaninvolvementisneededprimarilytodevelopmodelsofindividualsystemcomponents.Theproblemthatishardforhumanreasoning,namely,thatofreasoningaboutinteractionsamongsystemcomponents,is

relegatedtoamechanicalprocedure.Theadvantagesofamodel-basedapproachare:

Identificationofknownandunknownvulnerabilities.Analysisofformalmodelscanidentifyknownandas-yet-unknownvulnerabilities.Incontrast,therule-basedapproacheshavebeenlimitedtoexaminingthesystemforknownvulnerabilities.

Modularity.Theeffortrequiredtoaddnewsystemcomponents(e.g.newprivilegedpro-gramsorsignificantsoftwareupgrades)isdeterminedonlybythenewcomponentstobeadded.Modelsofexistingcomponentsneednotbechanged.Thiscontrastswithrule-basedapproaches,wherenewrulesneedtobeaddedthatcapturenotonlytheinteractionsamongnewcomponents,butalsointeractionsbetweennewandoldcomponents.

Generatingpatternsformisuseintrusiondetection.Whenvulnerabilitiesareidentifiedbyouranalysis,wemaysometimesbeabletorectifythem.Atothertimes,theremaybenoim-mediatefix,asitmayrequirechangestovendor-providedsoftware,orsincethechangesmayinterferewithlegitimatefunctionalityofthesystem.Asecondlineofdefenseforvulnera-blesystemsismisuseintrusiondetection,wheresystemuseismonitoredinordertodetectknownexploitations.Theexploitscenariosareusuallyspecifiedbyanexpert,whiletheprocessofdetectionofexploitsisautomated.Theapproachoutlinedinthispaperenablesautomationofthefirsttaskaswell,sincethecounterexamplesgeneratedbyourmodel-checkingtechniquecorrespondtoexploits.Wecanmechanicallytranslatetheseexploitsintopatternsforamisuseintrusiondetectionsystem.

Automaticgenerationofrulesforcheckingvulnerabilitiesofspecificconfigurations.Theproposedapproachcandetectsystemvulnerabilitiesevenwhennoinformationisprovidedabouttheinitialsystemconfiguration.Ourmodel-checkingtechniqueproducesexploitsce-nariosthatareconditionaluponthe(unspecified)initialconfiguration.Eachofthesecondi-tionsthencaptureapotentialvulnerabilitythatcanbecheckedusingarule.Themainbenefitofusingtheserulesisthattheycanpotentiallybecheckedmoreeconomically(intermsoftimeandmemoryusage)thanrunningthemodelchecker.

Thispaperbuildsonsomepreliminaryresultsonmodel-basedvulnerabilityanalysiswehadre-portedearlierin[17].Sincethen,RitcheyandAmmann[20]havesuggestedapromisingapproachforautomatingnetworkvulnerabilityanalysis.Theirapproachstartswithhigherlevelmodelsthanours.Theirmodelscaptureknownexploitsonindividualsystems,e.g.,thatagivenversionofawebservercontainsavulnerabilitythatallowsaremoteusertogainaccessasalocaluser,andthatacertainhostisrunningthisversionoftheserver.Modelcheckingisthenusedtocheckiftheseexploitscanbe“strungtogether”toachieveagreaterdegreeofaccessthanwhatcanbeobtainedbyindividualexploits.Incontrast,ourapproachisaimedatdiscoveringtheindividualexploitsfrommodelsof(legitimate)behaviorsofsystems.Anotherimportantdifferenceisthattheirmod-elsarefinite,whichenablesthemtousewidelyavailablemodelcheckingtoolssuchasSMV[8]andSPIN[13]toperformvulnerabilityanalysis.Incontrast,weneedtodealwithinfinitestatesystems.Thisisbecausefinitemodelscannotcapturecomponentssuchasfilesystemswherefilescanbeadded,renamedorremoved,andthereisnoboundonhowmanytimestheseoperationsmayberepeated.

2ModellingSecurity-RelatedBehaviorsofSystems

Inthissection,wefirstdescribeourmodelforasmallsubsetofaUNIX-basedsystem.Thissubsetcapturesasimplifiedviewofthefilesystemandotheroperatingsystemfacilities,andissufficienttouncovernontrivialvulnerabilitiesduringtheanalysisprocess.Webeginwithashortdescriptionofthelanguageweuseformodelling,describedinenoughdetailtounderstandthemodels.(Acompletedescriptionofthelanguageisnotrelevantforthepurposesofthispaper,andhencenotincludehere.)

2.1ModellingLanguage

WedescribeourmodelusingamodellinglanguagesimilartoCSP[12],butextendedwithobject-orientedcapabilities.SinceourunderlyingmodelcheckerisbasedontheProloglanguage,manyfeaturesofthemodellinglanguagearesimilartothoseinProlog.Inaddition,someofthesyn-tacticfeaturesaresimilartothoseusedinPromela,themodellinglanguageusedintheSPIN[13]verificationsystem.

Inthislanguage,asystemismodelledasacollectionofconcurrentlyexecutingprocessesthatcommunicatewitheachother.Eachprocessisviewedasanobject.Itsinternalstateisencapsu-lated,andcannotbeaccessedbyotherprocesses.Communicationamongprocessestakesplaceviamethodinvocations.Methodinvocationissynchronous:itcausestheinvokingprocesstoblockuntilthemethodinvocationiscompleted,andreturnvaluessentback.

Objectsareinstancesofclasses.Aclassdefinitionconsistsofthedefinitionoftheencapsulatedstate,definitionsofexternallyvisiblemethodsanddefinitionsoflocalmethods(otherwiseknownasprivatemethodsorhelperfunctions).Singleinheritanceissupportedinthelanguage.Thus,aclassdefinitionisoftheform:

classClassName(DataMemberNames)[:BaseClassName(DataMemberNames1)]MethodDefn+

Anobjectiscreatedbyinvokingtheclassnamewithparameterscorrespondingtoitsdatamem-bers,usingthesyntax:

ClassName(DataMembers)

Methodsaredefinedusingthefollowingsyntax.

[private]MethodName(Parameters)::=MethodBody.

LikepredicatesintheProloglanguage,methodinvocationsinthislanguagealwaysreturnabooleanvalue.Inaddition,someoftheargumentstoamethodmaygetinstantiatedasaresultofinvoca-tion.Thisfeatureisusedtocommunicatereturnvalues.Weusetheconventionthatallofthereturnparametersappearaftertheinputparametersinmethodinvocations.

Thelanguagesupportsbasicdatatypessuchasbooleans,integers,floatsandstrings.Usualoperationsonthesetypesarealsosupported,andcanbeusedtoconstructcomplexexpressionsfromvalues(orvariables)ofbasictypes.Thelanguagealsosupportscompoundtypesbasedonanalgebraictypesystem,similartothatprovidedbyProlog.Thesetypesareusedtorepresentstructureddatasuchasfilenames,filecontents,andthecontentsoftheentirefilesystem.Twoofthemostcommoncompoundtypesaretuplesandlists.

Weassumethatdifferentprocessesexecuteconcurrently.Thelanguageusesaninterleavingsemanticstodeterminetheresultofconcurrentexecutions.Atthelowestlevel,operationssuchasassignmentareperformedatomically.

Amethodbodyconsistsofasequenceofoperations.Alloperationsreturnabooleanvalue,withthevaluetruedenotingsuccessfulcompletionoftheoperationandfalsedenotingfailure.Methodinvocationbeginswiththeexecutionofthefirstoperationinthesequence.Ifthisoperationsucceeds,thenthenextoperationisexecutedandsoon.Ifalloftheoperationsinasequencesucceed,thenwesaythattheentiresequencesucceeds.Otherwise,thesequencefails,returningthevaluefalse.Insuchacase,themethodinvocationitselfreturnsfalse,indicatingfailure.Operationscaneitherbeprimitiveorcompound.Aprimitiveoperationiseitheramethodinvocation,oranapplicationofapredefinedpredicate,suchasequalityorotherrelationalopera-tions.NotethattheequalitypredicatehasthesamesemanticsasinProlog—inparticular,itcanbindvaluestovariables.Acompoundoperationisconstructedfromprimitiveoperationsusingthefollowingconstructs:

Atomicexecution:atomicOpSeqhasthesamesemanticsasOpSeq,exceptthattheopera-tionswithinOpSeqwillbeexecutedatomically,i.e.,theirexecutionwillnotbeinterleavedwiththeexecutionofotherprocesses.

Alternation:OpSeq1OpSeq2willsucceedifeitherOpSeq1orOpSeq2succeeds.Other-wise,itwillfail.NotethatOpSeq2willbeexecutedonlyifOpSeq1fails.

Parallelcomposition:OpSeq1OpSeq2willresultinconcurrentexecutionofoperationsinOpSeq1andOpSeq2.Ifeitherofthesesequencessucceed,thentheentireconstructsucceeds.

if-then-else:ifOpSeq1thenOpSeq2elseOpSeq3willresultinexecutionofOpSeq1.Ifitsucceeds,thenOpSeq2willbeexecuted,anditssuccessorfailurewilldeterminethesuccessorfailureoftheif-construct.IfOpSeq1failsthenOpSeq3willbeexecuted,anditssuccessorfailurewilldeterminethesuccessorfailureoftheif-construct.

Guardedcommand:G1OpSeq1G2OpSeq2GnOpSeqnhasthefollowingsemantics.Oneoftheguardsthatevaluatetotrue,sayGk,willbechosenarbitrarily,andthecorrespondingoperationsequenceOpSeqkwillbeexecuted.Ifthisse-quencefails,analternativeguardthatevaluatestotruewillbechosen,andtheoperationsequencecorrespondingtothatguardwillbeexecuted.Ifnoneoftheoperationsequences(correspondingtoguardsthatevaluatetotrue)succeed,thentheguardedconstructfails.Otherwise,itsucceeds.Forsimplicity,werestricttheguardstocontainonlypredefinedoperations,suchasequalitychecking.Theycannotcontainmethodinvocations.

Loopconstruct:loopOperationSequenceconstructhasthemeaningthatOperationSe-quencewillbeexecutedrepeatedly.Moreprecisely,itsbehaviorcanbespecifiedusingtherecursivedefinition

loopOpSeq=OpSeq,loopOpSeq

SemanticsofoperationfailureissimilartothatofProlog.Whenafailureoccurs,executionback-trackstothepointwhereanalternativeexecutionpathcouldbetaken.Allvariablebindingsmadebetweenthispointandthepointoffailureareundone,andexecutionnowproceedsdowntheal-ternatepath.Notethatthisimpliesthat(a)thesameoperationmaysucceedmanytimes,possiblywithdifferentvariablebindings,and(b)inanoperationsuchasOpSeq1OpSeq2,itispossibleforOpSeq1tosucceed,butasubsequentoperationthatfollowsalternationmayfail,inwhichcase,executionmaybacktracktothealternationconstruct,atwhichpointOpSeq2maybetried.Additionaldetailsaboutthelanguageareprovidedtogetherwiththeexamplesbelow.

2.2ModelofFileSystem

Thestateofafilesystemismodelledasasetoftuplesoftheform(FileName,Owner,Group,Permissions,Content).Thefilenameisrepresentedasalist:anamesuchas“/a/b/c”wouldberepresentedas[a,b,c].Theownerandgrouparerepresentedasintegers.ThepermissionfieldcapturestheusualUNIXpermissioninformationonfiles.Thefilecontentisrepresentedasnormal(C)fornormalfileswhosecontentisgivenbyC,andlink(F)for(symbolic)linkstoanotherfileF.

Tosimplifythepresentation,wearenotrepresentingdirectoriesasfiles.However,thedirectorystructureiscapturedimplicitlyinthewayfilesarenamed.Ineffect,thismeansthatinformationsuchasdirectorylevelpermissioncannotberepresenteddirectly;itmustbepropagatedandrepre-sentedaspermissiononfilescontainedinthedirectory.

ThefilesystembehavioriscapturedbythefileSystemclassshownbelow.NotetheuseofProlog-styleconvention:variablenamesstartwithacapitalletter,whileconstant,classandfunctionnamesstartwithalowercaseletter.

Thefilesystemsupportsoperationstoreadandwritefiles.Thewriteoperationcanalsobeusedforfilecreation,whilearemoveoperationisprovidedforfiledeletion.Fileattributessuchasownershipandpermissioncanbechangedusingtheoperationschmod,chgrpandchmod.Ourfilesystemmodeldoesnotcapturehardlinks,butsymboliclinkscanbecreatedusingthesymlinkoperation.Allofthefileoperationsmakeuseofahelperfunctioncalledresolvethatfirstresolvessymboliclinksintorealfilenames,andthenperformspermissionchecking.

classfileSystem(S){

//publicmethods

read(File,U,G,C)::=resolve(File,U,G,read,F1),getContent(F1,C)write(File,U,G,C)::=resolve(File,U,G,write,F1),updateFile(F1,C)remove(F,U,G)::=resolve(File,U,G,write,F1),delete(F1)chown(F,U,G,O)::=resolve(F,U,G,root,F1),chngOwner(F1,O)chgrp(F,U,G,O)::=resolve(F,U,G,owner,F1),chngGroup(F1,G)chmod(F,U,G,M)::=resolve(F,U,G,owner,F1),chngMod(F1,M)symlink(L,F,U,C)::=write(L,U,G,link(F))

AnumberofotherhelperfunctionssuchasgetContentandupdateFileareusedintheabovemethods.Thedefinitionofthesehelperfunctionsisstraightforward.Ofthese,weprovidethedefinitionofgetContentbelow,whileomittingtheothersintheinterestofconservingspace.

getContent(F,C)::=member((F,U,G,P,normal(C)),S)

Thehelperfunctionresolveisnontrivial,andweprovideitsdefinitionbelow.Itsparametersare:thefilenameFtoberesolved,theuserandgroupidentifiersUandGwithrespecttowhichpermissioncheckingneedstobedone,andanoptionargumentOpt.ItreturnstheresolvednameF1inthefifthparameter.Theresolvemethodwillfaileitherifthefilenamedoesnotexist,orifthepermissioncheckfails.

resolve(F,U,G,Opt,F1)::=resolveLink(F,F2),

member((F2,O,G1,P,normal(C)),S),//checkiftupleispresentinsetS((U=root)||//nopermissionchecksforroot((Opt=owner),(U=O))||//Opt=owner:checkifuserUisfileowner((Opt=write),

(((U=O),(P=(S,(R,1,X),G2,U2)))|//ownerpermmember(U,G1),(P=(S,O1,(R,1,X),U1))|//grpperm(P=(S,O1,G2,(R,1,X))))//userpermthenresolveLink(F,F1))||

((Opt=read),....)||

....//otheroptionsomitted

resolveLink(F,F1)::=if(member((F,U,G,P,link(F2)),S)thenresolveLink(F2,F1)

elseF1=F

TheresolvemethodusesahelperfunctionresolveLink.Thelatterisarecursivefunctionthatkeepsfollowingsymboliclinksuntilanormalfilenameisidentified.ItdoesthisbycheckingifafilenamedFispresentinthefilesystem.(Notethatthestateofthefilesystemitselfisbeingcapturedasalist,andmemberisapredicatethatisusedtosearchforaspecifiedelementinthelist.)IfFisnotpresent,thenresolveLinkfails.Otherwise,ifthecontentofFisoftheformlink(F2),thenresolveLinkisinvokedrecursivelytofollowthislink.Otherwise,itmustbeanormalfileandhenceFisreturnedastheresolvedname.NotethatthedefinitionofresolveLinkcorrectlycapturesthefactthatnopermissioncheckingisdoneforsymboliclinks.

Oncesymboliclinksareresolved,resolveproceedstocheckfilepermissions.NotethatnocheckingisdoneiftheuseridUcorrespondstothatofroot.Otherwise,permissioncheckproceeds,basedonthevalueofoptionOpt.Iftheoptionisread,writeorexecute,thecor-respondingpermissionsarechecked.Iftheoptionisowner,thenthepermissioncheckoperationneededisoneofcheckingiftheuseridprovidedasaparameteristhesameasthefileowner.

2.3ModelofUNIXProcesses

UNIXprocessesaremodelledusingabaseclasscalledunixProcthatcapturesbehaviorscommontoallprocesses,plusaderivedclassperprogramthatwewishtomodel.ThestateofaunixProcobjectischaracterizedbyitsrealandeffectiveuser/groupidentifiers,plusinformationaboutgroupsknowntothesystem.Inaddition,itcontainsareferencetothefilesystemobject,andthevaluesofcommandlinearguments.Itprovideshelperfunctionsthatcorrespondroughlytosystemcalls.

classunixProc(UID,EUID,GID,EGID,ArgList,FS,UserGroups){

read(F,C)::=FS.read(F,EUID,EGID,C)write(F,C)::=FS.write(F,EUID,EGID,C)

..//definitionofseveralothersimilarmethodsisomitted.

run(F,ArgList1)::=//correspondstofork+exec(F)inUNIXFS.resolve(F,EUID,EGID,exec,F1),

ifFS.resolve(F1,EUID,EGID,setuid,F2)

thenFS.getOwner(F1,EUID1)elseEUID1=EUID,

ifFS.resolve(F1,EUID,EGID,setgid,F3)

thenFS.getGroup(F1,EGID1)elseEGID1=EGID,

FS.getContent(F1,program(C)),//F1mustcontainaprogramcreate(C,UID,EUID1,GID,EGID1,ArgList1,FS,UserGroups)

//createisalanguageconstructthatresultsincreationof//anewobjectbelongingtotheclassofitsfirstargument.//Thestateoftheobjectshouldcorrespondexactlytothe//parameterssuppliedtocreate

....//Othermethodsomitted}

SubclassesofunixProcdefineexternallyaccessiblemethods,andmakeuseofthemethodsprovidedbyunixProcclass.Theyalsoneedtoprovideamainfunctionthatgetsexecutedassoonasaprocessiscreated.Theprocessterminates(andtheobjectdestroyed)whenthemainfunctionterminates.

BasedonunixProc,wecandefineanlprclassasfollows.Atthelevelofthefilesystem,lpreithercopiesthefiletobeprintedintoaspooldirectoryorlinksittheresymbolically,dependinguponacommandlineoption.

//Inadditiontousualprocessparameters,lprtakes2arguments:

//thenameofthefiletobeprinted,andanoptionthatindicatesifthis//fileistobecopiedtothespooldirectorybeforeprinting,orjust//symbolic-linkedfromthespooldirectory.classlpr(U,EU,G,EG,[File,Opt],FS,UG):

unixProc(U,EU,G,EG,[File,Opt],FS,UG){main()=

atomic{//Nisusedtocreateatemporarynameforthespoolfile

read([var,spool,lp,count],N),

write([var,spool,lp,count],(N+1)%1000)},

FS.resolve(File,U,G,read,F1),//accessiblityofFilecheckedforU,if(Opt=s)//butsubsequentoperationsare

thensymlink([var,spool,lp,N],File)//performedwithrootprivilegeelseread(File,C),write([var,spool,lp,N],C)}}

Inasimilarmanner,wecandefinethebehaviorofahighlysimplifiedmailreceiver/senderasfollows.Thismailserveroperatesbystoringeveryincomingemailmessageinaspooldirectorycorrespondingtotherecipient.Forsimplicity,wemodeltheactofstoringinawaythatlosespreviouscontentsofthespoolfile.

classmailer(FS,UG):unixProc(root,root,sys,sys,[],FS,UG){

send(U,M)::=write([var,spool,mail,U],M)}

Finally,wemodeltheactionofthecomsatmailnotifierprogram.Itlooksupthefile/etc/utmptoidentifytheterminalwhereeachuserisloggedin.Wheneveranewmessageisreceivedforauser,comsatprintsthemessageontheuser’sterminal.

Werepresentthecontentofthe/etc/utmpasalistofrecords.Weaddadditionalhelperfunctionstothefilesystemmodeltosupportwritingandreadingfromsuchstructuredfiles.OfparticularinterestisahelperfunctioncalledreadRecthatallowsaccesstoaspecificrecordwhosefirstcomponentisspecifiedasanargumenttoreadRec.

classcomsat(FS,UG):unixProc(root,root,sys,sys,[],fs,ug){

main()::=loop{

read([var,spool,mail,Rcvr],Msg)readRec([etc,utmp],Rcvr,Tty),write(Tty,Msg)}

}

Theloopconstructindicatesthattheoperationsinsidetheloopareexecutedforever,untiltheprocessiskilled.TheseoperationsmakeuseofanunboundvariableRcvr.Suchvariablesaretreatedasexistentiallyquantified.Operationally,thisamountstobindingthevariabletoanarbitraryvalueinitsdomain.Thus,comsatnondeterministicallychoosessomefileinthemaildirectorysuchthatthecorrespondinguserisloggedin,andprintingthemessageontheuser’sterminal.Data-nondeterminism,ascapturedbytheuseofsuchunboundvariables,isakeymech-anismthatsimplifiesourmodels.

Wenowdevelopamodelofauser.Theuser’sbehaviorisalsohighlynondeterministicinnature:he/sheselectsanarbitraryfileinthesystem,andmayreadthisfileoroverwriteitwitharbitrarycontent.Theusermayalsorunarbitrarycommands,orsendanarbitrarymessagetoanarbitraryuser.Arbitrarychoiceindatavaluesiscapturedbyusingunboundvariables.Thearbitrarychoiceamongthecommandsiscapturedbytheguardedcommandconstructwithintheloop.Theguardedcommandconstructiswithinaloop,whichindicatesthattheuserwillkeepperformingtheseactionsindefinitely.

classuser(U,G,FS,UG):unixProc(U,U,G,G,[],FS,UG){

main()::=loop{

true->read(F1,C)||true->write(F1,C)||true->run(lpr,Args)||true->mailer.send(U1,M1)}

Finally,weputalloftheclassesdefinedsofarintoasinglesystemmodelusingaclasscalledinit.Notetheuseofoperator,whichdenotesparallelcompositionofmultipleprocesses.

classinit(FS,UG){

main()::=mailer(FS,UG)|comsat(FS,UG)|user(U,G,FS,UG)}

3DetectingSystemVulnerabilities

Inourapproach,weusemodelcheckingtechniquestoanalyzethebehaviorsofthesystemmodel.Inthesimplestcase,securitypropertiesareinvariants:propertiesthatmustholdateverystateofthesystem.Forinstance,thesimplemodeldescribedintheprevioussectiondoesnotmodellegitimatewaystomodifythepasswordfile(e.g.,passwd);hence,theconstancyofthepasswordfileisadesiredsysteminvariant.InSection3.3wedescribehowmorecomplex(temporal)propertiesthatdependonorderofeventscanbespecified.

Oneoftheimportantfeaturesofmodelcheckingtechniquesistheirabilitytogeneratecounter-examples,whicharesequencesofstatesthatleadtoviolationofthegivenproperty.Inourap-plication,thecounter-examplescorrespondtothestepsthatanattackercanusetoexploitsystemvulnerabilities.However,currentmodelcheckingtoolscannotbeusedasis,sincemanycompo-nentsofthesystemmodeldescribedinSection2haveinfinitelymanyreachablestates(e.g.,thestatesofthefilesystem).Currentmodelcheckingtoolsworkmainlywithfinite-statesystems.HencewedevelopedaprototypemodelcheckerbasedcloselyontheXMCsystem[18],asystemthathasbeendevelopedbyoneoftheauthorsofthispaper.XMCcanhandlecertainclassesofinfinite-statesystemsbyusingimplicitrepresentationofstatespaceusingconstraints.TheXMCsystemisimplementedusingtheXSBtabledlogicprogrammingsystem[22]bycastingthemodelcheckingproblemasaqueryevaluationproblem.TablingprovidesstrongerterminationpropertiesforXSBincomparisonwith(untabled)logicprogrammingsystems.Inparticular,computationsforsolvingequationsusingiterativeprocedures(e.g.,fix-pointiteration)canbeprogrammedveryeasily,thusmakingXSBanidealplatformforrapidimplementationofprogramanalyzersandmodel-checkers.

InXMC,thetransitionrelationofthesystemmodelistreatedasanexternaldatabase;theverificationproblemissolvedbyrunningreachabilityqueriesoverthisdatabase.Ourprototypefollowsthesameapproach.Thesignificantdifferenceisthatthereachabilityqueriesaremadeoveraninfinitetransitionsysteminthecaseofvulnerabilityanalysis.ThisinfinitenessishandledbyexploitingthefollowingfeaturesoftheXSBsystem.

FollowingXMC,werepresentstatesofthesystemmodelusingterms.Thedifferenceinourprototypeisthatthesetermsmaycontainlogical(unbound)variablesthatrepresentunknowndatainthesystemmodels.

Weuseconstraintsbetweentermstorelatestatesinthesystemmodel.Inthefinite-statecasehandledbyXMC,thestatesarerepresentedbyground(i.e.variable-free)terms,andrelationbetweenstatesisasimpletable.Inourprototypewerelatestates,nowrepresentedbypossiblynon-groundterms,usingequalityconstraintsamongthevariables.

WeusethepoweroftablinginXSBtoidentify“similar”states(inourcase,statesthatdifferonlyinthenamesofboundvariables)andtoreusecomputationswhenastatesimilartooneencounteredearlierisseenagain.

Inourimplementation,wetranslatethehigh-levelmodelofthesystemintoaPrologdatabase(asetoffacts)thatrepresentsthesystem’stransitionrelation.AsnotedinSection2,ourmodelling

languageresemblesProloginmanyways.Thisfactorconsiderablysimplifiesthetranslational-gorithm.(Infact,thetranslationisverysimilartothatdescribedin[10]fortranslatingprocessesdescribedinavalue-passingprocessalgebraintologicprogramrulesrepresentingthetransitionrelation.)Althoughthetranslationalgorithmisconceptuallysimple,itsimplementationstillre-quiressignificanteffort.Giventhesmallscaleofourmodels,wehavefounditeasiertoperformthistranslationmanually.

Inthefollowing,wefirstassumethatthepropertytobeverifiedisspecifiedasaformulaintemporallogic[14].Wethendescribethenotionofintentionsmodel(seeSection3.3)whicheliminatestheneedtoencodecomplexsecuritypropertiesintemporallogic.Themodelcheckingprocedureisimplementedasreachabilityquery,andisevaluatedusingtheXSBsystem.

3.1ModelCheckingInfinite-StateSystems

Theinfinitenessinthestatespaceofasystemarisesfromtwofactors—datanondeterminism(in-finitebranchingfactor),andexecutionhistories(infinitelylongpaths)—eachofwhichishandledusingadifferentfeatureofthemodelchecker.

Infinitenessduetodatanondeterminismishandledbytermconstraints.Recallthatdatanon-determinismarisesfromunboundvariablesinthesystemmodel.Termconstraintscapturethepossiblevaluesofsuchvariablessuccinctly.TheconstraintsarerepresentedandmanipulatedbytheXSBsystemitself,andneednofurtherprogramming.Forinstance,considertheproblemofverifyingwhether/etc/passwdcanbeoverwritteninthesystemmodelinSection2.Observefromtheexamplethatthesystemcanevolvewhenanarbitraryuserchoosestoperformawriteactionofsomefile,orwhenausersendsmail.Withthelogic-programming-basedmodelchecker,neithertheusernorthemessageneedstobeboundtoanyparticularvalue:werepresenttheseaslogicalvariables.Unificationandbacktrackingautomaticallygeneratethecasesofinterest,bybindingthevariablesonlytovaluesthatleadtovulnerabilities.Forinstance,whenausersendsmail,theprocesscomsatisenabled,whichsendsanotification(usingwrite)tothedestina-tionspecifiedin/etc/utmp.Notethat,atthispoint,neitherthecontentsnorthepermissionson/etc/utmpareknown.Themodelcheckertrieseachcaseinturn,bybindingthevariablestotheneededsetofvalues.If/etc/utmpisunreadableoriftherequiredentry(thedestinationfornotifyingincomingmail)isnotfound,nonotificationissentandthesystemrevertsbacktoitsoriginalstate.Ontheotherhand,ifthedestinationfornotificationispresentin/etc/utmp,thenawritetoisissued.Sincethecontentsof/etc/utmpareunknown,notethatwillbeleftasavariable.Ifthedestinationcanbe/etc/passwd,thenitisindeedpossibletochangethepasswordfileinourmodel.Thus,themodelcheckingalgorithmconcludesthatif/etc/utmpspecifies/etc/passwdasoneofthenotificationdestinations,thenitispossibletoviolatesystemsecurity.

Infiniteexecutionsequencesarehandledbyabstractingthesequencestofinite(possiblyre-peating)segmentsofacertainkind.Ofparticularimportanceistheabstractionthatboundsthelengthsofsequences.Capturingunknown(ordon’t-care)valuesbyvariablescanautomaticallyabstractinfiniteexecutionsequences.Forinstance,considerauserwriteactiontoanarbitraryfileinthesystemmodelinSection2.Thisdoesnotconstitute“progress”sinceitdoesnotenableanystatechangethatwasimpossiblebefore.Thelackofprogressiseasilycapturedbytermcon-straints.Inthestatebeforeawriteoperationtoanarbitraryfile,thefile’scontentisrepresentedbyavariable,say.Instateafterthewriteoperation,thefile’scontentischangedto,whichissimplyavariant(i.e.,identicalmodulovariablerenaming)oftheoriginalcontent.Iftheeffectofwriteoperationisknown(say,thenewcontentis),thenthenewstateisaninstanceof(i.e.,issubsumedby)theoldstate:hence,nonewtransitionsarepossible.Thusweseethatprogresscanbeseenaschangemodulotermsubsumption.

Theabovescenarioassumedthatnothingisknownabouttheinitialstateofthesystem:thefiles,theircontents,therelevantpermissions,etc.Whenthesystem’sinitialstateis(atleastpar-tially)known,auser’swriteactionchangesthesystemstate;forinstance,theconstraintthat/etc/utmphasnoreferenceto/etc/passwdmaynolongerbetrueafteranarbitrarywriteactionisdone,iftheaccesspermissionsof/etc/utmpallowthewriteactiontosucceed.Thus,thestateofthesystemafteranarbitrarywriteactionisdifferentfromtheinitialstateofthesys-tem.Themodelcheckerwillexplorethesystemevaluationfromthisstate,andcanagainconcludethatthereisapotentialvulnerabilityaslongas/etc/utmpcanbemodifiedbyanarbitraryuser.Variableabstractionaloneisinsufficientingeneral,andweemployapproximationsthatloseinformationbyeitherignoringstatechanges(thuspruningexecutionsequences),orignoringcon-ditionsonstatechanges(thusrepeatingexecutionsequences).Notethatsuchanabstractionmaybe“incomplete”inthesensethatvulnerabilitiesintheoriginalmodelmaynotbepresentintheabstractmodel.However,thislimitationisreasonableinourcaseifweassumethatthesystemvulnerabilitieswillbeexploitedbyhumanattackersusingtheirintuitionandexpertisetocomeupwithattackscenarios.Thisimpliesthatthesequenceofactionsthattheywouldperformtoachieveintrusionwilltypicallybeashortsequence,andthusitmaybeacceptabletomissoutvulnerabil-itiesthatrequirelongsequencesofactions.Basedonthisassumption,ourmethodusesasearchprocedurewithiterativedeepening,stoppingthesearchafterapredetermineddepth.ThesearchprocedureusestheprogrammingandtablingcapabilitiesofXSB.

3.2GeneratingCounter-Examples

Thecounter-exampletracesproducedbyamodelcheckercorresponddirectlytoattackscenarios.Hencethesetofallcounter-examplescanbeusedtodriveintrusiondetection.Notethat,eveninthefinite-statecase,itisinfeasibletoenumerateallpossiblecounter-examples.Toovercomethisproblem,weavoidanexplicitenumerationofallcounterexamples,insteadchoosingtorepresentthemusingafinite-stateautomaton.Theautomatonrepresentsthesetofcounter-examples,suchthateachexamplecorrespondstoapathintheautomaton.Theautomatarepresentationissuccinctandcanbeuseddirectlyforintrusiondetection.Moreover,suchanautomatoncanbeconstructedbyinspectingthememotablesbuiltduringmodelchecking:thetableentriesformthestatesoftheautomatonandthedependenciesbetweentheentriesformthetransitions.

Theautomata-basedrepresentationofcounter-examplesextendsnaturallytothecaseofinfinite-statesystemsaswell.Inthiscase,eachstateintheautomatonisassociatedwithasetofvariables,whilethetransitionsspecifyconditionsontheirvalues.Suchautomatahavetheabilitytorepresentgenericcounter-examples:thosethatareparameterizedwithrespecttospecificsystemconfigura-tions.Wecangeneratesuchcounter-examplesbyleavingtheinitialstateofthesystemunboundandusingdatanondeterminismtolazilybindingthestatevariables,asexplainedearlierwiththe

comsatexample.Theautomatarepresentingthesegenericexamplescanthenbeinstantiatedfor

particularsystemconfigurationparameterstocheckforvulnerabilities.Thustheautomatathem-selvesaregenericwithrespecttoconfigurations.However,theautomatamustberegeneratedwhensystem’scapabilitieschange,e.g.,whennewservicesareadded.

Notethatingeneral,forinfinite-statesystems,theremaybenofiniterepresentationforthesetofallcounter-examples.However,notethattheabstractionsweuseboundthelengthofcounterexamplesequences,therebymakingitpossibletofindafiniterepresentationforthesetofallcounterexamples.

3.3BeyondInvariantProperties

Inthecomsatexampleexplainedearlier,thepropertyofinterestwasaninvariant.Ingeneral,however,onewouldbeinterestedinpathproperties.Forinstance,theremaybeapasswordchang-ingprogrampasswdonasystemthatallowsausertomodifyhis/herpassword,andthuschangethecontentsofthepasswordfile.Clearly,executionpathswherethepasswordfileischangedbythepasswdprogram,orbyasystemadministrator,donotcorrespondtoanyvulnerabilities.

Pathpropertiescanbeencodedintemporallogic[14].Theycaneliminate“degeneratepaths”suchasthosewherethesuperuserchangesthepasswordfileoritischangedbythepasswdpro-gram.Thisisdonebyaddingantecedentstotheoriginalsafetypropertythatareviolatedbysuchdegeneratepaths.

Aproblemthatarisesinthecontextofvulnerabilityanalysisisthatthedescriptionofdegen-eratepathstendstobecomeverylarge,sincetherearemanydegeneratecases.Forinstance,theremaybemanydifferentwaysinwhichasuperusercanchangethepasswordfile:byoverwritingit,byusinganeditor,byusingthepasswdcommand,etc.Enumeratingallsuchdegeneratepathsisimpracticalsincethetemporallogicformulabecomesverylargeanddifficulttounderstand,andhenceislikelytocontainerrors.

Toaddressthisproblem,weproposethefollowingapproachwheretheoriginalsafetypropertyisleftunchanged.Inordertoeliminatedegeneratepaths,wedevelopasecondmodelcalledtheintentionsmodel.Anintentionsmodelcapturestheintendedoutcomeofexecutingeveryprogram.Theseintentionsarestatedintermsofthefilesthatmaybewrittenorexecutedinthecourseofexecutingtheprogram.Thesystemmodelhasvulnerabilitiesifitcontainspathstounsafestatesforwhichthereexistsnocorrespondingpathintheintentionsmodel.

Forexample,anintentionmodelofmaildaemonwouldbethatitwritesfilesinthedirectory/usr/spool/mail.Theintentionmodeloflprwouldbethatitwritesfilesinthedirectory/usr/spool/lp.Theintentionmodelofpasswdprogramwouldbethatitwrites/etc/passwdfile.Theintentionmodel,bydefault,willrefertonormalizedfilenames,whichcorrespondtoanabsolutefilenamesthatarenotasymboliclinks.Thiswouldbeappropriateinthecaseofmaildaemonandlpr.Situationswheresymboliclinksarepermitted,willbemadeexplicitintheintentionsmodel.Forinstance,anintentionmodelofcpprogramwillstatethatitwilloverwriteafileprovidedasanargument,regardlessofwhetheritisasymboliclinkornot.

Whenanintentionsmodelisused,themodelcheckermustdisregardthe“intendedpaths,”i.e.,pathswhereeveryactionisalsointheintentionsmodel.Asimplewaytodothisistoleavethemodelcheckerunchanged,butpruneawaypathsfromthecounter-exampleautomaton.Clearly,

moreefficienttechniquestoeliminateintendedpathscanbedeveloped,andisatopicofcurrentresearch.

4AnalysisResults

Ourcurrentimplementationfindsvulnerabilitiesexpressedasviolationsofinvariantproperties.Whenreportingtheviolations,wedistinguishbetweenthevalueofinitialsystemconfigurationparametersandthesequenceofeventsthatleadstotheviolation.Wepresenttheresultsintheformat

whenscenario

whereconditionspecifiestheconfigurationparametersandexploitisthepaththatleadstotheviolation.

4.1Vulnerabilitiesduetocomsat

GiventhesimplemodelofaUNIXsystemdescribedinSection2,ourcurrentimplementationiden-tifiesthefollowingvulnerabilitiesthatwouldultimatelyenablethepasswordfiletobeoverwritten.

Thesevulnerabilitieswerefoundusingaquerytocheckforreachabilityof_.write([etc,passwd],_):astatewhereanarbitraryprocesswritesto/etc/passwd.

Thefirstvulnerabilityidentifiedisatrivialone:itcorrespondstothecasewhenthepasswordfileisworld-writable.Eventhoughthisanobviousvulnerability,itisneverthelessaninterestingdiscovery,giventhatthemodeldoesnotevenmentionthefile/etc/passwd.Theuseofdata-nondeterminisminourmodels,anditsimplementationusingterm-constraints,enablesustoderivethisscenario.

whenFS.resolve([etc,passwd],U1,G1,write,F1)scenario

[user(U1,G1,FS,UG).write([etc,passwd],M)]

Thewaytoreadthisisasfollows:ifthereexistsafile/etc/passwdthatiswritablebysomeuserU1belongingtoagroupG1,thenthisusercanwritethepasswordfilewitharbitrarydataM.Thesecondvulnerabilityidentifiedisthecomsatvulnerabilitydescribedintheintroduction.IthappenswhenauserU1haspermissiontowritethe/etc/utmpfile.Noteagainthatthisvulnera-bilitywasidentified,evenwhenthemodelcheckerwasprovidednoinformationabouttheoriginalstateofthesystem.Byvirtueofthewaytermconstraintsarehandledinourmodel-checker,itisabletoinfertheappropriaterelationshipsthatmustholdbetweenthecontentsofthe/etc/utmpfileandthepasswordfile,aswellasthefilepermissionsthatmustholdforthevulnerabilitytobeexploited.

when

FS.resolve([etc,utmp],U1,G1,write,F1)

scenario

[user(U1,G1,FS,UG).write([etc,utmp],(U2,[etc,passwd])),user(U3,G3,FS,UG)invokesmailer.send(U2,M),mailer.write([var,spool,mail,U2],M),comsat.read([var,spool,mail,U2],M),

comsat.readRec([etc,utmp],U2,[etc,passwd]),comsat.write([etc,passwd],M)]

Thescenariocanbereadasfollows:inthefirststep,userU1writesthefile/etc/utmpwiththerecord(U2,/etc/passwd).Inthenextstep,userU3invokesthemailerprogramtosendamessageMtouserU2.ThiscausesthemailertowritethemessageMintothespoolfile/var/spool/mail/U2.Inthefourthstep,thecomsatprogramreadsthisspoolfile.Inthefifthstep,comsatreadstherecordfrom/etc/utmpthatindicatesthatU2isloggedinontheterminal/etc/passwd(thisrecordhavingbeenwritteninthefirststepofthescenario),andthenoverwrites/etc/passwdwiththemailmessageM.NotethatalthoughthescenariomentionsthreeusersU1,U2andU3,allthreeareexistentiallyquantifiedvariables—whichmeansthattheycanallbethesameuser.

Thethirdvulnerabilityissimilartothesecondone,buttheuserdirectlyoverwritesthespoolfileinsteadofusingthemailertoupdatethespoolfile.Inordertodothis,thisusermusthavewritepermissiontothespoolfile,andthisextraconditioniscapturedinthecondition:

when

FS.resolve([etc,utmp],U1,G1,write),

FS.resolve([var,spool,mail,U2],U3,G3,write)scenario

[user(U1,G1,ug).write([etc,utmp],(U2,[etc,passwd])),user(U3,G3,ug).write([var,spool,mail,U2],M),comsat.read([var,spool,mail,U2],M),

comsat.readrec([etc,utmp],U2,[etc,passwd]),comsat.write([etc,passwd],M)]

Anotherattackscenarioisaninterestingvariationonthepreviousattack,anddoesnotrequirewritepermissionto/etc/utmp.Itbringstogethertwoknownexploits,oneinvolvingtheuseofsymboliclinksandtheotherbeingthecomsatvulnerabilitymentionedabove.Althoughwehaddevelopedthemodelsourselves,wehadnotrealizedthatourmodelcontainedthisvulnerability.Itisnoteworthythatinspiteofthesimplicityofthemodelsused,ourmodelcheckingprocedureidentifiedvulnerabilitiesthatwereunknowntous.

when

FS.resolve([var,spool,mail,U2],U1,G1,write,F1)scenario

[user(U1,G1,FS,UG).symlink([var,spool,mail,U2],[etc,utmp]),user(U3,G3,FS,UG)invokesmailer.send(U2,(U4,[etc,passwd])),mailer.write([var,spool,mail,U2],(U4,[etc,passwd])),user(U5,G5,FS,UG)invokesmailer.send(U4,M),

mailer.write([var,spool,mail,U4],M),comsat.read([var,spool,mail,U4],M),

comsat.readrec([etc,utmp],U4,[etc,passwd]),comsat.write([etc,passwd],M)]

Inthisscenario,anuserU1firstsymbolicallylinksthespoolfile/var/spool/mail/U2to/etc/utmp.Inthesecondstep,userU3invokesthemailertosendamessagetotheuserU2.Themessagebodyconsistsofthesinglerecord(U4,[etc,passwd]).Inthethirdstep,themailerwritesthisrecordontothespoolfile/var/spool/mail/U2.Sincethisspoolfilehadbeenlinkedtothe/etc/utmpfileinthefirststep,therecordisactuallywrittentothe/etc/utmpfile.NotethatthisstephappensbecausethemailerblindlyoverwritesthespoolfilecorrespondingtotheuserU2withoutchecking(a)whetheranyuser(inparticularU2)haswritepermissionforthatfile,and(b)whetheritisasymboliclink.Therestofthestepsintheexploitareidenticaltothoseofthepreviousvulnerability.

4.2Vulnerabilitiesduetolpr

Beforeanalysis,weabstractedthesystemmodelforlprbymakingthetemporaryspoolfilenametobeaconstant(i.e.,makingthecountingmodulo1insteadof1000).Thecombinationofsymboliclinksandthestandardspoolfilenamingconventionintroducesthefollowingvulnerability:

when

FS.resolve(F1,U1,G1,write,F2),

FS.resolve([etc,passwd],U2,G2,read,F3),FS.resolve(F1,U3,G3,read,F4),FS.resolve(F5,U3,G3,exec,F6),FS.getContent(F6,program(lpr))scenario

[user(U1,G1,FS,UG).write(F1,C1),

user(U2,G2,FS,UG).run(lpr,[[etc,passwd],s]),user(U3,G3,UG).run(lpr,[F1])]

Sincewestartwithaninitialstatethatcorrespondstoanunboundvariable,therearenofilesthatcanbeprintedintheinitialstate.Thescenarioshowsthatsuchafilecanbecreated,andlaterread.Italsorequiresreadpermissiononthepasswordfile.

5ConcludingRemarks

Inthispaper,wepresentedanewmodel-basedapproachforanalyzingconfigurationvulnerabili-ties.Whereaspreviousapproachesreliedonexpertknowledgetocodifycausesofconfigurationvulnerabilities,thisstepisnotnecessaryinourapproach.Consequently,ourapproachcannotonlyidentifypreviouslyexploitedvulnerabilities,butalsodiscovernewonesthathaveneverbeenexploited.Ourexamplesdemonstratethecapabilitytodiscoversuchvulnerabilities:knowledge

aboutvulnerabilitieswasneverencodedintothesystemmodel,butouranalysiswasabletode-tectthevulnerabilities.Itevenidentifiedvulnerabilitieswhosepresenceinthesystemmodelwereunknowntous.

Theresultsofouranalysiscanbeusedinmanyways.Thefirstandobvioususeisinre-configuringthesystemtoeliminatethevulnerabilitiesidentifiedbymodel-basedanalysis.Thereconfiguredsystemcanbereanalyzedtoensurethat(most)vulnerabilitieshavebeeneliminated.Aseconduseistofeedthecounter-examplesgeneratedbyouranalysisintoanintrusiondetectionsystem.Theintrusiondetectionsystemcannowidentifyallattemptstoexploitthevulnerabili-tiesidentifiedbyouranalysis,andmaybeabletopreventthemfromsucceeding.Athirdwaytouseouranalysisistobeginwithminimalinformationabouttheinitialstateofthesystem,inwhichcaseouranalysisgeneratesassumptionsabouttheinitialsystemthatleadtovulnerabilities.Theseassumptionscorrespondtothe“vulnerabilitycauses”thatcanbeencodedintoconfigurationcheckerssuchasCOPSandSATAN.

Themainchallengeinusingtheapproachpresentedinthispaperisoneofscale.Althoughourmodelcheckercaneasilyhandlethemodelsdescribedinthispaper,morerealisticsystemmodelswillbemuchlarger,makingitsignificantlyhardertoperformanaccurateanalysis.However,webelievethisisatemporarydifficulty:someoftheauthorsofthispaper,aswellasanumberofotherresearchers,aredevelopingbetterandbettermodelcheckersthatareabletohandlelargerandlargersystems.Asecondchallengeistheeffortrequiredfordevelopingmodels.Weareinvestigatingsourcecodeanalysistechniquesthatcanhelpautomatethemodelgenerationprocess.

References

[1]T.Aslam,I.KrsulandE.Spafford,ATaxonomyofSecurityFaults,ProceedingsoftheNa-tionalComputerSecurityConference,1996.[2]R.Baldwin,Rulebasedanalysisofsecuritychecking.MITLCSTechnicalReportNo.401,

1988.[3]M.Bishop,M.Dilger,CheckingforRaceConditionsinFileAccess.ComputingSystems

9(2),1996,pp.131-152.[4]M.BishopandB.Bailey,Acriticalanalysisofvulnerabilitytaxonomies,TRCSE-96-11,

Dept.ofComp.Sci.,UniversityofCaliforniaatDavis,1996.[5]W.ChenandD.S.Warren,Tabledevaluationwithdelayingforgenerallogicprograms,Jour-naloftheACM,43(1):20–74,January1996.[6]E.M.ClarkeandE.A.Emerson,Designandsynthesisofsynchronizationskeletonsusing

branching-timetemporallogic,ProceedingsoftheWorkshoponLogicofPrograms,LNCS131,1981.[7]E.M.Clarke,E.A.Emerson,andA.P.Sistla,Automaticverificationoffinite-stateconcurrent

systemsusingtemporallogicspecifications,ACMTOPLAS,8(2),1986.

[8]E.M.Clarke,K.McMillan,S.Campos,andV.Hartonas-GarmHausen,Symbolicmodel

checking,ComputerAidedVerification’96,pages419–422.[9]E.M.ClarkeandJ.M.Wing,Formalmethods:Stateoftheartandfuturedirections,ACM

ComputingSurveys,28(4),December1996.[10]Y.DongandC.R.Ramakrishnan,AnOptimizingCompilerforEfficientModelChecking,

ProceedingsofFORTE/PSTV,1999.[11]D.FarmerandE.Spafford,TheCOPSSecurityCheckerSystem,CSD-TR-993,Department

ofComputerScience,PurdueUniversity,1991.[12]C.A.R.Hoare,CommunicatingSequentialProcesses,Prentice-Hall,1985.

[13]G.J.Holzmann,ThemodelcheckerSPIN,IEEETransactionsonSoftwareEngineering,

23(5):279–295,May1997.[14]Z.MannaandA.Pnueli,TheTemporalLogicofReactiveandConcurrentSystems:Specifi-cation,Springer-Verlag,1991.[15]R.Milner,CommunicationandConcurrency,PrenticeHall,1989.

[16]J.P.QueilleandJ.Sifakis.SpecificationandverificationofconcurrentsystemsinCesar.In

ProceedingsoftheInternationalSymposiuminProgramming,volume137ofLNCS,1982.Springer-Verlag.[17]C.R.RamakrishnanandR.Sekar,Model-BasedVulnerabilityAnalysisofComputerSystems,

2ndInt’lWorkshoponVerification,ModelCheckingandAbstractInterpretation,1998.[18]C.R.Ramakrishnan,I.V.Ramakrishnan,S.A.Smolka,Y.Dong,X.Du,A.Roychoudhuryand

V.N.Venkatakrishnan,XMC:ALogic-Programming-BasedVerificationToolset,ComputerAidedVerification(CAV),2000.[19]Y.S.Ramakrishna,C.R.Ramakrishnan,I.V.Ramakrishnan,TerranceSwift,S.A.Smolka,and

D.S.Warren,Efficientmodel-checkingusingtabledresolution,ProceedingsofCAV’97,June1997.[20]R.RitcheyandP.Ammann,UsingModelCheckingtoAnalyzeNetworkVulnerabilities,

IEEEOaklandSymposiumonSecurityandPrivacy,2000.[21]H.TamakiandT.Sato,OLDTresolutionwithtabulation,InternationalConferenceonLogic

Programming,pages84–98.MITPress,1986.[22]TheXSBlogicprogrammingsystemv2.1,

http://www.cs.sunysb.edu/sbprolog.

2000.Availablefrom

[23]D.Zerkle,K.Levitt,NetKuang–AMulti-HostConfigurationVulnerabilityChecker,Proc.of

the6thUSENIXSecuritySymposium.SanJose,California,July22-25,1996,pp.195-204.