ďťż  
logo.png
ban.jpg
Saturday, April 5th, 2025 
  • zanotowane.pl
  • doc.pisz.pl
  • pdf.pisz.pl
  • efriends.pev.pl
    • « 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
    [ Pobierz całość w formacie PDF ]
    AlgebraicSpecicationofComputerViruses
    andTheirEnvironments
    MattWebster
    ?
    M.P.Webster@csc.liv.ac.uk
    DepartmentofComputerScience,UniversityofLiverpool,Liverpool,L697ZF,UK
    Abstract.Thispaperintroducesanapproachtoformalspecicationof
    computervirusesandtheirenvironmentsthroughthedevelopmentofal-
    gebraicspecificationsusingGurevich’sAbstractStateMachines(ASMs)
    andGoguen’sOBJ.DistributedASMsareusedtodevelopamodelof
    anabstractcomputervirus,whichthroughaprocessofrenementis
    convertedintomodelsofdierentvirustypes.Furtherrenementhas
    resultedinanexecutablespecication,writtenintheAbstractState
    MachineLanguage,AsmL.Themodelsstrengthenthethesisthatany
    algorithmcanbemodelledatanaturalabstractionlevelusinganAb-
    stractStateMachine.TheASMmodelscombinedwiththeAsmLex-
    ecutablespecicationprovideacomplementarytheoreticalandexperi-
    mentalframeworkforproofsandexperimentsoncomputervirusesand
    theirenvironments,aswellasausefulmeansofclassicationofdierent
    computervirusestypes.Nextwelookatadierentapproachtocomputer
    virusanalysisusingOBJ,whichisusedtospecifycomputerviruseswrit-
    teninanadhocprogramminglanguage,SPL.TheOBJspecicationis
    showntobeusefulforthedetectionofavirustypethatisparticularly
    diculttodetect–themetamorphiccomputervirus(MCV).Finally,the
    usefulnessofthetwospecicationsforreasoningaboutcomputerviruses
    isdiscussedandinthisregardthetwoformalismsarecompared.
    1Introduction
    Computervirusesare(oftenharmful)computerprogramsthatreplicateau-
    tonomouslythroughcomputerlesystems.Theyaretypicallydesignedtorepli-
    catewithouttheusers’consent,andareabletodamagedataorsoftwareon
    infectedmachines.Ingeneral,computervirusesreplicateusingthelegitimate
    infrastructureofanoperatingsystem(e.g.diskinput/outputroutines),and
    consequentlythespreadofcomputervirusesisdiculttopreventabsolutely
    withoutrestrictingtheoperatingsystem(OS)insomeway.
    Academicstudyofcomputervirusesbeganin1987,whenCohendenedan
    abstractcomputervirusandgaveaproofoftheundecidabilityofcomputervirus
    detection,provingthattherewouldbenodetection-basedpanaceaforthecom-
    putervirusproblem[1].Preventingcomputervirusesthroughtheuseofseverely
    ?
    WiththankstomysupervisorsGrantMalcolmandAlexeiLisitsa,forshowingme
    thepowerandbeautyofalgebraicspecication.
    100
    restrictedoperatingsystemsispossible,sincethecomputerviruscanonlywork
    bymodifyingstoredprogramsinmemorysothattheycontainacopyofthe
    virus.However,thecomputerarchitecturethatallowsprogramcreationand
    modificationisatthecoreoftheflexibilityandeciencyofmoderncomputers;
    forexample,nocompilercouldrunwithoutthecreationandmodicationof
    storedprograms.Thus,ndingacureforcomputervirusesbyrestrictingtheir
    environmentsisimpractical,andreliabledetectionisimpossible.Thereforethe
    ghttostopillicitcomputervirusesbecomesaquestionofoptimization,i.e.,
    “Howcanwebestprotectourselvesagainstcomputerviruses?”Inaddition,
    tractabilityisaprimaryconcernduetothetrade-obetweeneciencyand
    thoroughnessofanti-virus(AV)scanners.Withthisandthesustainedprolifera-
    tionofcomputervirusesinmind,generaltheoriesofcomputervirusesandtheir
    environmentswouldbeuseful.Formalspecicationofthebehaviourofdierent
    virustypescanprovideinsighttodevelopersofanti-virussoftwarebyhighlight-
    ingthecommonalitybetweendierentcomputerviruses,e.g.byencouragingthe
    reuseofdetectionanddisinfectionmethods.Knowledgeofwhichspecicdetails
    oftheimplementationofcomputersystemsaordsurvivalforvirusescanbede-
    rivedfromformalmodels,andcanbeusedtorestrictcomputervirusbehaviour
    throughthedevelopmentofsystemsthatareinherently(andprovably)more
    secure.
    Inthispaper,twoseparateapproachestocomputervirusformalisationare
    presented.In§2AbstractStateMachines[2]areusedtobuildaformalmodel
    ofanabstractcomputervirus,whichisrenedtoseveralmorespecicvirus
    types.AnexecutablespecicationinAsmL(basedontheASMmodels)isgiven,
    formingwiththeASMmodelsacomplementarytheoreticalandexperimental
    test-bedforformalproofsoncomputervirusesandtheirenvironments,aswell
    asaformalmeansofcomputerviruscategorisation.OBJ[3]isusedin§3to
    buildaformalframeworkforcomputervirologybasedonorder-sortedequational
    rewriting.Anadhocsimpleprogramminglanguage(SPL)isusedtoimplement
    computervirusesandexecutableles,andaformallanguagerepresentationof
    anoperatingsystemiscreated.In§3.3apromisingnewmeansofdetecting
    metamorphiccomputervirusesbasedontheOBJspecicationisdemonstrated.
    In§4itisshownhowtheseformalalgebraicspecicationsarereadilyapplicable
    tocomputervirusdetectiontechnologythroughtheapplicationofthedevelop-
    mentsmadeinMCVdetectionandcomputervirusclassication.
    1.1MetamorphicComputerViruses
    Theundecidabilityofcomputervirusdetectionisoneoftheoldestresultsin
    theeldofcomputervirology,butanti-virusscannershavetraditionallycom-
    pensatedforthisbyexploitingaweaknesscommontomanyna¨Ĺvecomputer
    viruses:constantsyntax.Thestringofbinarydigitscorrespondingtoaparticu-
    larcomputervirususuallyremainsunchangedfromonegenerationtothenext,
    asdoestheplacementofthecomputerviruswithintheinfectedexecutablele,
    e.g.oneparticularvirusmightbeplacedatthestartofanyexecutableitinfects.
    AVscannerswouldsearchexecutablefilesforvirus“signatures”–stringsofbits
    101
    thatcorrespondtoaparticularvirus–attheusualsitesofinfectionwithinexe-
    cutablesles.Thepresenceofasignaturewouldsignalthattheexecutablewas
    infected,andthatfurtherstepsneededtobetakentodisinfectthele.
    Inordertoavoiddetection,thewritersofcomputervirusesbegantodevelop
    waysofobfuscatingthesuspectviruscode.Oneattemptatthis,thepolymor-
    phiccomputervirus,whichchangesitssyntactic(binarydigit)representation
    usingencryption,failstoremainhiddenfromAVscannersonceitsmeansof
    decryptionhasbeendiscovered.Oncedecrypted,allgenerationsofpolymorphic
    computerviruseslookalike,andthesignature-basedapproachtodetectioncan
    beused.Amorepowerfulmeansofdetectionavoidanceisemployedbythemeta-
    morphiccomputervirus.Eachsuccessivegenerationofametamorphiccomputer
    virusmodiesthesyntax,butleavesthesemanticsunchanged.Inthiswaythe
    behaviourofeachsuccessivegenerationisthesame,butthevirusappearsto
    bedierent.Thus,itbecomesmuchmoredicultforanAVscannertodetect
    ametamorphiccomputervirususingasignature-basedapproach,anditisnot
    possibletokeeparecordofallpossiblegenerationsbecausethereareanun-
    limitednumber
    1
    .Inthiswaythemetamorphiccomputercansuccessfullyavoid
    detection[4].
    Thisproblemisnotconnedtoaparticularprogramminglanguage.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]thatreliableidenticationofaknown
    virusisnp-complete,andThimblebyetal[8]havedevelopedaformalismto
    describetrojansandcomputervirusinfection.Additionally,Lakhotia&Mo-
    hammed[9]havestudiedanapproachbasedonimposingorderonhigh-level
    languagestatementsinordertoreducethenumberofsyntacticvariantsand
    thereforeaidMCVdetection.
    1
    Programsizeis(theoretically)unlimited,soaninnitenumberofvariantsonasingle
    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
    approachtoalgebraicspecicationofsoftwaresystems,whereeachstepofan
    algorithmistreatedasaboundednumberofchangestoanalgebra,andthe
    wholealgorithmcanbedescribedusinganitenumberofsimpletransition
    rules.TheASMthesisstatesthatanyalgorithmcanbemodelledatanatural
    abstractionlevelusinganASM[2].
    Algebraically,anAbstractStateMachineisdenedasfollows.LetAbean
    AbstractStateMachine.Thevocabulary(orsignature)ofAisanitesetof
    functions,eachofaxedarity.TheuniversesofAarethesetsonwhichthe
    functionsofAact,e.g.anASMthataddstwointegerswillrequirethesetofall
    integersasoneofitsuniverses.ThestateofAconsistsofanon-emptysetX(the
    superuniverseofA),togetherwithinterpretationsofeveryfunctionnameinthe
    signature.ThesuperuniverseofAdoesnotchange,buttheinterpretationsofthe
    functionnamesmay.Thesuperuniversecontainsdistinctelementstrue,false,
    undefthatletushaveBooleantests,andpartialfunctions(e.g.f(a)=undef).
    Whilstthestructureaboveisusedtodenethefunctionsusedandthesort
    setsofanASMspecication,theyaregluedtogethertoformacompletespeci-
    cationusingrules[2].Theupdaterule(variableupdates),theconditionalrule
    (conditionalstatementexecution)andtheblockrule(parallelstatementexecu-
    tion)areproventobesucienttospecifyallsequentialalgorithms[10].
    2.1DistributedASMs
    DistributedASMs(DASMs)areanextensiontotheASMformalismforspeci-
    cationofmulti-agentcomputations[2].InthispaperDASMsareusedtomodel
    thebehaviourofthecomputervirus’environment–theoperatingsystem.A
    setModulesrepresentstheprogramsstoredinthelestorereadytoberun.A
    setAgentsrepresentsprocessesinmemory,whichrunaparticularmodule(pro-
    gram).Agentsruninparallelwithoneanother.Theuserismodelledusinga
    (non-deterministic)externalfunctionthatrunsprogramsrandomlybyassigning
    modulestonewagents.Thiscouldbeimplementedeitherbyactualuserinput,
    ormorelikely,byafunctionthatnon-deterministicallyselectsexecutableles
    toberun.Whenaparticularagenthasreachedxpoint,thatis,whenithas
    ceasedtoupdatethestore,itisconsideredtohavenisheditsexecutionrun
    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
    Thefunctionsinthevocabularyaredenedasfollows.
    –Infected:Modules!Boolean.Returnstrueiamodulehasbeeninfected
    withtheviralrule.Returnsfalseotherwise.
    –Infect:Modules×Rules!P(Modules).Infectionbyacomputervirusis
    amodicationtothesetModulesinthespecication,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
    ASMblockrulespeciesthatanygivenblockofstatementswillexecutein
    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.
    Whenthemodied(infected)modulesarerun,theviralmodulendsevenmore
    modulestoinfect.
    SpecicationofcomputervirusesisanewapplicationofASMs,andassuch
    hasstrengthenedtheASMthesisthatanyalgorithmcanbemodelledatanatural
    levelofabstractionbyanAbstractStateMachine[2].
    Throughaprocessofrenementitisstraightforwardtospecifymorespecic
    virustypesbasedon,andconformingto,thedescriptionoftheabstractvirus.
    [ Pobierz całość w formacie PDF ]
  • zanotowane.pl
  • doc.pisz.pl
  • pdf.pisz.pl
  • hot-wife.htw.pl
    		•
    « S E A R C H »


    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
    « C O P Y R I G H T   I N F O »
    © 2003 Ktoś, kto mĂłwi, Ĺźe nie zna się na sztuce, Ĺşle zna samego siebie.. Design by Templates For All.