skeleton.aslan++

specification @filename
channel_model CCM

entity Environment {
 

	types
		cookie < text;
		param < text;
		fnode < param;
		page < fnode;
		sess < text;
		nonce < text;

	symbols
		sqli_bypass, sqli, sqli_write, sqli_read, sqli_insert: param; 			%sql injection payload
		path_injection: param; 		%valid file
		xss: param; 		% XSS payload
		evil_file: fnode; 		%valid file
		honest, webapplication : agent;

		% Honest entity
		nonpublic hknows : message set;


		eq, emp : text;	% used as separator
		nonpublic sanitized(message) : message;

		nonpublic client_xss(message) : fact;


		%DBMS
		nonpublic db: message set;
		nonpublic query(message set,message): fact;
		nonpublic query_read(message) : fact;
		nonpublic query_write(message) : fact;
		nonpublic insert(message set,message): fact;
		nonpublic update(message set, message, message) : fact;
		nonpublic delete(message set, message) : fact;
		nonpublic inDB(message): fact;
		nonpublic inDB_write(message): fact;
		nonpublic inDB_read(message): fact;
		nonpublic inDB_bypass(message): fact;
		nonpublic inDB_insert(message) : fact;

	
		% database structure
		@databasestructure

		%Filesystem
		nonpublic fs: message set;
		nonpublic file(message) : message;
		nonpublic writeFile(message): fact;
		nonpublic readFile(message): fact;
		nonpublic inFS(message): fact;

		Result : message;

		% request 
		% page, parameters, cookie
		http_request(message, message, message): message;	

		% response
		% page, result
		http_response(message, message, message): message;	

		% none parameter
		none : text;

		@pages
		@params
		
		% messages tagss
		@tags

	clauses
		% database vulns
		db_hc_ev(M)  : inDB(M) :- M=sqli.?;

		db_hc_ev_write(M)  : inDB_write(M) :- M=sqli_write.?;

		db_hc_ev_read(M)  : inDB_read(M) :- M=sqli_read.?;

		db_hc_ev_bypass(M)  : inDB_bypass(M) :- M=sqli_bypass.?;

		db_hc_ev_insert(M)  : inDB_insert(M) :- M=sqli_insert.?;

		% client side vulns
		db_hc_ev_xss(M) : client_xss(M) :- M=xss.?;

		% file-system vulns
		fs_hc_ev(M)  : inFS(M) :- M=path_injection.?;

entity Session(Webapplication, Honest: agent) {

	entity Webapplication(Actor, Honest: agent) {
		symbols
		WebNonce : nonce;
		Entity : agent;
		@webappsymbols
		body{
			while(true){
				select{
					@webappbody
				}
			}%end while
		}%end body
	}


	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	% HONEST ENTITY
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  entity Honest(Actor, Webapplication : agent){
	
		symbols
			WebNonce : nonce;
			Page : page;
			Cookie : cookie;
			Params, Body : message;
			Tag : text;
			@webappsymbols
		
		body{
				while(true){
						select{
							@honestbody

								% This represent the intruder that sent a link to
								% the honest agent used for Reflected XSS but also for CSRF
								on( i *->* Actor : ?Page.?Params.?Tag ):{
									%assert o: Page !=  index | Params != u.s.xss.?.s.p.s.none | !hknows->contains(?) | Tag != tag1;
									%assert o: Page !=  insertPage | Params != comment.s.xss.insertPage | Tag != tag1;
									%assert h: exists M. hknows->contains(M) & cookieUsed(M);
									Cookie := ?;
									WebNonce := fresh();
									Actor *->* Webapplication : http_request(Page,Params,Cookie).Tag.WebNonce;
									Webapplication *->* Actor : http_response(?Page, ?Body, ?Cookie).Tag.WebNonce;
									hknows->add(Cookie);
									if(client_xss(Body)){
										Actor -> i : hknows;
									}
								}

						} %end select
				} %end while
		} % end body
 } % end entity
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	% END HONEST ENTITY
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	% DATABASE ENTITY
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	%TODO: fix SQLquery is just one message
	
	entity Database{
		symbols
			SQLquery, Key: message;
			File : fnode;
			Page : page;
			Sql, Val : message;
			Table : message set;
	
		body{
				while(true){
					select{
					% query behavior
					on(query(?Table, ?SQLquery)):{
						select{
							on(Table->contains(SQLquery) | (SQLquery=sanitized(?Sql) & Table->contains(?Sql))):{
								Result := SQLquery;
							}
							% malicious behavior
							on(inDB_bypass(SQLquery) & Table->contains(?Sql)):{
								Result := Sql;
							}
							on(inDB_read(SQLquery) & fs->contains(file(?File))):{
								Result := file(File);
							}
							on(inDB_write(SQLquery) & SQLquery = sqli_write.?File.?):{
								fs->add(file(File));
							}
							on(inDB_insert(SQLquery)):{
								Table->add(SQLquery);
							}
							on(inDB(SQLquery)):{
								Result := db;
							}
						}
						retract query(Table, SQLquery);
					}

					% query read behavior
					on(query_read(?SQLquery)):{
						select{
							on(fs->contains(file(SQLquery))):{
								Result := file(SQLquery);
							}
							% malicious behavior
							on(inDB_bypass(SQLquery) & Table->contains(?Sql)):{
								Result := Sql;
							}
							on(inDB_read(SQLquery) & fs->contains(file(?File))):{
								Result := file(File);
							}
							on(inDB_write(SQLquery) & SQLquery = sqli_write.?File.?):{
								fs->add(file(File));
							}
							on(inDB_insert(SQLquery)):{
								Table->add(SQLquery);
							}
							on(inDB(SQLquery)):{
								Result := db;
							}
						}
						retract query(Table, SQLquery);
					}

					% query write behavior
					on(query_write(?SQLquery)):{
						select{
							on(true):{
								fs->add(file(SQLquery));
							}
							% malicious behavior
							on(inDB_bypass(SQLquery) & Table->contains(?Sql)):{
								Result := Sql;
							}
							on(inDB_read(SQLquery) & fs->contains(file(?File))):{
								Result := file(File);
							}
							on(inDB_write(SQLquery) & SQLquery = sqli_write.?File.?):{
								fs->add(file(File));
							}
							on(inDB_insert(SQLquery)):{
								Table->add(SQLquery);
							}
							on(inDB(SQLquery)):{
								Result := db;
							}
						}
						retract query_write(SQLquery);
					}

					% query insert behavior
					on(insert(?Table, ?SQLquery)):{
						select{
							on(true):{
								Table->add(SQLquery);
							}
							% malicious behavior
							on(inDB_bypass(SQLquery) & Table->contains(?Sql)):{
								Result := Sql;
							}
							on(inDB_read(SQLquery) & fs->contains(file(?File))):{
								Result := file(File);
							}
							on(inDB_write(SQLquery) & SQLquery = sqli_write.?File.?):{
								fs->add(file(File));
							}
							on(inDB_insert(SQLquery)):{
								Table->add(SQLquery);
							}
							on(inDB(SQLquery)):{
								Result := db;
							}
						}
						retract insert(Table, SQLquery);
					}

					% query delete behavior
					on(delete(?Table, ?SQLquery)):{
						select{
							on(true):{
								Table->remove(SQLquery);
							}
							% malicious behavior
							on(inDB_bypass(SQLquery) & Table->contains(?Sql)):{
								Result := Sql;
							}
							on(inDB_read(SQLquery) & fs->contains(file(?File))):{
								Result := file(File);
							}
							on(inDB_write(SQLquery) & SQLquery = sqli_write.?File.?):{
								fs->add(file(File));
							}
							on(inDB_insert(SQLquery)):{
								Table->add(SQLquery);
							}
							on(inDB(SQLquery)):{
								Result := db;
							}
						}
						retract insert(Table, SQLquery);
					}
					% query update behavior
					on(update(?Table, ?Key, ?SQLquery)):{
						select{
							on(true):{
								Table->remove(Key);
								Table->add(SQLquery);
								Result := SQLquery;
							}
							% malicious behavior
							on(inDB_bypass(SQLquery) & Table->contains(?Sql)):{
								Result := Sql;
							}
							on(inDB_read(SQLquery) & fs->contains(file(?File))):{
								Result := file(File);
							}
							on(inDB_write(SQLquery) & SQLquery = sqli_write.?File.?):{
								fs->add(file(File));
							}
							on(inDB_insert(SQLquery)):{
								Table->add(SQLquery);
							}
							on(inDB(SQLquery)):{
								Result := db;
							}
						}
						retract update(Table, Key, SQLquery);
					}
				} %behavior select
		} %while 
	} %body
  }%dbEntity
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	% FILESYSTEM ENTITY
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	entity Filesystem{

			symbols
				Path ; message;
				Val: fnode;

			body{
				while(true){
					select{
						% begin honest behavior
						on(readFile(?Path) & fs->contains(file(?Path))):{
							Result := file(Path);
							retract readFile(Path);
						}
						on(writeFile(?Path)):{
								fs->add(file(Path));
								retract writeFile(Path);
						}
						% end honest behavior

						% begin dishonest behavior
						on(readFile(?Path) & inFS(?Path) & fs->contains(file(?Val))):{
							Result := file(Val);
							retract readFile(Path);
						}
						% end dishonest behavior
					} % select
				}%while
			}%body
	}%fs_entity
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


	body{ %of session

		@databaseinit
		new Webapplication(webapplication, honest); %, webapplication, database, filesystem);  
		new Database;
		new Filesystem;
		new Honest(honest, webapplication);
	}

	goals %of session 
		security_goal:
			[](!iknows(db));
}

body{ %of Environment
	new Session(webapplication, honest);
}

}