%:- table attacker_control_process/3, se_file_type/2.
%:- table se_can_execute/3.
%:- table se_domain_can_change/4, dac_execve/5.
%:- table attacker_control_step/3.
%:- table dac_setid/2.

:- dynamic se_state_reachable/2.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% dac rules

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

member(X, [_|T]) :- member(X, T).

uid_in_group(Uid, Gid) :-
  user_info(_, Uid, Gid).

uid_in_group(Uid, Gid) :-
  user_info(User, Uid, _), 
  group_info(_, Gid, Group),
  member(User, Group).

perm_set(read, 1, _, _) :- !.
perm_set(write, _, 1, _) :- !.
perm_set(execute, _, _, 1).

perm_not_set(read, 0, _, _) :- !.
perm_not_set(write, _, 0, _) :- !.
perm_not_set(execute, _, _, 0).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% dac_can_access_solid is called only when all the parameters are instantiated
dac_can_access_solid(0, _, _, _, _, _, _, _) :- !.

dac_can_access_solid(Uid, _, Uid, _, Mode, uper(R, W, X), _, _) :-
  !, perm_set(Mode, R, W, X).

dac_can_access_solid(_, Gid, _, Gid, Mode, _, gper(R, W, X), _) :-
  !, perm_set(Mode, R, W, X).

dac_can_access_solid(Uid, _, _, Fgid, Mode, _, gper(R, W, X), _) :-
  uid_in_group(Uid, Fgid), !,
  perm_set(Mode, R, W, X).
  
dac_can_access_solid(_, _, _, _, Mode, _, _, oper(R, W, X)) :-
  perm_set(Mode, R, W, X).

dac_can_access(Uid, Gid, Program, Mode) :-
  file_info(path(Program), type(regular), owner(Fuid), group(Fgid), Uper, Gper, Oper, _, _, _, _, _, _),
  dac_can_access_solid(Uid, Gid, Fuid, Fgid, Mode, Uper, Gper, Oper).

dac_can_execute(Uid, Gid, Program) :-
  dac_can_access(Uid, Gid, Program, execute).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% check whether the new state has more privileges
% privilege_enhancing(Uid, Gid, Domain, NewUid, NewGid, NewDomain)
% (1) Uid/Gid changes, and the old Uid/Gid is not zero
% (2) Domain changes

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

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

privilege_enhancing(_, _, Domain, _, _, NewDomain) :-
  Domain \== NewDomain.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% update DAC portion of process state for executing a program

dac_execve(OUid, OGid, NUid, NGid, Program) :-
  file_info(path(Program), type(regular), owner(Owner), group(Group), _, _, _, setuid(SU), setgid(SG), _, _, _, _),
  dac_setuid(SU, Owner, OUid, NUid),
  dac_setgid(SG, Group, OGid, NGid).

%% setuid bit not set
dac_setuid(0, _, OUid, OUid).

%% setuid bit set
dac_setuid(1, Owner, _, Owner).

%% setgid bit not set
dac_setgid(0, _, OGid, OGid).

%% setgid bit set
dac_setgid(1, Group, _, Group).
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% whether the program has a setuid/setgid bit
dac_setid(Program, 1) :-
  file_info(path(Program), type(regular), _, _, _, _, _, setuid(1), _, _, _, _, _).

dac_setid(Program, 1) :-
  file_info(path(Program), type(regular), _, _, _, _, _, _, setgid(1), _, _, _, _).

