:- dynamic aa_node/1, aa_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, Prof, NewUid, NewGid, NewProf)
% (1) Uid/Gid changes, and the old Uid/Gid is not zero
% (2) Profile changes

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

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

privilege_enhancing(_, _, Prof, _, _, NewProf) :-
  Prof \== none,
  Prof \== NewProf.

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

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

%% if a profile has a certain file privilege
aa_file_privilege(none, _File, _Mode) :- !.

aa_file_privilege(Prof, File, read) :-
  aa_access_mode(Prof, Pattern, r(1), _, _, _, _, _, _),
  wildcard_match(Pattern, File), !.

aa_file_privilege(Prof, File, write) :-
  aa_access_mode(Prof, Pattern, _, w(1), _, _, _, _, _), 
  wildcard_match(Pattern, File), !.

aa_file_privilege(Prof, File, execute) :-
  aa_access_mode(Prof, Pattern, _, _, ux(1), _, _, _, _),
  wildcard_match(Pattern, File), !.

aa_file_privilege(Prof, File, execute) :-
  aa_access_mode(Prof, Pattern, _, _, _, px(1), _, _, _),
  wildcard_match(Pattern, File),
  aa_profile(File), !.

aa_file_privilege(Prof, File, execute) :-
  aa_access_mode(Prof, Pattern, _, _, _, _, ix(1), _, _),
  wildcard_match(Pattern, File).

%-------------------------------------------------
aa_has_capability(none, _Capability).

aa_has_capability(Profile, Capability) :-
  aa_capability(Profile, Capability).

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

% what is the new pro
aa_new_profile(none, Program, NewProf) :-
  aa_profile(Program), !,
  NewProf = Program.

aa_new_profile(none, _Program, NewProf) :-
  !, NewProf = none.

aa_new_profile(OldProf, Program, NewProf) :-
  aa_access_mode(OldProf, Pattern, _, _, ux(1), _, _, _, _),
  wildcard_match(Pattern, Program), !,
  NewProf = none.

aa_new_profile(OldProf, Program, NewProf) :-
  aa_access_mode(OldProf, Pattern, _, _, _, px(1), _, _, _),
  wildcard_match(Pattern, Program), !,
  NewProf = Program.

% the case of ix
aa_new_profile(OldProf, _Prog, NewProf) :-
  NewProf = OldProf.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
aa_program_profile(Program, Profile) :-
  aa_profile(Program), !,
  Profile = Program.

aa_program_profile(_Program, none).

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

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

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

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

%profile_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_capability(sys_module).

load_module_goal(proc(0, _Gid, Profile)) :-
  critical_capability(Cap),
  aa_has_capability(Profile, Cap).

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

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% aa_generate_graph generates all the nodes and edges in the graph
aa_generate_graph(InitPred, GoalPred) :-
  %% clear the scratch pad
  retractall(aa_node(_)),
  retractall(aa_edge(_, _, _)),
  uniq_assert(aa_node(init)),
  call(InitPred, Proc, [Program]),
  uniq_assert(aa_edge(init, Proc, exploit(Program, 1))),
  aa_generate_graph_node(Proc, GoalPred).

aa_generate_graph_node(Proc, _GoalPred) :-
  aa_node(Proc), !, fail.

aa_generate_graph_node(Proc, GoalPred) :-
  uniq_assert(aa_node(Proc)),
  write(assert_node(Proc)), nl,
  call(GoalPred, Proc),
  !, fail.

aa_generate_graph_node(proc(Uid, Gid, Profile), GoalPred) :-
  dac_can_execute(Uid, Gid, Program),
  aa_file_privilege(Profile, Program, execute),
  dac_execve(Uid, Gid, NewUid, NewGid, Program),
  aa_new_profile(Profile, Program, NewProfile),
  %
  privilege_enhancing(Uid, Gid, Profile, NewUid, NewGid, NewProfile),
  %
  dac_setid(Program, SetIdBit),
  uniq_assert(aa_edge(proc(Uid, Gid, Profile), proc(NewUid, NewGid, NewProfile), exec(Program, SetIdBit))),
  %
  aa_generate_graph_node(proc(NewUid, NewGid, NewProfile), GoalPred),
  fail.

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

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

  %%
  findall(aa_edge(X, Y, Z), aa_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([aa_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).

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

%% vulnerable files
vulnerable_executable('/bin/trojan_horse').
vulnerable_executable('/home/chen131/trojan_horse').

%% capabilities for network
net_capability(net_admin).
net_capability(net_raw).
net_capability(net_bind_service).

%% a daemon that opens to network
open_to_network(Profile) :-
  net_capability(Cap),
  aa_has_capability(Profile, Cap),
  !.

%% can create an executable program
create_executable(Profile, Program) :-
  aa_file_privilege(Profile, Program, write), !.

%% trojan profile: (1) open to network (2) can produce vulnerable exe
trojan_profile(Profile, Program) :-
  vulnerable_executable(Program),
  aa_profile(Profile),
  open_to_network(Profile),
  create_executable(Profile, Program).

