| « M E N U » |
»
|
| » Ktoś, kto mówi, że nie zna się na sztuce, źle zna samego siebie. | | » Aldiss Brian W. - Na zewnątrz, KSIĄŻKI, E-book, Aldiss Brian | | » Aldiss Brian Wilson - Opowiadania I, e-book, Aldiss Brian | | » Aldiss Brian Wilson - Kryptozoik, e-book, Aldiss Brian | | » Aldiss Brian W. - Nieobliczalna gwiazda, KSIĄŻKI, E-book, Aldiss Brian | | » Alex Joe - Cicha jak ostatnie tchnienie, e-book, Alex Joe | | » Alistair MacLean - Łamacz kodów, KSIĄŻKI, E-book, Alistair MacLean | | » Alistair MacLean - Rzeka Śmierci, KSIĄŻKI, E-book, Alistair MacLean | | » Aldiss Brian W. - Kamyczki Poety Tu Fu, KSIĄŻKI, E-book, Aldiss Brian | | » Alistair MacLean - Air Force One zaginął, KSIĄŻKI, E-book, Alistair MacLean | | » Al-Râzî's Book of Secrets - The Practical Laboratory in the Medieval Islamic World by Gail Marlow Taylor (2008), Alchemia i spagiryka |
zanotowane.pldoc.pisz.plpdf.pisz.plefriends.pev.pl
|
|
|
[ Pobierz całość w formacie PDF ]
AlgebraicSpecificationofComputerViruses
andTheirEnvironments
MattWebster
?
M.P.Webster@csc.liv.ac.uk
DepartmentofComputerScience,UniversityofLiverpool,Liverpool,L697ZF,UK
Abstract.Thispaperintroducesanapproachtoformalspecificationof
computervirusesandtheirenvironmentsthroughthedevelopmentofal-
gebraicspecificationsusingGurevich’sAbstractStateMachines(ASMs)
andGoguen’sOBJ.DistributedASMsareusedtodevelopamodelof
anabstractcomputervirus,whichthroughaprocessofrefinementis
convertedintomodelsofdierentvirustypes.Furtherrefinementhas
resultedinanexecutablespecification,writtenintheAbstractState
MachineLanguage,AsmL.Themodelsstrengthenthethesisthatany
algorithmcanbemodelledatanaturalabstractionlevelusinganAb-
stractStateMachine.TheASMmodelscombinedwiththeAsmLex-
ecutablespecificationprovideacomplementarytheoreticalandexperi-
mentalframeworkforproofsandexperimentsoncomputervirusesand
theirenvironments,aswellasausefulmeansofclassificationofdierent
computervirusestypes.Nextwelookatadierentapproachtocomputer
virusanalysisusingOBJ,whichisusedtospecifycomputerviruseswrit-
teninanadhocprogramminglanguage,SPL.TheOBJspecificationis
showntobeusefulforthedetectionofavirustypethatisparticularly
diculttodetect–themetamorphiccomputervirus(MCV).Finally,the
usefulnessofthetwospecificationsforreasoningaboutcomputerviruses
isdiscussedandinthisregardthetwoformalismsarecompared.
1Introduction
Computervirusesare(oftenharmful)computerprogramsthatreplicateau-
tonomouslythroughcomputerfilesystems.Theyaretypicallydesignedtorepli-
catewithouttheusers’consent,andareabletodamagedataorsoftwareon
infectedmachines.Ingeneral,computervirusesreplicateusingthelegitimate
infrastructureofanoperatingsystem(e.g.diskinput/outputroutines),and
consequentlythespreadofcomputervirusesisdiculttopreventabsolutely
withoutrestrictingtheoperatingsystem(OS)insomeway.
Academicstudyofcomputervirusesbeganin1987,whenCohendefinedan
abstractcomputervirusandgaveaproofoftheundecidabilityofcomputervirus
detection,provingthattherewouldbenodetection-basedpanaceaforthecom-
putervirusproblem[1].Preventingcomputervirusesthroughtheuseofseverely
?
WiththankstomysupervisorsGrantMalcolmandAlexeiLisitsa,forshowingme
thepowerandbeautyofalgebraicspecification.
100
restrictedoperatingsystemsispossible,sincethecomputerviruscanonlywork
bymodifyingstoredprogramsinmemorysothattheycontainacopyofthe
virus.However,thecomputerarchitecturethatallowsprogramcreationand
modificationisatthecoreoftheflexibilityandeciencyofmoderncomputers;
forexample,nocompilercouldrunwithoutthecreationandmodificationof
storedprograms.Thus,findingacureforcomputervirusesbyrestrictingtheir
environmentsisimpractical,andreliabledetectionisimpossible.Thereforethe
fighttostopillicitcomputervirusesbecomesaquestionofoptimization,i.e.,
“Howcanwebestprotectourselvesagainstcomputerviruses?”Inaddition,
tractabilityisaprimaryconcernduetothetrade-obetweeneciencyand
thoroughnessofanti-virus(AV)scanners.Withthisandthesustainedprolifera-
tionofcomputervirusesinmind,generaltheoriesofcomputervirusesandtheir
environmentswouldbeuseful.Formalspecificationofthebehaviourofdierent
virustypescanprovideinsighttodevelopersofanti-virussoftwarebyhighlight-
ingthecommonalitybetweendierentcomputerviruses,e.g.byencouragingthe
reuseofdetectionanddisinfectionmethods.Knowledgeofwhichspecificdetails
oftheimplementationofcomputersystemsaordsurvivalforvirusescanbede-
rivedfromformalmodels,andcanbeusedtorestrictcomputervirusbehaviour
throughthedevelopmentofsystemsthatareinherently(andprovably)more
secure.
Inthispaper,twoseparateapproachestocomputervirusformalisationare
presented.In§2AbstractStateMachines[2]areusedtobuildaformalmodel
ofanabstractcomputervirus,whichisrefinedtoseveralmorespecificvirus
types.AnexecutablespecificationinAsmL(basedontheASMmodels)isgiven,
formingwiththeASMmodelsacomplementarytheoreticalandexperimental
test-bedforformalproofsoncomputervirusesandtheirenvironments,aswell
asaformalmeansofcomputerviruscategorisation.OBJ[3]isusedin§3to
buildaformalframeworkforcomputervirologybasedonorder-sortedequational
rewriting.Anadhocsimpleprogramminglanguage(SPL)isusedtoimplement
computervirusesandexecutablefiles,andaformallanguagerepresentationof
anoperatingsystemiscreated.In§3.3apromisingnewmeansofdetecting
metamorphiccomputervirusesbasedontheOBJspecificationisdemonstrated.
In§4itisshownhowtheseformalalgebraicspecificationsarereadilyapplicable
tocomputervirusdetectiontechnologythroughtheapplicationofthedevelop-
mentsmadeinMCVdetectionandcomputervirusclassification.
1.1MetamorphicComputerViruses
Theundecidabilityofcomputervirusdetectionisoneoftheoldestresultsin
thefieldofcomputervirology,butanti-virusscannershavetraditionallycom-
pensatedforthisbyexploitingaweaknesscommontomanyna¨ıvecomputer
viruses:constantsyntax.Thestringofbinarydigitscorrespondingtoaparticu-
larcomputervirususuallyremainsunchangedfromonegenerationtothenext,
asdoestheplacementofthecomputerviruswithintheinfectedexecutablefile,
e.g.oneparticularvirusmightbeplacedatthestartofanyexecutableitinfects.
AVscannerswouldsearchexecutablefilesforvirus“signatures”–stringsofbits
101
thatcorrespondtoaparticularvirus–attheusualsitesofinfectionwithinexe-
cutablesfiles.Thepresenceofasignaturewouldsignalthattheexecutablewas
infected,andthatfurtherstepsneededtobetakentodisinfectthefile.
Inordertoavoiddetection,thewritersofcomputervirusesbegantodevelop
waysofobfuscatingthesuspectviruscode.Oneattemptatthis,thepolymor-
phiccomputervirus,whichchangesitssyntactic(binarydigit)representation
usingencryption,failstoremainhiddenfromAVscannersonceitsmeansof
decryptionhasbeendiscovered.Oncedecrypted,allgenerationsofpolymorphic
computerviruseslookalike,andthesignature-basedapproachtodetectioncan
beused.Amorepowerfulmeansofdetectionavoidanceisemployedbythemeta-
morphiccomputervirus.Eachsuccessivegenerationofametamorphiccomputer
virusmodifiesthesyntax,butleavesthesemanticsunchanged.Inthiswaythe
behaviourofeachsuccessivegenerationisthesame,butthevirusappearsto
bedierent.Thus,itbecomesmuchmoredicultforanAVscannertodetect
ametamorphiccomputervirususingasignature-basedapproach,anditisnot
possibletokeeparecordofallpossiblegenerationsbecausethereareanun-
limitednumber
1
.Inthiswaythemetamorphiccomputercansuccessfullyavoid
detection[4].
Thisproblemisnotconfinedtoaparticularprogramminglanguage.Within
anyTuring-completeprogramminglanguagethereissomeredundancy,thatis,
themappingfromsyntaxtosemanticsismany-to-one
2
.Thisredundancyal-
lowsthemetamorphiccomputervirustoavoiddetection(bysignature-based
methods)throughautomatedsyntacticvariantgenerationatrun-time.
1.2RelatedWork
Agoodintroductiontotheoreticalcomputervirologyandtheformalisationof
computervirusescanbefoundinearlyworkbyCohen[1,5]andAdleman[6].
FurthertoCohen’sworkontheundecidabilityofcomputervirusdetection,
Spinellishasrecentlydemonstrated[7]thatreliableidentificationofaknown
virusisnp-complete,andThimblebyetal[8]havedevelopedaformalismto
describetrojansandcomputervirusinfection.Additionally,Lakhotia&Mo-
hammed[9]havestudiedanapproachbasedonimposingorderonhigh-level
languagestatementsinordertoreducethenumberofsyntacticvariantsand
thereforeaidMCVdetection.
1
Programsizeis(theoretically)unlimited,soaninfinitenumberofvariantsonasingle
metamorphiccomputervirusispossiblethroughtheintroductionof“junkcode”
thatdoesnotalterthestateofthemachine,butneverthelesshasasyntactical
representation.Agoodexamplewouldbethe
NOP
instructionin68000assembly
language,whichdoesnotalterthestateatalluponitsexecution.
2
SupposethatthereisaTuring-completeprogramminglanguageforwhichthereisa
one-to-onemappingfromsyntaxtosemantics.Ifsuchalanguageexisted,itwouldbe
possibletoprovetheequivalenceofanytwoprograms
p
1
and
p
2
bytranslationinto
thislanguage.Sinceprogramequivalenceisanundecidableproblem,therecanbeno
suchlanguage.(Thisproofassumesthatifsuchalanguageexistedthentranslation
intothelanguagewouldbepossible.)
102
2TheASMApproach
AbstractStateMachines(formerlyknownasEvolvingAlgebras)areaformal
approachtoalgebraicspecificationofsoftwaresystems,whereeachstepofan
algorithmistreatedasaboundednumberofchangestoanalgebra,andthe
wholealgorithmcanbedescribedusingafinitenumberofsimpletransition
rules.TheASMthesisstatesthatanyalgorithmcanbemodelledatanatural
abstractionlevelusinganASM[2].
Algebraically,anAbstractStateMachineisdefinedasfollows.LetAbean
AbstractStateMachine.Thevocabulary(orsignature)ofAisafinitesetof
functions,eachofafixedarity.TheuniversesofAarethesetsonwhichthe
functionsofAact,e.g.anASMthataddstwointegerswillrequirethesetofall
integersasoneofitsuniverses.ThestateofAconsistsofanon-emptysetX(the
superuniverseofA),togetherwithinterpretationsofeveryfunctionnameinthe
signature.ThesuperuniverseofAdoesnotchange,buttheinterpretationsofthe
functionnamesmay.Thesuperuniversecontainsdistinctelementstrue,false,
undefthatletushaveBooleantests,andpartialfunctions(e.g.f(a)=undef).
Whilstthestructureaboveisusedtodefinethefunctionsusedandthesort
setsofanASMspecification,theyaregluedtogethertoformacompletespeci-
ficationusingrules[2].Theupdaterule(variableupdates),theconditionalrule
(conditionalstatementexecution)andtheblockrule(parallelstatementexecu-
tion)areproventobesucienttospecifyallsequentialalgorithms[10].
2.1DistributedASMs
DistributedASMs(DASMs)areanextensiontotheASMformalismforspecifi-
cationofmulti-agentcomputations[2].InthispaperDASMsareusedtomodel
thebehaviourofthecomputervirus’environment–theoperatingsystem.A
setModulesrepresentstheprogramsstoredinthefilestorereadytoberun.A
setAgentsrepresentsprocessesinmemory,whichrunaparticularmodule(pro-
gram).Agentsruninparallelwithoneanother.Theuserismodelledusinga
(non-deterministic)externalfunctionthatrunsprogramsrandomlybyassigning
modulestonewagents.Thiscouldbeimplementedeitherbyactualuserinput,
ormorelikely,byafunctionthatnon-deterministicallyselectsexecutablefiles
toberun.Whenaparticularagenthasreachedfixpoint,thatis,whenithas
ceasedtoupdatethestore,itisconsideredtohavefinisheditsexecutionrun
andterminated.TheoperatingsystemissimplythedistributedASMitself.The
agentsrunmodules,andrunconcurrentlywithoneanother.
2.2AnAbstractComputerVirus
AnASMfortheabstractcomputervirus,whichisdesignedtoencompassthe
entireclassofcomputerviruses,isasfollows.
Superuniverse,S
AV
=Agents[Modules[Rules[Boolean[{undef},where
AgentsisthesetofagentsthatarerunbythedistributedASM;Modulesisthe
setofmodules;andRulesisthesetofwell-formedrulesforASMs.
103
Vocabulary,
AV
Thefunctionsinthevocabularyaredefinedasfollows.
–Infected:Modules!Boolean.Returnstrueiamodulehasbeeninfected
withtheviralrule.Returnsfalseotherwise.
–Infect:Modules×Rules!P(Modules).Infectionbyacomputervirusis
amodificationtothesetModulesinthespecification,sothatthesetof
ASMrulescorrespondingtothevirusm
v
isexecutedby(atleast)onemore
modulethanwaspreviouslythecase.m
v
isreturnedbyThisProgram,and
addedtosomem2ModulesbyInfect.
–ThisProgram:!Rules.Returnstheviralrule.Thismodelsa“real-life”
functionthatcananalytically(orotherwise)generatetheviralcodeinthe
module,andreturnit.Apossibleimplementationofthiswouldbetodelimit
theviralcodewithinaninfectedprogramusingsomesequenceofbits(e.g.
fromanassemblylanguageperspective,anumberof
NOP
sstrungtogether),
whichtheviruscanlaterusetoderiveitsowncodewhenitcomestocopying
itforinfection.
–State:!{Done}[{undef}.Usedtoenforcesequentiality;initialvalueis
undef.
RulesThesetofrulescorrespondingtotheabstractvirusisasfollows.The
ASMblockrulespecifiesthatanygivenblockofstatementswillexecutein
parallel,thereforeanylistofruleswillexecuteinparallelunlesssequentiality
isenforcedusingguards.Sincethefollowingruleshouldexecuteonlyonceper
executionofthemoduleinwhichitresides,weensurethisthroughtheuseof
thenullaryfunctionState,whichissettoDoneonceasingleinfectionhastaken
place.
AbstractVirus=ifnot(State=Done)then
chooseminModulessatisfyingnot(Infected(m))
Modules:=Infect(m,ThisProgram)
Infected(m):=true
State:=Done
endchoose
endif
TheviralruleabovecopiesitselftoothermodulesinthedistributedASM.
Whenthemodified(infected)modulesarerun,theviralmodulefindsevenmore
modulestoinfect.
SpecificationofcomputervirusesisanewapplicationofASMs,andassuch
hasstrengthenedtheASMthesisthatanyalgorithmcanbemodelledatanatural
levelofabstractionbyanAbstractStateMachine[2].
Throughaprocessofrefinementitisstraightforwardtospecifymorespecific
virustypesbasedon,andconformingto,thedescriptionoftheabstractvirus.
[ Pobierz całość w formacie PDF ]
zanotowane.pldoc.pisz.plpdf.pisz.plhot-wife.htw.pl
|
|
| Cytat |
Dobry przykład - połowa kazania. Adalberg
I ty, Brutusie, przeciwko mnie?! (Et tu, Brute, contra me?! ) Cezar (Caius Iulius Caesar, ok. 101 - 44 p. n. e)
Do polowania na pchły i męża nie trzeba mieć karty myśliwskiej. Zygmunt Fijas
W ciepłym klimacie najłatwiej wyrastają zimni dranie.
Gdybym tylko wiedział, powinienem był zostać zegarmistrzem. - Albert Einstein (1879-1955) komentując swoją rolę w skonstruowaniu bomby atomowej
|
|