dac_setid(Program, 0) :-
  file_info(path(Program), type(regular), _, _, _, _, _, setuid(0), setgid(0), _, _, _, _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% selinux file label type
se_file_type(Program, Type) :-
  file_info(path(Program), _, _, _, _, _, _, _, _, _, _, _, se_type(Type)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% if a domain has certain privileges
se_domain_privilege(domain(Domain), type(Type), class(Class), op(Op)) :-
    dom_priv(Domain, Type, Class, OpList),
    member(Op, OpList).

%% is there program to cause domain change 
se_domain_can_change(Domain, NewDomain, Type, Program) :-
    se_entrypoint(old_dom(Domain), new_dom(NewDomain), type(Type)),
    se_domain_privilege(domain(Domain), type(NewDomain), class(process), op(transition)),
    se_file_type(Program, Type).

se_can_execute(Domain, Program, Type) :-
    se_file_type(Program, Type),
    se_domain_privilege(domain(Domain), type(Type), class(file), op(execute)).


% What happens when Domain executes Program 
se_execve(Domain, NewDomain, Type) :- 
    se_entrypoint(old_dom(Domain), new_dom(NewDomain), type(Type)),
    se_domain_privilege(domain(Domain), type(NewDomain), class(process), op(transition)),
    !.

se_execve(Domain, Domain, _Type).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% here is how we define a state controlled by attacker
%attacker_control_process(Uid, Gid, Domain) :-
%  attacker_control_step(_, proc(Uid,Gid,Domain), _).

%% compromising a network daemon program
%attacker_control_step_ps(net, proc(Uid,Gid,Domain), action(Program, 1)) :-
%  process_networking(Pid),
%  process_running(Pid, Uid, Gid, Program, _, _, Domain).
%
%attacker_control_step(net, Proc, Action) :-
%  attacker_control_step_ps(net, Proc, Action).

%% Load a new setuid root program
%% or,
%% Load an ordinary program, considering only those causing domain transitions
%attacker_control_step(proc(Uid,Gid,Domain), proc(NewUid,NewGid,NewDomain), action(NewProgram, SetIdBit)) :-
%  attacker_control_process(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).

%se_analyze(net, GoalPred) :- 
%  !,
%  process_networking(Pid),
%  process_running(Pid, Uid, Gid, Program, _, _, Domain),
%  se_analyze_recursion(proc(Uid, Gid, Domain), [Program]).

net_init(proc(Uid,Gid,Domain), [Program]) :-
  process_networking(Pid),
  process_running(Pid, Uid, Gid, Program, _, _, Domain).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
critical_cap_op(sys_module).

load_module_goal(proc(0, _Gid, Domain)) :-
  critical_cap_op(Op),
  se_domain_privilege(domain(Domain), _, class(capability), op(Op)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
critical_file_type_solid(Type) :-
  file_info(path(_), type(regular), owner(0), _, _, _, oper(_,0,_), _, _, _, _, _, se_type(Type)).

critical_file_type(Type) :-
  se_type(Type),
  critical_file_type_solid(Type).

write_critical_file_goal(proc(0, _Gid, Domain)) :-
  critical_file_type(Type),
  se_domain_privilege(domain(Domain), type(Type), class(file), op(write)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
se_analyze(InitPred, GoalPred) :-
  %% clear the scratch pad
  retractall(se_state_reachable(_,_)),
  findall(state(Proc, Programs), call(InitPred, Proc, Programs), Bag),
  %% call(InitPred, proc(Uid,Gid,Domain), Programs),
  se_analyze_start(Bag, GoalPred).

se_analyze_start([], _GoalPred).

se_analyze_start([state(proc(Uid,Gid,Domain), Programs) | _], GoalPred) :-
%  write(se_analyze_start(proc(Uid,Gid,Domain), Programs)), nl,
  se_analyze_recursion(proc(Uid,Gid,Domain), Programs, GoalPred), fail.
%  se_analyze_start(T, GoalPred),
%  write(se_analyze_over), nl.

se_analyze_start([_ | T], GoalPred) :-
  se_analyze_start(T, GoalPred).

se_analyze_recursion(proc(Uid,Gid,Domain), Programs, GoalPred) :-
  %% 
  se_state_reachable(proc(Uid,Gid,Domain), SetOfPrograms), !,
%  write(analyze1(proc(Uid,Gid,Domain), Programs)), nl,
  %% state already reachable
  check_exp_progs_improvement(Programs, SetOfPrograms, NewSetOfPrograms),
  %% Programs is an improvement
  retract(se_state_reachable(proc(Uid,Gid,Domain), SetOfPrograms)),
  assert(se_state_reachable(proc(Uid,Gid,Domain), NewSetOfPrograms)),
  explore_state(proc(Uid,Gid,Domain), Programs, GoalPred).

%% This is when proc(..) is a new state
se_analyze_recursion(proc(Uid,Gid,Domain), Programs, GoalPred) :-
%  write(analyze2(proc(Uid,Gid,Domain), Programs)), nl,
  assert(se_state_reachable(proc(Uid,Gid,Domain), [Programs])),
  explore_state(proc(Uid,Gid,Domain), Programs, GoalPred).
  
explore_state(proc(Uid,Gid,Domain), Programs, GoalPred) :-
  call(GoalPred, proc(Uid, Gid, Domain)), !,
  write(find_succeed_state_____(proc(Uid,Gid,Domain), Programs)), nl,
  fail.

explore_state(proc(Uid,Gid,Domain), Programs, GoalPred) :-
  se_can_execute(Domain, NewProgram, Type),
%  write(explore1(proc(Uid,Gid,Domain), NewProgram, Type)), nl,
  dac_can_execute(Uid, Gid, NewProgram),
  se_execve(Domain, NewDomain, Type),
  dac_execve(Uid, Gid, NewUid, NewGid, NewProgram),
%  write(explore2(proc(Uid,Gid,Domain),newproc(NewUid,NewGid,NewDomain),Programs,NewProgram)), nl,
%
  privilege_enhancing(Uid, Gid, Domain, NewUid, NewGid, NewDomain),
%  write(explore3(proc(Uid,Gid,Domain),newproc(NewUid,NewGid,NewDomain),Programs,NewProgram)), nl,
  dac_setid(NewProgram, SetIdBit),
%  write(explore4(SetIdBit)), nl,
  new_exploit_list(Programs, NewProgram, SetIdBit, NewPrograms),
%  write(explore5(NewPrograms)), nl,
%
  se_analyze_recursion(proc(NewUid,NewGid,NewDomain), NewPrograms, GoalPred),
  fail.

  %% Perhaps use sorted set, to make some of the operationgs faster.

new_exploit_list(Programs, _NewProgram, 0, Programs).
%
new_exploit_list(Programs, NewProgram, 1, [NewProgram | Programs]).


%% if Programs is a superset of any list in SetOfPrograms
redundant_exp_list(Programs, [H | _]) :-
  subset(H, Programs), !.

redundant_exp_list(Programs, [_ | T]) :-
  redundant_exp_list(Programs, T).

%% if no list in SetOfPrograms is a subset of Programs, insert Programs
check_exp_progs_improvement(Programs, SetOfPrograms, _NewSet) :-
  redundant_exp_list(Programs, SetOfPrograms), !, fail.

check_exp_progs_improvement(Programs, SetOfPrograms, NewSetOfPrograms) :-
  remove_redundant_exp_list(Programs, SetOfPrograms, CurrSet),
  NewSetOfPrograms = [Programs | CurrSet].

%% remove any list that is a superset of programs
remove_redundant_exp_list(_, [], []).

remove_redundant_exp_list(Programs, [OldH | OldT], NewSet) :-
  subset(Programs, OldH), !,
  remove_redundant_exp_list(Programs, OldT, NewT),
  NewSet = NewT.

remove_redundant_exp_list(Programs, [OldH | OldT], NewSet) :-
  remove_redundant_exp_list(Programs, OldT, NewT),
  NewSet = [OldH | NewT].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
write_reachable_states(StateFile, SucStateFile, GoalPred) :-
  findall(state(Proc, SetOfPrograms), se_state_reachable(Proc, SetOfPrograms), Bag),

  open(StateFile, write, Myfile1),
  tell(Myfile1),
  write_states_in_bag(Bag, true_goal),
  close(Myfile1),
  
  open(SucStateFile, write, Myfile2),
  tell(Myfile2),
  write_states_in_bag(Bag, GoalPred),
  close(Myfile2).

true_goal(_).

write_states_in_bag([], _).

write_states_in_bag([state(Proc, SetOfPrograms) | _], GoalPred) :-
  call(GoalPred, Proc),
  write(state(Proc, SetOfPrograms)), nl, fail.

write_states_in_bag([_ | T], GoalPred) :-
  write_states_in_bag(T, GoalPred).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% analyze the policy

%% vulnerable exe type: if executed, may enter a unconfined domain
vulnerable_exe_type(Type) :-
  se_domain_privilege(domain(unconfined_t), type(Type), class(file), op(execute)),
  se_execve(unconfined_t, unconfined_t, Type),
  !.

%% sockets that listen to the real network (excluding internal sockets)
real_socket(rawip_socket).
real_socket(tcp_socket).
real_socket(udp_socket).

%% a domain that opens to network
open_to_network(Domain) :-
  real_socket(Socket),
  se_domain_privilege(domain(Domain), _, class(Socket), op(read)),
  !.

%% can create a executable type
create_executable(Domain, Type) :-
  se_domain_privilege(domain(Domain), type(Type), class(_), op(create)),
  se_domain_privilege(domain(Domain), type(Type), class(_), op(setattr)),
  !.

%% trojan domain: (1) open to network (2) can produce vulnerable exe
trojan_domain(Domain, Type) :-
  se_domain(Domain),
  open_to_network(Domain),
  se_type(Type),
  vulnerable_exe_type(Type),
  create_executable(Domain, Type).

