%:- table ifedac_attacker_control_process/4.
%:- table ifedac_attacker_control_step/3.
%:- table ifedac_execve/5.
%:- table ifedac_privilege_enhancing/8.

set_union(_, bot, bot).
set_union(bot, _, bot).
set_union([], X, X).

set_union([A|[]], X, X) :- member(A, X), !.
set_union([A|[]], X, [A|X]) :- !.

system_user(Uid) :- 
  Uid \== 500, Uid \== 501, Uid \== 502.
  
normal_user(Uid) :-
  Uid == 500.

normal_user(Uid) :-
  Uid == 501.

normal_user(Uid) :-
  Uid == 502.

ifedac_privilege_enhancing(Uid, _, _, _, NewUid, _, _, _) :-
  Uid \== 0,
  Uid \== NewUid.

ifedac_privilege_enhancing(Uid, Gid, _, _, _, NewGid, _, _) :-
  Uid \== 0,
  Gid \== 0,
  Gid \== NewGid.

ifedac_privilege_enhancing(_, _, Int, ExceptionDomain, _, _, _, NewExceptionDomain) :-
  Int \== [],
  ExceptionDomain \== NewExceptionDomain,
  NewExceptionDomain \== empty.
  
ifedac_wpc(File, []) :- 
	file_info(path(File), type(regular), owner(Uid), _, _, _, oper(_,0,_), _, _, _, _, _, _),
	system_user(Uid).

ifedac_wpc(File, [Uid]) :-
	file_info(path(File), type(regular), owner(Uid), _, _, _, oper(_,0,_), _, _, _, _, _, _),
	normal_user(Uid).

ifedac_wpc(File, bot) :-
	file_info(path(File), type(regular), _, _, _, _, oper(_,1,_), _, _, _, _, _, _).

ifedac_execve([], _, [], NewProgram, NewProgram) :-
	ifedac_wpc(NewProgram, []),
	ifedac_exception_system(NewProgram),
	!.

ifedac_execve([Uid], _, [Uid], NewProgram, NewProgram) :-
	ifedac_wpc(NewProgram, []),
	ifedac_exception_user(NewProgram),
	!.

ifedac_execve(Int, ExceptionDomain, Int, ExceptionDomain, NewProgram) :-
	ifedac_wpc(NewProgram, []),
	ifedac_exception_execve_inherit(ExceptionDomain, NewProgram),
	!.
	
ifedac_execve(Int, ExceptionDomain, Int, NewProgram, NewProgram) :-
	ifedac_wpc(NewProgram, []),
	ifedac_exception_execve(ExceptionDomain, NewProgram),
	!.

ifedac_execve(Int, _, NewInt, empty, NewProgram) :-
	ifedac_wpc(NewProgram, Wpc),
	set_union(Wpc, Int, NewInt).

net_init(net).

rootkit_goal(proc(Uid, _, Int, _)) :- 
  Uid == 0,
  Int == [].

rootkit_stop(proc(_, _, Int, _)) :- 
  Int \== [].

ifedac_analyze(InitPred, GoalPred, StopPred) :-
  call(InitPred, InitialState),
  ifedac_explore_state(InitialState, GoalPred, StopPred).

ifedac_explore_state(net, GoalPred, StopPred) :-
  assert(ifedac_control_process(net)),
  process_networking(Pid),
  ifedac_process_running(Pid, Uid, Gid, Program, Int, ExceptionDomain),
  ifedac_rap(ExceptionDomain),
  assert(ifedac_control_process_edge(proc(Uid, Gid, Int, ExceptionDomain), step(Program, 1), net)),
  ifedac_add_node(proc(Uid, Gid, Int, ExceptionDomain), GoalPred, StopPred),
  fail.

ifedac_explore_state(net, GoalPred, StopPred) :-
  assert(ifedac_control_process(net)),
  process_networking(Pid),
  ifedac_process_running(Pid, Uid, Gid, Program, Int, ExceptionDomain),
  set_union([net], Int, NewInt),
  assert(ifedac_control_process_edge(proc(Uid, Gid, NewInt, ExceptionDomain), step(Program, 1), net)),
  ifedac_add_node(proc(Uid, Gid, NewInt, ExceptionDomain), GoalPred, StopPred),
  fail.

