alarmsesetnod32id

LTLModel-CheckingforMalwareDetectionFuSongandTayssirTouiliLIAFA,CNRSandUniv.
ParisDiderot,France{song,touili}@liafa.
univ-paris-diderot.
frAbstract.
Nowadays,malwarehasbecomeacriticalsecuritythreat.
Traditionalanti-virusessuchassignature-basedtechniquesandcodeemulationbecomein-sufcientandeasytogetaround.
Thus,itisimportanttohaveefcientandro-bustmalwaredetectors.
In[20,19],CTLmodel-checkingforPushDownSystems(PDSs)wasshowntobearobusttechniqueformalwaredetection.
However,theapproachof[20,19]lacksprecisionandrunsoutofmemoryinseveralcases.
Inthiswork,weshowthatseveralmalwarespecicationscouldbeexpressedinamoreprecisemannerusingLTLinsteadofCTL.
Moreover,LTLcanexpressmaliciousbehaviorsthatcannotbeexpressedinCTL.
Thus,sinceLTLmodel-checkingforPDSsispolynomialinthesizeofPDSswhileCTLmodel-checkingforPDSsisexponential,weproposetouseLTLmodel-checkingforPDSsformalwaredetection.
Ourapproachconsistsof:(1)ModelingthebinaryprogramasaPDS.
Thisallowstotracktheprogram'sstack(neededformalwaredetec-tion).
(2)Introducinganewlogic(SLTPL)tospecifythemaliciousbehaviors.
SLTPLisanextensionofLTLwithvariables,quantiers,andpredicatesoverthestack.
(3)ReducingthemalwaredetectionproblemtoSLTPLmodel-checkingforPDSs.
WereducethismodelcheckingproblemtotheemptinessproblemofSymbolicB¨uchiPDSs.
Weimplementedourtechniquesinatool,andweappliedittodetectseveralviruses.
Ourresultsareencouraging.
1IntroductionOverthepastdecades,thelandscapeofmalware'sintenthaschanged.
Moreandmoresophisticatedmalwareshavebeendesignedformoregeneralcyber-espionagepurposes.
Forexample,Stuxnet,DuquandFlamearedeployedfortargetedattacksincountries,suchasIran,Israel,Sudan.
Traditionalantivirustechniques:codeemulationandsigna-ture(pattern)-basedtechniquesbecomeinsufcient.
Indeed,codeemulationtechniquesmonitoringonlyseveraltracesofprogramsinalimitedtimespanmaymisssomema-liciousbehaviors,andsignature-basedtechniquesusingpatternsofprograms'codestocharacterizemalwarecanonlydetectknownmalwares.
Addressingtheselimitations,manyeffortshavebeenmade[1,4,5,17,7,8,13,2].
Amongthem,model-checkingisoneoftheefcienttechniquesformalwaredetection[4,17,7,8,13],asitallowstocheckthebehavior(notthesyntax)oftheprogramwith-outexecutingit.
However,[4,17,7,8,13]usenitestategraphs(automata)asprogrammodelthatcannotaccuratelyrepresenttheprogram'sstack.
Beingabletotrackthepro-gram'sstackisveryimportantformalwaredetectionasexplainedin[16].
Forexample,WorkpartiallyfundedbyANRgrantANR-08-SEGI-006.
N.
PitermanandS.
Smolka(Eds.
):TACAS2013,LNCS7795,pp.
416–431,2013.
cSpringer-VerlagBerlinHeidelberg2013LTLModel-CheckingforMalwareDetection417malwarewritersobfuscatethesystemcallsbyusingpushesandjumpstomakemalwarehardtoanalyze,becauseanti-virusesusuallydeterminemalwarebycheckingfunctioncallstooperatingsystems.
Toovercomethisproblem,weproposedanewapproachformalwaredetectionin[20,19]thatconsistsof(1)ModelingtheprogramusingaPushdownSystem(PDS).
Thisallowsustotrackthebehaviorofthestack.
(2)Introducinganewlogic,calledSCTPL,tospecifymaliciousbehaviors.
SCTPLcanbeseenasanextensionofthebranching-timetemporallogicCTLwithvariables,quantiers,andregularpredicatesoverthestack.
Extensionwithvariablesandquantiersallowstoexpressmaliciousbehaviorsinamoresuccinctwayandregularpredicatesallowtospecifypropertiesonthestackcontentwhichisimportantformalwaredetection.
(3)Andreducingthemalwaredetectionproblemtothemodel-checkingproblemofPDSsagainstSCTPLformulas.
Ourtechniqueswereimplementedandappliedtodetectseveralviruses.
However,usingthetechniquesof[20,19],theanalysisofseveralmalwaresrunsoutofmemoryduetothecomplexityofSCTPLmodel-checkingforPDSs.
Bylookingcare-fullyattheSCTPLformulasspecifyingthemaliciousbehaviors,wefoundthatmostoftheseSCTPLformulascanbeexpressedinamoreprecisemannerusingtheLinearTemporalLogic(LTL).
SinceLTLcanexpresssomemaliciousbehaviorsthatcannotbeexpressedbySCTPL,andsincethecomplexityofLTLmodel-checkingforPDSsispolynomialinthesizeofPDSs,whereasthecomplexityofCTLmodel-checkingforPDSsisexponential,wewillapplyinthisworkLTLmodel-checkingformalwaredetection(insteadofapplyingSCTPLmodel-checkingaswedidin[20,19],sincethistechniquelacksprecisionandrunsoutofmemoryinseveralcases.
).
ToobtainsuccinctLTLformulasthatexpressmaliciousbehaviors,wefollowtheideaof[20,19]andin-troducetheSLTPLlogic,anextensionofLTLwithvariables,quantiersandregularpredicatesoverthestackcontent.
SLTPLisasexpressiveasLTLwithregularvalua-tions[9,14],butitallowstoexpressmaliciousbehaviorsinamoresuccinctway.
WeshowthatSLTPLmodel-checkingforPDSsispolynomialinthesizeofPDSsandwereducethemalwaredetectionproblemtoSLTPLmodel-checkingforPDSs.
Weusetheapproachof[19]tomodelaprogramasaPDS,inwhichthePDScontrollocationscorrespondtotheprogram'scontrolpoints,andthePDS'sstackmimicstheprogram'sexecutionstack.
Thisapproachallowstotracktheprogram'sstack.
InSLTPL,propositionscanbepredicatesoftheformp(x1,xn),wherethexi'sarefreevariablesorconstants.
Freevariablescangettheirvaluesfromanitedomain.
Variablescanbeuniversallyorexistentiallyquantied.
SLTPLwithoutpredicatesoverthestackcontent(calledLTPL)isasexpressiveasLTL,butitallowstoexpressmali-ciousbehaviorsinamoresuccinctway.
Forexample,considerthestatement"Thereisaregisterassignedby0,andthen,thecontentofthisregisterispushedontothestack.
"ThisstatementcanbeexpressedinLTLasalargeformulaenumeratingallthepossibleregistersasfollows:mov(eax,0)∧Xpush(eax)∨mov(ebx,0)∧Xpush(ebx)∨mov(ecx,0)∧Xpush(ecx)∨.
.
.
whereeveryinstructionisregardedasapredicate,e.
g.
,mov(eax,0)isapredicate.
How-ever,thisLTLformulaislargeforsuchasimplestatement.
UsingLTPL,thiscanbeexpressedbyrmov(r,0)∧Xpush(r)whichexpressesinasuccinctwaythatthereexistsaregisterrs.
t.
theaboveholds.
418F.
SongandT.
TouiliHowever,LTPLcannotspecifypropertiesaboutthestack,whichisimportantwith0andanaddressaasparameters1.
Aftercallingformalwaredetectionasexplainedpreviously.
Forexample,considerFig.
1(a).
ItcorrespondstoacriticalfragmentoftheTrojanLdPinchthataddsitselfintotheregistrykeylistingtogetstartedatboottime.
Todothis,itcallstheAPIfunctionGetModuleFileNameAthisfunction,thelenameofitsownexecutablewillbestoredintheaddressa.
Then,theAPIfunctionRegSetValueExAiscalledwithaasparameter(i.
e.
,itsownlename).
Thisaddsitslenameintotheregistrykeylisting.
WecannotspecifythismaliciousbehaviorinaprecisemannerusingLTPL.
Indeed,aviruswritercaneasilyusesomeobfuscationtechniquesinordertoescapefromanyLTPLspecication.
E.
g.
,letusintroduceonepushfollowedbyonepopafterpush0atlinel2asdoneinFig.
1(b).
ThisfragmenthasthesamemaliciousbehaviorthanthefragmentinFig.
1(a).
Sincel1:pushal2:push0l3:callGetModuleFileNameAl4:pushal5:callRegSetValueExA(a)(b)l1:pushal2:push0l3:pusheaxl4:popeaxl5:callGetModuleFileNameAl6:pushal7:callRegSetValueExAFig.
1.
(a)AfragmentoftheTro-janLdPinchand(b)Theobfus-catedversionthenumberofpushesandpopscanbearbitrary,itisalwayspossibleforviruswriterstochangetheircodeinordertoescapefromagivenLTPLformula.
Toovercomethisproblem,weintroduceSLTPL,whichisextensionofLTPLwithregularpredicatesoverthestack.
SuchpredicatesaregivenbyRegularVariableExpressionsoverthestackalphabetandsomefreevariables(whichcanalsobeexistentiallyanduniversallyquan-tied).
SLTPLisasexpressiveasLTLwithregularvaluations[9],butmoresuccinct.
Inthissetting,themaliciousbehaviorofFig.
1(a)and(b)canbespeciedasfollows:Facall(GetModuleFileNameA)∧0aΓ∧Fcall(RegSetValueExA)∧aΓ,where0aΓ(resp.
aΓ)isapredicateexpressingthatthetopofthestackare0anda(resp.
a).
TheSLTPLformulastatesthatthereexistsapathinwhichGetModuleFileNameAiscalledwith0andsomeaddressaasparameters(i.
e.
,0andaareonthetopofthestack),laterRegSetValueExAiscalledwithaasparameter.
ThisspecicationcandetectbothfragmentsinFig.
1(a)and(b),becauseitallowstospecifythecontentofthestackwhenGetModuleFileNameAiscalled.
NotethatitisimportanttousePDSsasamodelinordertohavespecicationswithpredicatesoverthestack.
Thus,wereducethemalwaredetectionproblemtotheSLTPLmodelcheckingprob-lemforPDSs.
Tosolvethisproblem,werstpresentareductionfromLTPLmodel-checkingforPDSstotheemptinessproblemofSymbolicB¨uchiPDSs(SBPDS).
Thislatterproblemcanbeefcientlysolvedby[10].
Then,weconsidertheSLTPLmodelcheckingproblemforPDSs.
WeintroduceExtendedFiniteAutomata(EFA)torepre-sentregularpredicates.
ToperformSLTPLmodel-checking,werstconstructaSym-bolicPDSwhichisakindofsynchronizationofthePDSandtheEFAsthatallowstodeterminewhetherthestackpredicatesholdatagivenstepbylookingonlyatthetop1Parameterstoafunctioninassemblyarepassedbypushingthemontothestackbeforeacalltothefunctionismade.
Thecodeinthecalledfunctionlaterretrievestheseparametersfromthestack.
LTLModel-CheckingforMalwareDetection419ofthestackofthesymbolicPDS.
ThisallowsustoreducetheSLTPLmodel-checkingproblemforPDSstotheemptinessproblemofSBPDSs.
Weimplementedourtechniquesinatoolandappliedittodetectmalwares.
Ourtoolcandetectallthemalwaresthatweconsidered.
TheexperimentalresultsshowthatdetectingmalwareusingSLTPLmodel-checkingperformsbetterthanusingSCTPLmodel-checking[20,19]andLTLmodel-checkingforPDSswithregularvaluations[9].
Moreover,theanalysisofseveralexamplesterminatedusingSLTPLmodel-checking,whileitrunsoutofmemory/timeusingSCTPLorLTLwithregularvaluationsmodel-checking.
Moreover,somemaliciousbehaviorsasexpressedin[20,19]producesomefalsealarms.
UsingSLTPL,thesefalsealarmsareavoided.
OurtoolcanalsodetectthenotoriousmalwareFlamethatwasundetectedformorethanveyears.
RelatedWork:QuantiedLinearTemporalLogic(QLTL)[18]isclosetoLTPL.
How-ever,QLTLdisallowstoquantifyoveratomicpropositions'parameters.
LTPLisasub-classoftheFirst-orderLinearTemporalLogic(FO-LTL)[12].
[12]doesnotconsiderthemodel-checkingproblem.
LMDG[22]andLMDG[21]aresub-logicsofFO-LTL.
However,LMDGdisallowstemporaloperatornestingandpropertiesbeyonditstem-plates,andLMDGcannotuseexistentialanduniversaloperators.
FO-LTLwasusedformalwaredetectionin[3].
Alltheseworkscannotspecifypredicatesoverthestack.
Model-checkingandstaticanalysissuchas[4,17,7,8,13,1,2]havebeenappliedtode-tectmaliciousbehaviors.
However,alltheseworksarebasedonmodelingtheprogramasanite-statesystem,andthus,theymissthebehaviorofthestack.
Asexplainedintheintroduction,beingabletotrackthestackisimportantformanymaliciousbehaviors.
[16]keepstrackofthestackbycomputinganabstractstackgraphwhichnitelyrep-resentstheinnitesetofallthepossiblestacksforeverycontrolpointoftheprogram.
Theirtechniquecandetectsomemaliciousbehaviorsthatchangethestack.
However,theycannotspecifytheothermaliciousbehaviorsthatSLTPLcandescribe.
[15]per-formscontext-sensitiveanalysisofcallandretobfuscatedbinaries.
Theyuseabstractinterpretationtocomputeanabstractionofthestack.
Webelievethatourtechniquesaremoreprecisesincewedonotabstractthestack.
Moreover,thetechniquesof[15]wereonlytriedontoyexamples,theyhavenotbeenappliedformalwaredetection.
CTPL[13]isanextensionofCTLwithvariablesandquantiers.
SCTPL[20,19]isanextensionofCTPLwithpredicatesoverthestackcontent.
CTL,CTPLandSCTPLareincomparablewithLTPLorSLTPL.
Formalwaredetection,experimentalresultsshowthatSLTPLmodel-checkingperformsbetterandismoreprecise.
Outline.
Sections2and3givethedenitionofPDSsandLTPL/SLTPL,respectively.
LTPL/SLTPLmodel-checkingforPDSsaregiveninSections4and5,respectively.
ExperimentsareshowninSection6.
2BinaryCodeModelingInthissection,werecallthedenitionofpushdownsystems.
Weusethetranslationof[19]tomodelbinaryprogramsaspushdownsystems.
APushdownSystem(PDS)isatupleP=(P,Γ,Δ),wherePisanitesetofcontrollocations,Γisthestackalphabet,andΔ(P*Γ)*(P*Γ)isanitesetoftransition420F.
SongandT.
Touilirules.
AcongurationofPisp,ω,wherep∈Pandω∈Γ.
If((p,γ),(q,ω))∈Δ,wewritep,γ→q,ωinstead.
ThesuccessorrelationP(P*Γ)*(P*Γ)isdenedasfollows:foreveryω∈Γ,p,γωPq,ωωifp,γ→q,ω.
Foreverycongurationc,c∈P*Γ,cisanimmediatesuccessorofciffcPc.
AnexecutionofPisasequenceofcongurationsπ=c0c1.
.
.
s.
t.
ciPci+1foreveryi≥0.
Letπ(i)denoteciandπidenotethesufxofπstartingfromπ(i).
Fortechnicalreasons,w.
l.
o.
g.
,weassumethatforeverytransitionrulep,γ→q,ω,|ω|≤2(see[10]).
3MaliciousBehaviorSpecicationWedenetheStackLinearTemporalPredicateLogic(SLTPL)asanextensionoftheLinearTemporalLogic(LTL)withvariablesandregularpredicatesoverthestackcon-tent.
Variablesareparametersofatomicpredicatesandcanbequantiedbytheexis-tentialanduniversaloperators.
RegularpredicatesarerepresentedbyregularvariableexpressionsandareusedtospecifythestackcontentofthePDS.
3.
1Environments,PredicatesandRegularVariableExpressionsFromnowon,wexthefollowingnotations.
LetX={x1,x2,.
.
.
}beanitesetofvariablesrangingoveranitedomainD.
LetB:X∪D→Dbeanenvironmentthatassignsavaluec∈Dtoeachvariablex∈Xs.
t.
B(c)=cforeveryc∈D.
B[x←c]denotestheenvironments.
t.
B[x←c](x)=candB[x←c](y)=B(y)foreveryyx.
LetBbethesetofalltheenvironments.
LetΘid={(B1,B2)∈B*B|B1=B2}betheidentityrelationforenvironments,andforeveryx∈X,Θx={(B1,B2)∈B*B|x∈Xs.
t.
xx,B1(x)=B2(x)}betherelationthatabstractsawaythevalueofx.
LetAP={a,b,c,.
.
.
}beanitesetofatomicpropositions,APXbeanitesetofatomicpredicatesoftheformb(α1,.
.
.
,αm)s.
t.
b∈AP,αi∈X∪Dforeveryi,1≤i≤m,andAPDbeanitesetofatomicpredicatesoftheformb(α1,.
.
.
,αm)s.
t.
b∈APandαi∈Dforeveryi,1≤i≤m.
LetP=(P,Γ,Δ)beaPDS,anitesetRofRegularVariableExpressions(RVEs)eoverX∪Γisdenedby:e::=|a∈X∪Γ|e+e|e·e|e.
ThelanguageL(e)ofaRVEeisasubsetofP*Γ*Bdenedinductivelyasfollows:L(p,,B)|p∈P,B∈B};L(x),wherex∈Xistheset{(p,γ,B)|p∈P,γ∈Γ,B∈B:B(x)=γ};L(γ),whereγ∈Γistheset{(p,γ,B)|p∈P,B∈B};L(e1+e2)=L(e1)∪L(e2);L(e1·e2)={(p,ω1ω2,B)|(p,ω1,B)∈L(e1);(p,ω2,B)∈L(e2)};L(e)={(p,ω,B)|ω∈{u∈Γ|(p,u,B)∈L(e)}}.
3.
2TheStackLinearTemporalPredicateLogicASLTPLformulaisaLTLformulawherepredicatesandRVEsareusedasatomicpropositions,andwherequantiersovervariablesareused.
Fortechnicalreasons,wesupposew.
l.
o.
g.
thatformulasaregiveninpositivenormalform.
WeusethereleaseoperatorRasthedualoftheuntiloperatorU.
Formally,thesetofSLTPLformulasisgivenby(wherex∈X,e∈Randb(α1,.
.
.
,αm)∈APX):::=b(α1,.
.
.
,αm)|b(α1,.
.
.
,αm)|e|e|∧|∨|x|x|X|U|RLTLModel-CheckingforMalwareDetection421TheotherstandardoperatorsofLTLcanbeexpressedbytheaboveoperators:Fψ=trueUψandGψ=falseRψ.
ASLTPLformulaψisaLTPLformulaifftheformulaψdoesnotuseanyregularpredicatee∈R.
Avariablexisafreevariableofψifitisoutofthescopeofaquanticationinψ.
GivenaPDSP=(P,Γ,Δ),letλ:APD→2Pbealabelingfunctionthatassignsasetofcontrollocationstoeachpredicate.
Letc=p,ωbeacongurationofP.
PsatisesaSLTPLformulaψinc(denotedbyc|=λψ)iffthereexistsanenvironmentB∈Bs.
t.
csatisesψunderB(denotedbyc|=Bλψ).
c|=Bλψholdsiffthereexistsanexecutionπstartingfromcs.
t.
πsatisesψunderB(denotedbyπ|=Bλψ),whereπ|=Bλψisdenedbyinductionasfollows:π|=Bλb(α1,.
.
.
,αm)iffthecontrollocationpofπ(0)isinλb(B(α1),.
.
.
,B(αm));π|=Bλb(α1,.
.
.
,αm)iffπ|=Bλb(α1,.
.
.
,αm)doesnottrue;π|=Bλeiff(π(0),B)∈L(e);π|=Bλeiff(π(0),B)L(e);π|=Bλψ1∧ψ2iffπ|=Bλψ1andπ|=Bλψ2;π|=Bλψ1∨ψ2iffπ|=Bλψ1orπ|=Bλψ2;π|=Bλxψiffforeveryv∈D,π|=B[x←v]λψ;π|=Bλxψiffthereexistsv∈Ds.
t.
π|=B[x←v]λψ;π|=BλXψiffπ1|=Bλψ;π|=Bλψ1Uψ2iffthereexistsi≥0s.
t.
πi|=Bλψ2andj,0≤jGivenaSLTPLformulaψ,letcl(ψ)(resp.
cl(ψ)andclU(ψ))denotethesetof-formulas(resp.
-formulasandU-formulas)oftheformxφ(resp.
xφandφ1Uφ2)ofψ.
Letcl(ψ)betheclosureofψdenedasthesmallestsetofformulascontainingψandsatisfyingthefollowing:ifφ1∧φ2∈cl(ψ)orφ1∨φ2∈cl(ψ),thenφ1∈cl(ψ)andφ2∈cl(ψ);ifXφ1∈cl(ψ),orxφ1∈cl(ψ),orxφ1∈cl(ψ)orφ1∈cl(ψ),thenφ1∈cl(ψ);ifφ1Uφ2∈cl(ψ),thenφ1∈cl(ψ),φ2∈cl(ψ)andX(φ1Uφ2)∈cl(ψ);ifφ1Rφ2∈cl(ψ),thenφ1∈cl(ψ),φ2∈cl(ψ)andX(φ1Rφ2)∈cl(ψ).
LTLwithregularvaluationsisanextensionofLTLwheretheatomicpropositionscanberegularsetsofcongurationsoverthestackalphabet[9,14].
SLTPLisasexpres-siveasLTLwithregularvaluations.
SincethedomainDisnite,wehave:Proposition1.
LTPLandLTL(resp.
SLTPLandLTLwithregularvaluations)havethesameexpressivepower.
SLTPLismoreexpressivethanLTL.
3.
3ModelingMaliciousBehaviorsUsingSLTPLWeconsideratypicalmaliciousbehavior:windowsvirusesthatcomputetheentryad-dressofKernel32.
dll.
WeshowthatthisbehaviorcanbeexpressedinamoreprecisemannerusingSLTPLinsteadofSCTPL,andthatifweuseSCTPLtodescribeit,wecanobtainfalsealarmsthatcanbeavoidedwhenusingSLTPL(seeTab.
1).
Kernel32.
dllBaseAddressViruses:ManyWindowsvirusesuseAPIfunctionstoachievetheirmalicioustasks.
TheKernel32.
dllleincludesseveralAPIfunctionsthatcanbeusedbytheviruses.
Inordertousethesefunctions,theviruseshavetondtheentryaddressesoftheseAPIfunctions.
Todothis,theyneedtodeterminetheKernel32.
dllentrypoint.
TheydeterminersttheKernel32.
dllPEl1:cmp[eax],5A4Dhjnzl2.
.
.
cmp[ebx],4550hjzl3l2:.
.
.
jmpl1l3(a)(b)l1:.
.
.
.
.
.
jnzl1cmp[eax],5A4Dhcmp[ebx],4550hFig.
2.
422F.
SongandT.
TouiliheaderinmemoryandusethisinformationtolocatetheKernel32.
dllexportsectionandndtheentryaddressesoftheAPIfunctions.
Forthis,theviruslooksrstfortheDOSheader(therstwordoftheDOSheaderis5A4Dhinhex(MZinascii));andthenlooksforthePEheader(thersttwowordsofthePEheaderis4550hinhex(PE00inascii)).
Fig.
2(a)presentsadisassembledcodefragmentperformingthismaliciousbehavior.
ThisbehaviorcanbespeciedinSLTPLusingtheformulaΨwv=GFr1cmp(r1,5A4Dh)∧Fr2cmp(r2,4550h).
ThisSLTPLformulaexpressesthattheprogramhasaloopsuchthattherearetwovariablesr1andr2suchthatrst,r1iscomparedto5A4Dh,andthenr2iscomparedto4550h.
Thisformulacandetectthemal-wareinFig.
2(a).
ItcanbeshownthatthereisnoCTL-likeformulaequivalenttoΨwv.
In[20,19],tobeabletoexpressthismaliciousbehaviorusingaCTL-likeformula,weusedthefollowingformula:Ψwv=EGEFr1cmp(r1,5A4Dh)∧EFr2cmp(r2,4550h).
ThisformulacandetectthemalwareinFig.
2(a).
However,thebenignprograminFig.
2(b)thatcompareswith5A4Dhand4550honlyonceisalsodetectedasamalwareusingΨwvduetotheloopatl1,whileΨwvwillnotdetectitasamalware.
Inourexperiments,asshowninTab.
1,severalbenignprogramsaredetectedasmalwaresusingΨwv,whereasΨwvclassiedthemasbenignprograms.
4LTPLModel-CheckingforPDSsInthissection,weshowhowtoreduceLTPLmodel-checkingforPDSstotheemptinessproblemofsymbolicB¨uchiPDSswhichcanbeefcientlysolvedby[10].
4.
1SymbolicB¨uchiPushdownSystemsASymbolicPushdownSystem(SPDS)Pisatuple(P,Γ,Δ),wherePisanitesetofcontrollocations,ΓisthestackalphabetandΔisasetofsymbolictransitionrulesoftheformp,γΘ→q,ωs.
t.
p,q∈P,γ∈Γ,ω∈Γ,andΘB*B.
Asymbolictransitionp,γΘ→q,ωdenotesthefollowingsetofPDStransi-tionrules:(p,B),γ→(q,B),ωforeveryB,B∈Bs.
t.
(B,B)∈Θ.
Forev-eryω∈Γ,(q,B),ωωisanimmediatesuccessorof(p,B),γω,denotedby(p,B),γωP(q,B),ωω.
Arun(execution)ofPfrom(p0,B0),ω0isasequence(p0,B0),ω0(p1,B1),ω1···overP*B*Γs.
t.
foreveryi≥0,(pi,Bi),ωiP(pi+1,Bi+1),ωi+1.
ASymbolicB¨uchiPushdownSystem(SBPDS)BPisatuple(P,Γ,Δ,F),where(P,Γ,Δ)isaSPDSandFPisanitesetofacceptingcontrollocations.
ArunoftheSBPDSBPisacceptingiffitinnitelyoftenvisitssomecontrollocationsinF.
LetL(BP)bethesetofcongurations(p,B),ω∈P*B*ΓfromwhichBPhasanacceptingrun.
Theorem1.
GivenaSBPDSBP=(P,Γ,Δ,F),foreveryconguration(p,B),ω∈P*B*Γ,whetherornot(p,B),ω∈L(BP)canbedecidedintimeO(|P|·|Δ|2·|D|3|X|).
GivenaSBPDSBPwithncontrollocations,mbooleanvariablesanddtransitionrules,[10]showsthatL(BP)canbecomputedintimeO(n·23m·d2).
WecanuseLTLModel-CheckingforMalwareDetection423|X|·log2|D|booleanvariablestorepresentthesetofvariablesXoverD.
Thus,wecandecidewhether(p,B),ωisinL(BP)intimeO(|P|·|Δ|2·|D|3|X|).
AGeneralizedSymbolicB¨uchiPDS(GSBPDS)BPisatuple(P,Γ,Δ,F),where(P,Γ,Δ)isaSPDSandF={F1,.
.
.
,Fk}isasetofsetsofacceptingcontrollocations.
ArunoftheGSBPDSBPisacceptingiffforeveryi,1≤i≤k,theruninnitelyoftenvisitssomecontrollocationsinFi.
LetL(BP)denotethesetofcongurations(p,B),ω∈P*B*ΓfromwhichtheGSBPDSBPhasanacceptingrun.
Proposition2.
GivenaGSBPDSBP,wecangetaSBPDSBPs.
t.
L(BP)=L(BP).
4.
2FromLTPLModel-CheckingforPDSstotheEmptinessProblemofSBPDSsLetP=(P,Γ,Δ)beaPDS,λ:APD→2Palabelingfunction,ψaLTPLformula.
WeconstructaGSBPDSBPψs.
t.
BPψhasanacceptingrunfrom(p,{ψ},B),ωiffPhasanexecutionπfromp,ωs.
t.
πsatisesψunderB.
Thus,p,ω|=λψiffthereexistsB∈Bs.
t.
BPψhasanacceptingrunfrom(p,{ψ},B),ω(sincep,ω|=λψiffthereexistsB∈Bs.
t.
p,ω|=Bλψ).
LetclU(ψ)={φ1U1,.
.
.
,φkUk}bethesetofU-formulasofcl(ψ).
WedeneBPψ=(P,Γ,Δ,F)asfollows:P=P*2cl(ψ),F={P*Fφ1U1,.
.
.
,P*FφkUk},whereforeveryi,1≤i≤k,FφiUi={Φcl(ψ)|ifφiUi∈Φtheni∈Φ},andΔisthesmallestsetoftransitionrulessatisfyingthefollowing:foreveryΦcl(ψ),p∈P,γ∈Γ,(α1):ifφ=b(x1,.
.
.
,xm)∈Φ,p,Φ,γΘ→p,Φ\{φ},γ∈Δ,whereΘ={(B,B)|B∈B∧p∈λ(b(B(x1),.
.
.
,B(xm)))};(α2):ifφ=b(x1,.
.
.
,xm)∈Φ,p,Φ,γΘ→p,Φ\{φ},γ∈Δ,whereΘ={(B,B)|B∈B∧pλ(b(B(x1),.
.
.
,B(xm)))};(α3):ifφ=φ1∧φ2∈Φ,p,Φ,γΘid→p,Φ∪{φ1,φ2}\{φ},γ∈Δ;(α4):ifφ=φ1∨φ2∈Φ,p,Φ,γΘid→p,Φ∪{φ1}\{φ},γ∈Δandp,Φ,γΘid→p,Φ∪{φ2}\{φ},γ∈Δ;(α5):ifφ=xφ1∈Φ,then:(α5.
1):ifxisnotafreevariableofanyformulainΦ,p,Φ,γΘx→p,Φ∪{φ1}\{φ},γ∈Δ;(α5.
2):otherwise,foreveryc∈D,p,Φ,γΘid→p,Φ∪{φc}\{φ},γ∈Δ,whereφcisφ1wherexissubstitutedbyc;(α6):ifφ=xφ1∈Φ,p,Φ,γΘid→p,Φ∪{φc|c∈D}\{φ},γ∈Δ,whereφcisφ1wherexissubstitutedbyc;(α7):ifφ=φ1Uφ2∈Φ,p,Φ,γΘid→p,Φ∪{φ2}\{φ},γ∈Δandp,Φ,γΘid→p,Φ∪{φ1,Xφ}\{φ},γ∈Δ;(α8):ifφ=φ1Rφ2∈Φ,p,Φ,γΘid→p,Φ∪{φ1,φ2}\{φ},γ∈Δandp,Φ,γΘid→p,Φ∪{φ2,Xφ}\{φ},γ∈Δ;(α9):ifΦ={Xφ1,.
.
.
,Xφm}andp,γ→p,ω∈Δ,p,Φ,γΘid→p,{φ1,.
.
.
,φm},ω∈Δ.
Intuitively,BPψisakindof"product"ofPandψ.
BPψhasanacceptingrunfrom(p,{ψ},B),ωiffPhasanexecutionπstartingfromp,ωs.
t.
πsatisesψunderB.
ThecontrollocationsofBPψareoftheformp,Φ,whereΦisasetofformulas,becausethesatisabilityofasingleformulaφmaydependonseveralotherformulas.
E.
g.
,thesatisabilityofφ1∧φ2dependsonφ1andφ2.
Thus,wehavetostoreasetof424F.
SongandT.
TouiliformulasintothecontrollocationsofBPψ.
Theintuitionbehindeachruleisexplainedasfollows.
(Byabuseofnotation,givenasetofformulasΦ,wewriteπ|=BλΦiffπ|=Bλφforeveryφ∈Φ.
)LetπbeanexecutionofPfromp,ω.
Ifb(x1,.
.
.
,xm)∈Φ,thenπ|=BλΦiffπ|=Bλb(x1,.
.
.
,xm)andπsatisesalltheotherformulasofΦunderB.
ThisisensuredbyItem(α1).
Item(α2)issimilartoItem(α1).
Ifφ1∧φ2∈Φ,then,π|=BλΦiffπ|=Bλφ1,π|=Bλφ2andπsatisesalltheotherformulasofΦunderB.
ThisisensuredbyItem(α3).
Item(α4)isanalogous.
Ifφ1Uφ2∈Φ,then,π|=BλΦiffπ|=Bλφ2holdsorboth(π|=Bλφ1andπ|=BλX(φ1Uφ2))hold,andπsatisesalltheotherformulasofΦunderB.
ThisisensuredbyItem(α7).
Sinceφ2shouldeventuallyhold,topreventthecasewheretherunofBPψalwayscarriesφ1andX(φ1Uφ2)andneverφ2,wesetP*Fφ1Uφ2=P*{Φcl(ψ)|ifφ1Uφ2∈Φthenφ2∈Φ}asasetofacceptingcontrollocations.
Then,theacceptingrunofBPψwillinnitelyoftenvisitsomecontrollocationsinP*Fφ1Uφ2whichguaranteesthatφ2eventuallyholds.
Item(α8)issimilartoItem(α7).
IfΦ={Xφ1,.
.
.
,Xφm},thenπ|=BλΦiffπ1|=Bλ{φ1,.
.
.
,φm}.
ItisensuredbyItem(α9).
Ifxφ∈Φ,thenπ|=BλΦiffπ|=Bλxφandπ|=BλΦ\{xφ}.
Sinceπ|=Bλxφiffπ|=Bλc∈Dφc,whereφcisφ1wherexissubstitutedbyc,wereplacexφbyc∈Dφc.
ThisisexpressedbyItem(α6).
Ifxφ∈Φ,thentheconstructiondependsonwhetherxisafreevariableofsomeformulainΦornot:–ifxisnotafreevariableofanyformulainΦ,thenπ|=BλΦiffthereexistsc∈Ds.
t.
π|=B[x←c]λφandπ|=BλΦ\{xφ}.
SincexisnotafreevariableofanyformulainΦ,wecangetthatπ|=BλΦ\{xφ}iffπ|=B[x←c]λΦ\{xφ}foreveryc∈D.
Thisimpliesthatπ|=BλΦiffthereexistsc∈Ds.
t.
π|=B[x←c]λφandπ|=B[x←c]λΦ\{xφ}.
ThisisensuredbyItem(α5.
1).
–otherwise,ifxisafreevariableofsomeformulainΦ,wecannotapplyItem(α5.
1).
Indeed,itmayhappenthatφissatisedonlywhenx=c,isnotsatisedwhenx=c,whereasπ|=Bλ{,xφ}.
Inthiscase,weapplyItem(α5.
2).
Sinceπ|=BλΦiffπ|=Bλc∈Dφcandπ|=BλΦ\{xφ},whereφcisφwherexissubstitutedbyc.
Sinceπ|=Bλc∈Dφciffthereexistsc∈Ds.
t.
π|=Bλφc,then,π|=BλΦiffthereexistsc∈Ds.
t.
π|=Bλφcandπ|=BλΦ\{xφ}.
ThisisensuredbyItem(α5.
2).
NotethatwecanuseItem(α5.
2)eveninthepreviouscasewhenxisnotafreevariableofanyformulainΦ.
However,itismoreefcienttouseItem(α5.
1)inthiscase,sinceItem(α5.
1)addsonlyonesymbolictransitionrule,whereasItem(α5.
2)adds|D|symbolictransitionrules.
Thus,wecanshowthat:Theorem2.
GivenaPDSP=(P,Γ,Δ),alabelingfunctionλ:APD→2P,andaLTPLformulaψ,wecanconstructaGSBPDSBPψwithO((|Δ|+|P|·|Γ|)·|D|·|X|·2|ψ|)transitionrulesandO(|P|·|D|·|X|·2|ψ|)statess.
t.
foreveryB∈Bandeverycongurationp,ω∈P*Γ,p,ωsatisesψunderBiff(p,{ψ},B),ω∈L(BPψ).
Notethatwedonotneedtoconsiderallthepossiblesubsetsofcl(ψ)duringthecon-structionofBPψ.
Inordertogettheabovecomplexity,wecanmaintainasetofsetsofformulaswhicharereachablefromthecongurationcarryingtheset{ψ}.
FromProposition2,Theorem2andTheorem1,wehave:LTLModel-CheckingforMalwareDetection425Theorem3.
GivenaPDSP=(P,Γ,Δ),alabelingfunctionλ:APD→2PandaLTPLformulaψ,foreveryB∈Bandcongurationp,ω,whetherp,ωsatisesψunderBornotcanbedecidedintimeO(|clU(ψ)|·|P|·|D|·|X|·(|Δ|+|P|·|Γ|)2·23|ψ|·|D|3|X|).
Thecomplexityfollowsfromthefactthatthenumberoftransitionrules(resp.
states)oftheSBPDSequivalenttoBPψisatmostO(|clU(ψ)|·(|Δ|+|P|·|Γ|)·|D|·|X|·2|ψ|)(resp.
O(|clU(ψ)|·|P|·|D|·|X|·2|ψ|)),andtheenvironmentsBonlyneedtoconsiderthevariablesthatareusedinψ.
Remark1.
TodoLTPLmodel-checkingforPDSs,byProposition1,wecantranslateLTPLformulasintoLTLformulasandapplyLTLmodel-checkingforPDSs[6,10].
ThiscanbedoneintimeO(23|ψ|·|D|(|cl(ψ)|+|cl(ψ)|)).
Ourapproachhasabettercomplexity.
5SLTPLModel-CheckingforPDSsInthissection,weshowhowtodoSLTPLmodel-checkingforPDSs.
Wefollowtheapproachof[9].
FixaPDSP,asetofvariablesXoverDandaSLTPLformulaψ.
Roughlyspeaking,foreachRVEeofψ,weconstructakindofniteautomatonVrecognizingallthecongurations(p,ω,B)∈P*Γ*Bs.
t.
(p,ω,B)∈L(e).
Then,wecomputeaSPDSPwhichisakindofsynchronizationofPandtheVsthatallowstodeterminewhetherthestackpredicatesholdatagivenstepbylookingonlyatthetopofthestackofP.
HavingPallowstoreadapttheconstructionofSection4andreducetheSLTPLmodel-checkingproblemforPDSstotheemptinessproblemofSBPDSs.
5.
1ExtendedFiniteAutomataTorepresentRVEs,weintroduceextendedniteautomata,inwhichtransitionrulescanbelabeledbyasetofvariablesand/ortheirnegations.
Formally,letP=(P,Γ,Δ)beaPDSandξ={α,α|α∈Γ∪X},anExtendedFiniteAutomaton(EFA)Visatuple(S,Λ,Γ,s0,Sf)whereSisanitesetofstates,Γistheinputalphabet,s0∈Sistheinitialstate,SfSisanitesetofnalstates,andΛisanitesetoftransitionrulesoftheforms1→s2s.
t.
s1,s2∈S,ξ.
LetB∈Bbeanenvironment,γ∈Γtheinputletter,supposeVisatstates1andt=s1→s2isatransitionruleinΛ,thenVcanmovetothestates2(i.
e.
,s2isanimmediatesuccessorofs1underBoverγ),denotedbys1γBs2,iffthefollowingconditionshold:(1)foreveryα∈,B(α)=γ;(2)foreveryα∈,B(α)γ(notethatB(γ)=γifγ∈Γ).
Obviously,thetransitiontwillneverberedwheneitherγ1,γ2∈∩Γs.
t.
γ1γ2orα,α∈forsomeα∈Γ∪X.
ThisimpliesthatcancontainonlyoneletterfromΓ,andforeachα∈X∪Γ,cannotcontainbothαandα.
Vrecognizes(accepts)awordγ0.
.
.
γnoverΓunderBiffVhasaruns0γ0Bs1.
.
.
snγnBsn+1s.
t.
sn+1∈Sf.
LetL(V)bethesetofallthecongurations(p,ω,B)∈P*Γ*Bs.
t.
VrecognizesωunderB.
AEFAVisdeterministic(resp.
total)iffforeverystates∈S,environmentB∈B,letterγ∈Γ,shasatmost(resp.
atleast)oneimmediatesuccessors∈SunderBoverγ.
Wecanshowthat:426F.
SongandT.
TouiliProposition3.
ForeveryEFAV=(S,Λ,Γ,s0,Sf),wecancomputeintimeO(2|Λ|)adeterministicandtotalEFAVs.
t.
L(V)=L(V).
Theorem4.
Foreveryregularpredicatee∈R,wecangetinpolynomialtimeanEFAVes.
t.
L(e)=L(Ve).
Givenaconguration(p,γ1.
.
.
γm,B)∈P*Γ*B,itsreverse(p,γ1.
.
.
γm,B)ristheconguration(p,γm.
.
.
γ1,B).
GivenasetLP*Γ*B,itsreverseLristheset{(p,γm.
.
.
γ1,B)|(p,γ1.
.
.
γm,B)∈L}.
Wecanshowthat:Proposition4.
ForeveryEFAV,wecangetanEFAVrinlineartimes.
t.
L(V)r=L(Vr).
Remark2.
TorepresentRVEs,[20]usesautomatawithalternatingtransitionrules,calledVariableAutomata(VA).
IfweuseVAstorepresentvariableexpressions,wewillobtainanalternatingSBPDSwhensynchronizingtheSLTPLformulawiththePDS.
WeintroduceEFAstoavoidusingalternation,sincecheckingtheemptinessofalternatingSBPDSsisexponentialinthesizeofthePDSs[20].
[11]introducesanotherkindofVAs,whichisnotsuitableforourpurpose,sincedeterminizingaVAasdenedin[11]isundecidable,but,weneedtheautomatatobedeterministicaswillbeexplainedlater.
5.
2StoringStatesintotheStackWexaPDSP=(P,Γ,Δ)andaSLTPLformulaψ.
Let{e1,.
.
.
,en}bethesetofRVEsusedinψ.
Wesupposew.
l.
o.
g.
thatPhasabottom-of-stack⊥∈Γthatisneverpoppedfromthestack.
Foreveryi,1≤i≤n,letVi=(Si,Λi,Γ,si0,Sif)beadeterministicandtotalEFAs.
t.
L(ei)r=L(Vi).
Sincewehavepredicatesoverthestack,tocheckwhethertheformulaψissatised,weneedtoknowateachstepwhichRVEsaresatisedbythestack.
Tothisaim,wewillcomputeaSPDSPwhichisakindofproductofPandtheEFAsV1,.
.
.
,Vn,wherethestatesoftheVisarestoredinthestackofP.
Roughlyspeaking,thestackalphabetofPisoftheform(γ,→S),where→S=s1,sn,si∈Siforeveryi,1≤i≤n,isavectorofstatesoftheEFAsV1,.
.
.
,Vn.
Foreveryi,1≤i≤n,let→S(i)denotetheithcomponentof→S.
Aconguration(p,B),(γm,→Sm)···(γ0,→S0)isconsistentiffforeveryi,1≤i≤n,Vihasarun→S0(i)γ0B→S1(i)···→Sm1(i)γm1B→Sm(i)overγ0···γm1,i.
e.
,thereverseofthestackcontentγm1···γ0.
Intuitively,aconsis-tentconguration(p,B),(γm,→Sm)···(γ0,→S0)denotesthatthestackcontentisγm···γ0andtherunsoftheEFAsV1,.
.
.
,Vnoverγ0···γm1reachthestates→Sm(1),.
.
.
,→Sm(n),respectively(notethatγ0···γm1isthereverseofthestackcontentγm1···γ0,thisiswhytheVisares.
t.
L(ei)r=L(Vi)).
Foreveryi,1≤i≤n,aconsistentconguration(p,B),(γm,→Sm)γ0,→S0)satiseseiundertheenvironmentBiffthereexistss∈Sifs.
t.
→Sm(i)γmBs.
I.
e.
,whether(p,B),(γm,→Sm)···(γ0,→S0)satiseseiunderBornotdependsonlyonthetopofthestack(γm,→Sm).
Formally,let→S=S1Snand→S0=s10,sn0.
WecomputetheSPDSP=(P,Γ,Δ)asfollows:Γ=Γ*→SisthestackalphabetandthesetΔoftransitionrulesaredenedasfollows:LTLModel-CheckingforMalwareDetection4271.
p1,(γ,→S)Θid→p2,∈Δiffp1,γ→p2,∈Δand→S∈→S;2.
p1,(γ,→S)Θid→p2,(γ1,→S)∈Δiffp1,γ→p2,γ1∈Δand→S∈→S;3.
p1,(γ,→S)Θ→p2,(γ2,→S)(γ1,→S)∈Δiffp1,γ→p2,γ2γ1∈Δandforeveryi,1≤i≤n,→S(i)i→→S(i)∈Λi,whereΘ={(B,B)|B∈B,i:1≤i≤n,(x∈i=B(x)=γ1)∧(y∈i=B(y)γ1)}.
Intuitively,therunofPreachesthecongurationp1,γm,···γ0andtherunsoftheEFAsV1,.
.
.
,Vnoverthestackwordγ0···γm1reachthestates→Sm(1),.
.
.
,→Sm(n),respectively,ifftherunofPreachestheconsistentconguration(p1,B),(γm,→Sm)···(γ0,→S0).
IfPmovesfromp1,γm,···γ0top2,γm1,···γ0usingtherulep1,γm→p2,,thentheEFAsV1,.
.
.
,Vnshouldbeat→Sm1(1),.
.
.
,→Sm1(n)afterreadingthestackwordγ0···γm2,i.
e.
,Pmovesfrom(p1,B),(γm,→Sm)···(γ0,→S0)to(p2,B),(γm1,→Sm1)···(γ0,→S0).
ThisisensuredbyItem1.
TheintuitionbehindItem2issimilar.
IfPmovesfromp1,γmγm1···γ0top2,γm+1γm···γ0usingtherulep1,γm→p2,γm+1γm,then,afterreadingγ0···γm,theEFAsV1,.
.
.
,Vnshouldbeat→Sm+1(1),.
.
.
,→Sm+1(n)whereforeveryi,1≤i≤n,→Sm(i)γmB→Sm+1(i).
I.
e.
,Pmovesfrom(p1,B),(γm,→Sm)(γm1,→Sm1)···(γ0,→S0)to(p2,B),(γm+1,→Sm+1)(γm,→Sm)γ0,→S0).
ThisisensuredbyItem3.
TherelationΘ={(B,B)|B∈B,i:1≤i≤n,(x∈i=B(x)=γm)∧(y∈i=B(y)γm)}inthetransitionrulep1,(γm,→Sm)Θ→p2,(γm+1,→Sm+1)(γm,→Sm)guaranteesthatforeveryi,1≤i≤n,thestate→Sm+1(i)istheimmediatesuccessorofthestate→Sm(i)overγmunderBinVi.
ThefactthatEFAsaredeterministicguaranteesthatthetopofthestackcaninferthetruthoftheregularpredicates.
ThefactthatEFAsaretotalmakessurethattheEFAsalwayshaveasuccessorstateonanarbitraryinputandenvironment.
5.
3ReadaptingtheReductionunderlyingTheorem2Inthissubsection,weshowhowtoreducetheSLTPLmodel-checkingproblemforSPDSstotheemptinessproblemofSBPDSsbyareadaptationoftheconstructionun-derlyingTheorem2.
LetBPψ=(P,Γ,Δ,F)betheGSBPDSs.
t.
:P=P*2cl(ψ),F={P*Fφ1U1,.
.
.
,P*FφkUk},whereforeveryi,1≤i≤k,FφiUi={Φcl(ψ)|φiUiΦori∈Φ},andΔisthesmallestsetoftransitionrulessatisfyingthefollowing:foreveryΦcl(ψ),p∈P,(γ,→S)∈Γ:(β1):ifφ=b(x1,.
.
.
,xm)∈Φ,p,Φ,(γ,→S)Θ→p,Φ\{φ},(γ,→S)∈Δ,whereΘ={(B,B)|B∈B∧p∈λ(b(B(x1),.
.
.
,B(xm)))};(β2):ifφ=b(x1,.
.
.
,xm)∈Φ,p,Φ,(γ,→S)Θ→p,Φ\{φ},(γ,→S)∈Δ,whereΘ={(B,B)|B∈B∧pλ(b(B(x1),.
.
.
,B(xm)))};(β3):ifφ=φ1∧φ2∈Φ,p,Φ,(γ,→S)Θid→p,Φ∪{φ1,φ2}\{φ},(γ,→S)∈Δ;(β4):ifφ=φ1∨φ2∈Φ,p,Φ,(γ,→S)Θid→p,Φ∪{φ1}\{φ},(γ,→S)∈Δandp,Φ,(γ,→S)Θid→p,Φ∪{φ2}\{φ},(γ,→S)∈Δ;(β5):ifφ=xφ1∈Φ,then:428F.
SongandT.
Touili(β5.
1):ifxisnotafreevariableofanyformulainΦ,p,Φ,(γ,→S)Θx→p,Φ∪{φ1}\{φ},(γ,→S)∈Δ;(β5.
2):otherwiseforeveryc∈D,p,Φ,(γ,→S)Θid→p,Φ∪{φc}\{φ},(γ,→S)∈Δ,whereφcisφ1wherexissubstitutedbyc;(β6):ifφ=xφ1∈Φ,p,Φ,(γ,→S)Θid→p,Φ∪{φc|c∈D}\{φ},(γ,→S)∈Δ,whereφcisφ1wherexissubstitutedbyc;(β7):ifφ=φ1Uφ2∈Φ,p,Φ,(γ,→S)Θid→p,Φ∪{φ2}\{φ},(γ,→S)∈Δandp,Φ,(γ,→S)Θid→p,Φ∪{φ1,Xφ}\{φ},(γ,→S)∈Δ;(β8):ifφ=φ1Rφ2∈Φ,p,Φ,(γ,→S)Θid→p,Φ∪{φ1,φ2}\{φ},(γ,→S)∈Δandp,Φ,(γ,→S)Θid→p,Φ∪{φ2,Xφ}\{φ},(γ,→S)∈Δ;(β9):ifΦ={Xφ1,.
.
.
,Xφm},foreveryp,(γ,→S)Θ→p,ω∈Δ,p,Φ,(γ,→S)Θ∩Θid→p,{φ1,.
.
.
,φm},ω∈Δ;(β10):ifφ=ei∈Φ∩R,p,Φ,(γ,→S)Θ→p,Φ\{φ},(γ,→S)∈Δ,whereΘ={(B,B)|B∈B,→S,→S(i)γB→S(i)∧→S(i)∈Sif};(β11):ifφ=ei∈Φs.
t.
ei∈R,p,Φ,(γ,→S)Θ→p,Φ\{φ},(γ,→S)∈Δ,whereΘ={(B,B)|B∈B,→S,→S(i)γB→S(i)∧→S(i)Sif}.
TheintuitionbehindBPψissimilartotheoneunderlyingTheorem2.
Phasanexecu-tionπstartingfromp,γm,.
.
.
,γ0s.
t.
πsatisesψunderBiffthereexiststates→Sm,.
.
.
,→S0s.
t.
(p,{ψ},B),(γm,→Sm)γ0,→S0)isconsistentandBPψhasanacceptingrunfrom(p,{ψ},B),(γm,→Sm)···(γ0,→S0).
Items(β1)β8)aresimilartoItems(α1)α8).
ThemaindifferencesareItems(β9),(β10)and(β11).
TherelationΘ∩ΘidinItem(β9)ensuresthat(p,{φ1,.
.
.
,φm},B),ωωisanimmediatesuccessorof(p,{Xφ1,.
.
.
,Xφm},B),(γ,→S)ωintherunofBPψiff(p,B),ωωisanimmediatesuccessorof(p,B),(γ,→S)ωinthecorrespondingrunofP,as(B,B)∈Θ∩Θidimpliesthat(B,B)∈Θ.
ThisimpliesthatBPψhasanacceptingrunfrom(p,{Xφ1,.
.
.
,Xφm},B),(γ,→S)ωiffPhasanimmedi-atesuccessor(p,B),ωωof(p,B),(γ,→S)ωs.
t.
BPψhasanacceptingrunfrom(p,{φ1,.
.
.
,φm},B),ωω.
Item(β10)expressesthatifei∈Φ,thenforeveryexecutionπs.
t.
π(0)=p,γm···γ0,π|=BλΦiffπ|=BλΦ\{ei}andπ|=Bλei(i.
e.
,(p,γm···γ0,B)∈L(ei),meaningthereexist→Sm+1,.
.
.
,→S0∈→Ss.
t.
foreveryj,0≤j≤m,→Sj(i)γjB→Sj+1(i)and→Sm+1(i)∈Sif).
ThisisguaranteedbyItem(β10)statingBPψhasanaccept-ingrunfrom(p,Φ,B),(γm,→Sm)···(γ0,→S0)iffBPψhasanacceptingrunfrom(p,Φ\{ei},B),(γm,→Sm)···(γ0,→S0)andthereexists→Sm+1∈→Ss.
t.
→Sm(i)γmB→Sm+1(i)and→Sm+1(i)∈Sif.
TheintuitionbehindItem(β11)issimilartoItem(β10).
Wegetthat:Theorem5.
Forevery(p,γm···γ0,B)∈P*Γ*B,p,γm···γ0|=Bλψiffthereexist→Sm,.
.
.
,→S0∈→Ss.
t.
(p,{ψ},B),(γm,→Sm)···(γ0,→S0)isconsistentandisinL(BPψ).
LTLModel-CheckingforMalwareDetection429FromProposition2,Theorem1andTheorem5,weobtainthat:Theorem6.
GivenaPDSP=(P,Γ,Δ),alabelingfunctionλ:APD→2PandaSLTPLformulaψ,forevery(p,ω,B)∈P*Γ*B,whetherornotp,ωsatisesψunderBcanbedecidedintimeO(|clU(ψ)|·|D|·|X|·|P|·(|Δ|+|P|·|Γ|)2·|→S|2·23|ψ|·|D|3|X|).
6ExperimentsWeimplementedourtechniquesinatoolformalwaredetection.
WeuseBDDstocom-pactlyrepresenttherelationsΘ.
Weevaluatedourtoolon270malwarestakenfromVXHeavensand27benignprogramstakenfromMicrosoftWindowsXPsystem.
Alltheex-perimentswererunonFedora13witha2.
4GHzCPU,2GBofmemory.
Thetimelimitisxedto20minutes.
Moreover,wecomparedtheperformancesofourtechniqueswithSCTPL[19]andLTLwithregularvaluations[9](denotedbyLTLr)model-checking.
Ourtoolwasabletodetectallthemalwares.
Duetolackofspace,Tab.
1showssomeresults.
TimeandmemoryaregiveninsecondsandMBrespectively.
#LOCde-notesthenumberofinstructionsoftheassemblyprogram.
TheresultYesdenotesthattheprogramisdetectedasamalware,otherwisetheresultisNo.
AscanbeseeninTab.
1,inmostcases,SLTPLmodel-checkingperformsbetter.
TheanalysisofseveralmalwaresusingSCTPLorLTLrmodel-checkingrunsoutofmemoryortime,whereasourtoolterminatesandisabletodetectthesemalwares.
Moreover,usingtheSCTPLTable1.
SomeResultsofMalwareDetectionExample#LOCSLTPLSCTPLLTLrTimeMemoryResultTimeMemoryResultTimeMemoryResultVirusAkez26413.
7859.
02Yes14.
7515.
59YestimeoutAlcaul.
b9049.
7937.
40Yes26.
251.
08YestimeoutAlcaul.
c3472.
059.
40Yes26.
522.
45Yes365.
53225.
67YesAlcaul.
d8370.
240.
17Yes23.
5220.
39YestimeoutEmail-wormKirbster1261948.
521383.
02Yeso.
o.
m.
timeoutKrynos.
b18357987.
22947.
92Yeso.
o.
m.
timeoutNewapt.
B117031120.
211042.
74Yeso.
o.
m.
timeoutNewapt.
F117711045.
17908.
35Yeso.
o.
m.
timeoutNewapt.
E117171059.
45970.
27Yeso.
o.
m.
timeoutMydoom.
j2233589.
6640.
15Yes200.
4148.
17YestimeoutMydoom.
v596010.
7819.
03Yes66.
3416.
49Yes1131.
001010.
24YesMydoom.
y2690266.
7736.
60Yes90.
0043.
19YestimeoutTrojanLdPinch.
aar124532.
03198.
88Yes1.
668.
47YestimeoutLdPinch.
aoq768846.
29234.
86Yes7.
3310.
13YestimeoutLdPinch.
mj595239.
07199.
28Yes5.
748.
90YestimeoutLdPinch.
ld66098.
3713.
36Yes5.
414.
24Yes452.
93410.
85YesBenignCmd.
exe35887109.
8120.
00Noo.
o.
m.
timeoutBlastcln.
exe13819103.
8780.
53No27.
726.
30YestimeoutRegsvr32.
exe12807.
3126.
85No0.
481.
87Yes158.
0648.
15Noipv6.
exe1370089.
1431.
04No60.
453.
14Yestimeoutdplaysvr.
exe679635.
4630.
39No17.
122.
84YestimeoutShutdown.
exe252431.
6962.
93Noo.
o.
m.
timeoutRegedt.
exe600.
020.
02No10.
620.
03Yes0.
020.
02NoJava.
exe21868184.
5827.
96No78.
64238.
77Yestimeout430F.
SongandT.
TouiliformulaΨwv(describedinSection3.
3)causesfalsealarmswhenchecking21benignprograms,whereasusingSLTPLwecorrectlyclassifytheseprogramsasbenign.
More-over,ourtoolwasabletodetectthewell-knownmalwareFlameandtodetectseveralothermalwaresthatcouldnotbedetectedbywell-knownanti-virusessuchasAvira,Avast,Kaspersky,McAfee,AVG,BitDefender,EsetNod32,F-Secure,Norton,Panda,TrendMicroandQihoo360.
References1.
Babic,D.
,Reynaud,D.
,Song,D.
:MalwareAnalysiswithTreeAutomataInference.
In:Gopalakrishnan,G.
,Qadeer,S.
(eds.
)CAV2011.
LNCS,vol.
6806,pp.
116–131.
Springer,Heidelberg(2011)2.
Beaucamps,P.
,Gnaedig,I.
,Marion,J.
-Y.
:BehaviorAbstractioninMalwareAnalysis.
In:Barringer,H.
,Falcone,Y.
,Finkbeiner,B.
,Havelund,K.
,Lee,I.
,Pace,G.
,Rosu,G.
,Sokolsky,O.
,Tillmann,N.
(eds.
)RV2010.
LNCS,vol.
6418,pp.
168–182.
Springer,Hei-delberg(2010)3.
Beaucamps,P.
,Gnaedig,I.
,Marion,J.
-Y.
:Abstraction-BasedMalwareAnalysisUs-ingRewritingandModelChecking.
In:Foresti,S.
,Yung,M.
,Martinelli,F.
(eds.
)ESORICS2012.
LNCS,vol.
7459,pp.
806–823.
Springer,Heidelberg(2012)4.
Bergeron,J.
,Debbabi,M.
,Desharnais,J.
,Erhioui,M.
,Lavoie,Y.
,Tawbi,N.
:Staticdetectionofmaliciouscodeinexecutableprograms.
In:SREIS(2001)5.
Bonfante,G.
,Kaczmarek,M.
,Marion,J.
-Y.
:ArchitectureofaMorphologicalMalwareDe-tector.
JournalinComputerVirology5,263–270(2009)6.
Bouajjani,A.
,Esparza,J.
,Maler,O.
:ReachabilityAnalysisofPushdownAutomata:Ap-plicationtoModel-Checking.
In:Mazurkiewicz,A.
,Winkowski,J.
(eds.
)CONCUR1997.
LNCS,vol.
1243,pp.
135–150.
Springer,Heidelberg(1997)7.
Christodorescu,M.
,Jha,S.
:Staticanalysisofexecutablestodetectmaliciouspatterns.
In:12thUSENIXSecuritySymposium(2003)8.
Christodorescu,M.
,Jha,S.
,Seshia,S.
A.
,Song,D.
X.
,Bryant,R.
E.
:Semantics-awaremal-waredetection.
In:IEEESymposiumonSecurityandPrivacy(2005)9.
Esparza,J.
,Kucera,A.
,Schwoon,S.
:ModelcheckingLTLwithregularvaluationsforpush-downsystems.
Inf.
Comput.
186(2)(2003)10.
Esparza,J.
,Schwoon,S.
:ABDD-BasedModelCheckerforRecursivePrograms.
In:Berry,G.
,Comon,H.
,Finkel,A.
(eds.
)CAV2001.
LNCS,vol.
2102,pp.
324–336.
Springer,Heidelberg(2001)11.
Grumberg,O.
,Kupferman,O.
,Sheinvald,S.
:VariableAutomataoverInniteAlphabets.
In:Dediu,A.
-H.
,Fernau,H.
,Martn-Vide,C.
(eds.
)LATA2010.
LNCS,vol.
6031,pp.
561–572.
Springer,Heidelberg(2010)12.
Hodkinson,I.
,Wolter,F.
,Zakharyaschev,M.
:MonodicFragmentsofFirst-OrderTempo-ralLogics:2000-2001A.
D.
In:Nieuwenhuis,R.
,Voronkov,A.
(eds.
)LPAR2001.
LNCS(LNAI),vol.
2250,pp.
1–23.
Springer,Heidelberg(2001)13.
Kinder,J.
,Katzenbeisser,S.
,Schallhart,C.
,Veith,H.
:DetectingMaliciousCodebyModelChecking.
In:Julisch,K.
,Kruegel,C.
(eds.
)DIMVA2005.
LNCS,vol.
3548,pp.
174–187.
Springer,Heidelberg(2005)14.
Kupferman,O.
,Piterman,N.
,Vardi,M.
Y.
:AnAutomata-TheoreticApproachtoInnite-StateSystems.
In:Manna,Z.
,Peled,D.
A.
(eds.
)TimeforVerication.
LNCS,vol.
6200,pp.
202–259.
Springer,Heidelberg(2010)15.
Lakhotia,A.
,Boccardo,D.
R.
,Singh,A.
,Manacero,A.
:Context-sensitiveanalysisofobfus-catedx86executables.
In:PEPM(2010)LTLModel-CheckingforMalwareDetection43116.
Lakhotia,A.
,Kumar,E.
U.
,Venable,M.
:Amethodfordetectingobfuscatedcallsinmali-ciousbinaries.
IEEETrans.
SoftwareEng.
31(11)(2005)17.
Singh,P.
K.
,Lakhotia,A.
:Staticvericationofwormandvirusbehaviorinbinaryexecuta-blesusingmodelchecking.
In:IAW(2003)18.
Sistla,A.
P.
,Vardi,M.
Y.
,Wolper,P.
:Thecomplementationproblemforb¨uchiautomatawithappplicationstotemporallogic.
Theor.
Comput.
Sci.
49,217–237(1987)19.
Song,F.
,Touili,T.
:EfcientMalwareDetectionUsingModel-Checking.
In:Giannakopoulou,D.
,Mery,D.
(eds.
)FM2012.
LNCS,vol.
7436,pp.
418–433.
Springer,Heidelberg(2012)20.
Song,F.
,Touili,T.
:PushdownModelCheckingforMalwareDetection.
In:Flanagan,C.
,K¨onig,B.
(eds.
)TACAS2012.
LNCS,vol.
7214,pp.
110–125.
Springer,Heidelberg(2012)21.
Wang,F.
,Tahar,S.
,Mohamed,O.
A.
:First-OrderLTLModelCheckingUsingMDGs.
In:Wang,F.
(ed.
)ATVA2004.
LNCS,vol.
3299,pp.
441–455.
Springer,Heidelberg(2004)22.
Xu,Y.
,Cerny,E.
,Song,X.
,Corella,F.
,Mohamed,O.
A.
:ModelCheckingforaFirst-OrderTemporalLogicUsingMultiwayDecisionGraphs.
In:Vardi,M.
Y.
(ed.
)CAV1998.
LNCS,vol.
1427,pp.
219–231.
Springer,Heidelberg(1998)