:- dynamic se_node/1, se_edge/3.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
uniq_assert(Fact) :-
  call(Fact), !, fail.

uniq_assert(Fact) :-
  assert(Fact).

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

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).

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

% 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(Uid, Gid, _, _, NewGid, _) :-
  Uid \== 0,
  Gid \== 0,
  Gid \== NewGid.

privilege_enhancing(_, _, Domain, _, _, NewDomain) :-
  Domain \== 'unconfined_t',
  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).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 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_typetrans(old_dom(Domain), new_dom(NewDomain), type(Type)),
    se_domain_privilege(domain(Domain), type(NewDomain), class(process), op(transition)),
	se_domain_privilege(domain(Domain), type(Type), class(_), op(entrypoint)),
    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_typetrans(old_dom(Domain), new_dom(NewDomain), type(Type)),
    se_domain_privilege(domain(Domain), type(NewDomain), class(process), op(transition)),
    !.

se_execve(Domain, Domain, _Type).

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

%-------------------------------------------------

policy_init(proc(0, 0, Domain), [foo]) :-
  se_domain(Domain),
  open_to_network(Domain).

%-------------------------------------------------

domain_init(proc(0, 0, ftpd_t), [foo]).

%-------------------------------------------------

target_init(proc(0, 0, X), [X]) :-
  se_domain(X),
  member(X, [httpd_t, ftpd_t, smbd_t, telnetd_t, unconfined_t]).

%-------------------------------------------------

local_init(proc(500, 500, unconfined_t), [none]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(Type) :-
  se_type(Type),
  file_info(path(_), type(regular), owner(0), _, _, _, oper(_,0,_), _, _, _, _, _, se_type(Type)).

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

%-------------------------------------------------

trojan_type(unconfined_home_t).
trojan_type(bin_t).

trojan_goal(proc(0, _Gid, Domain)) :-
  trojan_type(Type),
  create_executable(Domain, Type).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% se_generate_graph generates all the nodes and edges in the graph
se_generate_graph(InitPred, GoalPred) :-
  %% clear the scratch pad
  retractall(se_node(_)),
  retractall(se_edge(_, _, _)),
  uniq_assert(se_node(init)),
  call(InitPred, Proc, [Program]),
  uniq_assert(se_edge(init, Proc, exec(Program, 1))),
  se_generate_graph_node(Proc, GoalPred).

se_generate_graph_node(Proc, _GoalPred) :-
  se_node(Proc), !, fail.

se_generate_graph_node(Proc, GoalPred) :-
  uniq_assert(se_node(Proc)),
  write(assert_node(Proc)), nl,
  call(GoalPred, Proc),
  !, fail.

se_generate_graph_node(proc(Uid, Gid, Domain), GoalPred) :-
  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),
  uniq_assert(se_edge(proc(Uid, Gid, Domain), proc(NewUid, NewGid, NewDomain), exec(NewProgram, SetIdBit))),
  %
  se_generate_graph_node(proc(NewUid, NewGid, NewDomain), GoalPred),
  fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
write_graph(NodeFile, EdgeFile, InitPred, GoalPred) :-
  %%
  findall(Proc, se_node(Proc), Nodes),

  open(NodeFile, write, NodeFileId),
  tell(NodeFileId),
  write_node_list(Nodes, InitPred, GoalPred),
  close(NodeFileId),

  %%
  findall(se_edge(X, Y, Z), se_edge(X, Y, Z), Edges),

  open(EdgeFile, write, EdgeFileId),
  tell(EdgeFileId),
  write_edge_list(Edges, InitPred, GoalPred),
  close(EdgeFileId).

%-------------------------------------------------

write_node(Proc, _InitPred, GoalPred) :-
  call(GoalPred, Proc), !,
  writef('g_'),
  write(Proc).
 
write_node(Proc, InitPred, _GoalPred) :-
  call(InitPred, Proc, _), !,
  writef('i_'),
  write(Proc).

write_node(Proc, _InitPred, _GoalPred) :-
  write(Proc).

%-------------------------------------------------

write_node_list([], _, _).

write_node_list([H | _], InitPred, GoalPred) :-
  write_node(H, InitPred, GoalPred), nl, fail.

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

%-------------------------------------------------

write_edge_list([], _, _).

write_edge_list([se_edge(X,Y,Z) | _], InitPred, GoalPred) :-
  write_node(X, InitPred, GoalPred),
  writef('|'),
  write_node(Y, InitPred, GoalPred),
  writef('|'),
  write(Z),
  nl,
  fail.

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

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

se_analyze(InitPred, GoalPred) :-
  retractall(se_state_reachable(_, _)),
  call(InitPred, Proc, Programs),
  se_analyze_recursion(Proc, Programs, GoalPred).

se_analyze_recursion(Proc, Programs, GoalPred) :-
  se_state_reachable(Proc, SetOfPrograms), !,
  %% state already reachable
  check_exp_progs_improvement(Programs, SetOfPrograms, NewSetOfPrograms),
  %% Programs is an improvement
  retract(se_state_reachable(Proc, SetOfPrograms)),
  assert(se_state_reachable(Proc, NewSetOfPrograms)),
  explore_state(Proc, Programs, GoalPred).

%% This is when proc(..) is a new state
se_analyze_recursion(Proc, Programs, GoalPred) :-
  assert(se_state_reachable(Proc, [Programs])),
  explore_state(Proc, Programs, GoalPred).
  
explore_state(Proc, _Programs, GoalPred) :-
  call(GoalPred, Proc), !,
  fail.

explore_state(Proc, Programs, GoalPred) :-
  se_edge(Proc, NewProc, exec(NewProgram, SetIdBit)),
  new_exploit_list(Programs, NewProgram, SetIdBit, NewPrograms),
  se_analyze_recursion(NewProc, NewPrograms, GoalPred),
  fail.

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

new_exploit_list(Programs, NewProgram, 0, [exec(NewProgram) | Programs]).

new_exploit_list(Programs, NewProgram, 1, [exploit(NewProgram) | Programs]).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% if Programs is a superset of any list in SetOfPrograms
super_list(_L, []) :- !.

super_list([H | T2], [ H | T1]) :-
  !,
  super_list(T2, T1).

super_list([_ | T2], L1) :-
  super_list(T2, L1).

redundant_exp_list(Programs, [H | _]) :-
  super_list(Programs, H), !.

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) :-
  super_list(OldH, Programs), !,
  remove_redundant_exp_list(Programs, OldT, NewSet).

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 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 an 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_type(Type),
  vulnerable_exe_type(Type),
  write(type(Type)), nl,
  se_domain(Domain),
  open_to_network(Domain),
  create_executable(Domain, Type).

