Formal Affordance-based Models of Computer Virus Reproduction — Maude Specification

Matt Webster and Grant Malcolm

Instructions

To use the specification, save the specification below in a file called av.maude, execute Maude and type in av.
Maude Specification

*** av.maude - tested with:
*** Maude 2.3 built: Feb 14 2007 17:53:50.
*** Matt Webster, September-October 2007
*** A Maude specification of different anti-virus behaviour 
*** monitors, and how they classify viruses differently.

*** set up basic sorts for actions and events
fmod ACTION is 
	sorts Action .
endfm

fmod EVENT is
	sort Event .
endfm

*** set up views from trivial module so that we can have
*** lists and sets of these things
view Action from TRIV to ACTION	 is
	sort Elt to Action .
endv

view Event from TRIV to EVENT is 
	sort Elt to Event .
endv

*** Defines the library operations available to anti-virus software.
fmod AV-LIBRARY is
	*** parameterise the LIST module with Action and Event - 
	*** this gives us lists of Actions and Events
	pr LIST{Action} .
	pr LIST{Event} .

	sort Class .
	ops a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : -> Action .
	*** Anti-virus software can observe a virus executing,
	*** and then classify the resulting reproduction model. 
	op observe : List{Action} -> List{Event} .
	op classify : List{Event} -> Class .
	op Assisted : -> Class .
	op Unassisted : -> Class .

	vars S : Action .
	vars SL : List{Action} .
	var C : Event .
	var CL : List{Event} .
	
	eq observe( S SL ) = observe(S) observe(SL) .
	eq classify( nil ) = Unassisted .
	ceq classify( CL ) = Assisted 
		if CL =/= nil .
endfm

*** AV1 defines the behaviour monitoring capabilities of an antivirus program.
*** Calls to Windows Scripting Host are observable.
fmod AV1 is 
	pr AV-LIBRARY .

	ops CreateObject FindFolder GetFile ScriptName CopyFile : -> Event .
		
	eq observe( a1 ) = nil .
	eq observe( a2 ) = CreateObject .
	eq observe( a3 ) = FindFolder .	
	eq observe( a4 ) = GetFile ScriptName .
	eq observe( a5 ) = nil .	
	eq observe( a6 ) = CopyFile .	
endfm

*** baby virus: a1 a2 a3 a4 a5 a6
red observe( a1 a2 a3 a4 a5 a6 ) .
red classify( observe( a1 a2 a3 a4 a5 a6 ) ) .

*** AV2 defines the behaviour monitoring capabilities of an antivirus program.
*** Here, Baby is executed inside a sandbox.
fmod AV2 is 
	pr AV-LIBRARY .

	ops s1 s2 s3 s4 s5 s6 : -> Event .
	
	eq observe( a1 ) = s1 .
	eq observe( a2 ) = s2 .
	eq observe( a3 ) = s3 .	
	eq observe( a4 ) = s4 .
	eq observe( a5 ) = s5 .	
	eq observe( a6 ) = s6 .	
endfm

*** baby virus: a1 a2 a3 a4 a5 a6
red observe( a1 a2 a3 a4 a5 a6 ) .
red classify( observe( a1 a2 a3 a4 a5 a6 ) ) .

*** AV3 defines the behaviour monitoring capabilities of an antivirus program.
*** No events are observable for any action, i.e., behaviour monitoring is 
*** turned off.
fmod AV3 is 
	pr AV-LIBRARY .

	var A : Action .
	var LA : List{Action} .

	*** All lists of actions resulting in no events being detected
	eq observe( LA ) = nil .
endfm

*** baby virus: a1 a2 a3 a4 a5 a6

red observe( a1 a2 a3 a4 a5 a6 ) .
red classify( observe( a1 a2 a3 a4 a5 a6 ) ) .

*** AV4 defines the behaviour monitoring capabilities of an antivirus program.
*** Calls to FindFolder (afforded by WSH) are observable,
*** therefore WSH is a separate entity.
fmod AV4 is 
	pr AV-LIBRARY .

	op a3' : -> Action .

	ops CreateObject FindFolder GetFile ScriptName Copy : -> Event .
	
	eq observe( a1 ) = nil .
	eq observe( a2 ) = nil .
	eq observe( a3 ) = FindFolder .	
	eq observe( a3' ) = nil .		
	eq observe( a4 ) = nil .
	eq observe( a5 ) = nil .	
	eq observe( a6 ) = nil .	

endfm

*** Baby virus version 1
red observe( a1 a2 a3 a4 a5 a6 ) .
red classify( observe( a1 a2 a3 a4 a5 a6 ) ) .

*** Baby virus version 2
red observe( a1 a2 a3' a4 a5 a6 ) .
red classify( observe( a1 a2 a3' a4 a5 a6 ) ) .