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

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

umip_privilege_enhancing(_, _, Int, ExceptionDomain, _, _, _, NewExceptionDomain) :-
  Int \== high,
  ExceptionDomain \== NewExceptionDomain,
  NewExceptionDomain \== empty.
  
umip_wpc(File, high) :- 
	file_info(path(File), type(regular), _, _, _, _, oper(_,0,_), _, _, _, _, _, _).

umip_wpc(File, low) :-
	file_info(path(File), type(regular), _, _, _, _, oper(_,1,_), _, _, _, _, _, _).
	
umip_execve(high, _, high, NewProgram, NewProgram) :-
	umip_wpc(NewProgram, high),
	umip_exception(NewProgram),
	!.

umip_execve(Int, ExceptionDomain, Int, ExceptionDomain, NewProgram) :-
	umip_wpc(NewProgram, high),
	umip_exception_execve_inherit(ExceptionDomain, NewProgram),
	!.
	
umip_execve(Int, ExceptionDomain, Int, NewProgram, NewProgram) :-
	umip_wpc(NewProgram, high),
	umip_exception_execve(ExceptionDomain, NewProgram),
	!.

umip_execve(high, _, high, empty, NewProgram) :-
	umip_wpc(NewProgram, high),
	!.

umip_execve(high, _, low, empty, NewProgram) :-
	umip_wpc(NewProgram, low),
	!.
	
umip_execve(low, _, low, empty, _).

net_init(net).

local_init(proc(500, 500, high, empty)).

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

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

umip_analyze(InitPred, GoalPred, StopPred) :-
  assert(umip_control_process(nothing)),
  call(InitPred, InitialState),
  umip_add_node(InitialState, GoalPred, StopPred).

umip_explore_state(net, GoalPred, StopPred) :-
  process_networking(Pid),
  umip_process_running(Pid, Uid, Gid, Program, high, ExceptionDomain),
  umip_rap(ExceptionDomain),
  assert(umip_control_process_edge(proc(Uid, Gid, high, ExceptionDomain), step(Program, 1), net)),
  umip_add_node(proc(Uid, Gid, high, ExceptionDomain), GoalPred, StopPred),
  fail.

umip_explore_state(net, GoalPred, StopPred) :-
  process_networking(Pid),
  umip_process_running(Pid, Uid, Gid, Program, _, ExceptionDomain),
  assert(ifedac_control_process_edge(proc(Uid, Gid, low, ExceptionDomain), step(Program, 1), net)),
  umip_add_node(proc(Uid, Gid, low, ExceptionDomain), GoalPred, StopPred),
  fail.

umip_explore_state(proc(Uid, Gid, Int, ExceptionDomain), GoalPred, StopPred) :-
  dac_can_execute(Uid, Gid, NewProgram),
  dac_execve(Uid, Gid, NewUid, NewGid, NewProgram),
  umip_execve(Int, ExceptionDomain, NewInt, NewExceptionDomain, NewProgram),
  umip_privilege_enhancing(Uid, Gid, Int, ExceptionDomain, NewUid, NewGid, NewInt, NewExceptionDomain),
  dac_setid(NewProgram, SetIdBit),
  assert(umip_control_process_edge(proc(NewUid, NewGid, NewInt, NewExceptionDomain), step(NewProgram, SetIdBit), proc(Uid, Gid, Int, ExceptionDomain))), 
  umip_add_node(proc(NewUid, NewGid, NewInt, NewExceptionDomain), GoalPred, StopPred),
  fail.
  
umip_add_node(Proc, _, _) :-
  umip_control_process(Proc),
  !.
  
umip_add_node(Proc, GoalPred, _) :-
  call(GoalPred, Proc),
  assert(umip_control_process(Proc)), 
  !.
  
umip_add_node(Proc, _, StopPred) :-
  call(StopPred, Proc),
  !.
  
umip_add_node(Proc, GoalPred, StopPred) :-
  assert(umip_control_process(Proc)),
  umip_explore_state(Proc, GoalPred, StopPred).

umip_generate_exploits(InitPred) :-
  assert(umip_visited(nothing, nothing)),
  call(InitPred, InitialState),
  umip_visit(InitialState, []).
  
addProgram(Program, Set1, Set2) :-
  member(Program, Set1),
  Set2 = Set1,
  !.
  
addProgram(Program, Set1, [Program|Set1]).

umip_traverse_graph(X, VulSet) :-
  umip_control_process(X),
  umip_control_process_edge(Y, step(_, 0), X),
  umip_visit(Y, VulSet),
  fail.
  
umip_traverse_graph(X, VulSet) :-
  umip_control_process(X),
  umip_control_process_edge(Y, step(Program, 1), X),
  addProgram(Program, VulSet, NewVulSet),
  umip_visit(Y, NewVulSet),
  fail.

umip_visit(Proc, VulSet) :-
  umip_visited(Proc, VulSet),
  !.
  
umip_visit(Proc, VulSet) :-
  umip_visited(Proc, OldVulSet),
  subset(OldVulSet, VulSet),
  assert(umip_visited(Proc, VulSet)),
  !.

umip_visit(Proc, VulSet) :-
  assert(umip_visited(Proc, VulSet)),
  umip_traverse_graph(Proc, VulSet).

umip_goal(Proc, VulSet, GoalPred) :-
  umip_visited(Proc, VulSet),
  call(GoalPred, Proc),
  umip_minimal(Proc, VulSet).

umip_minimal(Proc, VulSet) :-
  umip_visited(Proc, OtherSet),
  VulSet \== OtherSet,
  subset(OtherSet, VulSet),
  !,
  fail.
    
umip_minimal(_, _).