ifedac_explore_state(proc(Uid, Gid, Int, ExceptionDomain), GoalPred, StopPred) :-
  assert(ifedac_control_process(proc(Uid, Gid, Int, ExceptionDomain))),
  dac_can_execute(Uid, Gid, NewProgram),
  dac_execve(Uid, Gid, NewUid, NewGid, NewProgram),
  ifedac_execve(Int, ExceptionDomain, NewInt, NewExceptionDomain, NewProgram),
  ifedac_privilege_enhancing(Uid, Gid, Int, ExceptionDomain, NewUid, NewGid, NewInt, NewExceptionDomain),
  dac_setid(NewProgram, SetIdBit),
  assert(ifedac_control_process_edge(proc(NewUid, NewGid, NewInt, NewExceptionDomain), step(NewProgram, SetIdBit), proc(Uid, Gid, Int, ExceptionDomain))), 
  ifedac_add_node(proc(NewUid, NewGid, NewInt, NewExceptionDomain), GoalPred, StopPred),
  fail.
  
ifedac_add_node(Proc, _, _) :-
  ifedac_control_process(Proc),
  !.
  
ifedac_add_node(Proc, GoalPred, _) :-
  call(GoalPred, Proc),
  assert(ifedac_control_process(Proc)), 
  !.
  
ifedac_add_node(Proc, _, StopPred) :-
  call(StopPred, Proc),
  !.
  
ifedac_add_node(Proc, _, _) :-
  ifedac_explore_state(Proc).

selinux_explore_state(net) :-
  assert(selinux_control_process(net)),
  process_networking(Pid),
  process_running(Pid, Uid, Gid, Program, _, _, Domain),
  assert(selinux_control_process_edge(proc(Uid, Gid, Domain), step(Program, 1), net)),
  selinux_add_node(proc(Uid, Gid, Domain)),
  fail.
  
selinux_explore_state(proc(Uid, Gid, Domain)) :-
  assert(selinux_control_process(proc(Uid, Gid, Domain))),
  se_can_execute(Domain, NewProgram, Type),
  dac_can_execute(Uid, Gid, NewProgram),
  se_execve(Domain, NewDomain, Type),
  dac_execve(Uid, Gid, NewUid, NewGid, NewProgram),
  privilege_enhancing(Uid, Gid, Domain, NewUid, NewGid, NewDomain),
  dac_setid(NewProgram, SetIdBit),
  assert(selinux_control_process_edge(proc(NewUid, NewGid, NewDomain), step(NewProgram, SetIdBit), proc(Uid, Gid, Domain))),
  selinux_add_node(proc(NewUid, NewGid, NewDomain)),
  fail.
  
selinux_add_node(Proc) :-
  selinux_control_process(Proc),
  !.
  
selinux_add_node(Proc) :-
  selinux_explore_state(Proc).

selinux_traverse_graph(X, VulList) :-
  assert(selinux_visited(X, VulList)),
  selinux_control_process(X),
  selinux_control_process_edge(Y, step(_, 0), X),
  selinux_visit(Y, VulList),
  fail.
  
selinux_traverse_graph(X, VulList) :-
  assert(selinux_visited(X, VulList)),
  selinux_control_process(X),
  selinux_control_process_edge(Y, step(Program, 1), X),
  member(Program, VulList),
  selinux_visit(Y, VulList),
  fail.
  
selinux_visit(Proc, VulList) :-
  selinux_visited(Proc, VulList),
  !.

selinux_visit(Proc, VulList) :-
  selinux_traverse_graph(Proc, VulList).

addProgram(Program, Set1, Set2) :-
  member(Program, Set1),
  Set2 = Set1,
  !.
  
addProgram(Program, Set1, [Program|Set1]).

ifedac_traverse_graph(X, VulSet) :-
  assert(ifedac_visited(X, VulSet)),
  ifedac_control_process(X),
  ifedac_control_process_edge(Y, step(_, 0), X),
  ifedac_visit(Y, VulSet),
  fail.
  
ifedac_traverse_graph(X, VulSet) :-
  assert(ifedac_visited(X, VulSet)),
  ifedac_control_process(X),
  ifedac_control_process_edge(Y, step(Program, 1), X),
  addProgram(Program, VulSet, NewVulSet),
  ifedac_visit(Y, NewVulSet),
  fail.
  
ifedac_visit(Proc, VulSet) :-
  ifedac_visited(Proc, OldVulSet),
  subset(VulSet, OldVulSet),
  assert(ifedac_visited(Proc, VulSet)),
  !.

ifedac_visit(Proc, VulSet) :-
  ifedac_traverse_graph(Proc, VulSet).

ifedac_goal(Proc, VulSet, GoalPred) :-
  ifedac_visited(Proc, VulSet),
  call(GoalPred, Proc),
  ifedac_minimal(Proc, VulSet).

ifedac_minimal(Proc, VulSet) :-
  ifedac_visited(Proc, OtherSet),
  VulSet \== OtherSet,
  subset(VulSet, OtherSet),
  !,
  fail.
    
ifedac_minimal(_, _).  