:- dynamic se_node/1, se_edge/3.
:- dynamic se_file_type_represent/2, se_represent_prog/2, se_similar_prog/2.
:- dynamic se_memo_trojan2_succeed/1, se_memo_trojan2_fail/1.

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

uniq_assert(Fact) :-
  assert(Fact).

%-------------------------------------------------
uniq_assert_true(Fact) :-
  call(Fact), !.

uniq_assert_true(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(Uid, Gid, FUid, FGid, AccessMode, Upers, Gpers, Opers)
% 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, FileType, Mode) :-
  file_info(path(Program), type(FileType), 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, regular, 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).
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 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).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Domain and Type are instantiated
se_can_execute_type(Domain, Type, NewDomain) :-
    se_typetrans(old_dom(Domain), new_dom(NewDomain), type(Type)),
	!,
    se_domain_privilege(domain(Domain), type(Type), class(file), op(execute)),
    se_domain_privilege(domain(Domain), type(NewDomain), class(process), op(transition)),
	se_domain_privilege(domain(NewDomain), type(Type), class(file), op(entrypoint)).

se_can_execute_type(Domain, Type, NewDomain) :-
    se_domain_privilege(domain(Domain), type(Type), class(file), op(execute)),
    se_domain_privilege(domain(Domain), type(Type), class(file), op(execute_no_trans)),
	NewDomain = Domain.

%% Domain is instantiated
se_can_execute_prog(Domain, Program, NewDomain) :-
    se_file_type_represent(Program, Type),
    se_can_execute_type(Domain, Type, NewDomain).
%	write(searched(Type,Program, Domain, NewDomain)), nl.

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

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

local_init(proc(Uid, Gid, unconfined_t), none) :-
  user_info(chen131, Uid, Gid).

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

ppp_init(proc(0, 0, pppd_t), none).

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

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

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

%% 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_type(unconfined_home_t).
trojan_type(bin_t).

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

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

se_proc_write_folder(Domain, Type, NewType) :-
  se_file_creation(domain(Domain), folder_type(Type), newfile_class(file), newfile_type(NewType)),
  !,
  se_domain_privilege(domain(Domain), type(Type), class(dir), op(write)),
  se_domain_privilege(domain(Domain), type(NewType), class(file), op(write)).
  
se_proc_write_folder(Domain, Type, NewType) :-
  se_domain_privilege(domain(Domain), type(Type), class(dir), op(write)),
  se_domain_privilege(domain(Domain), type(Type), class(file), op(write)),
  NewType = Type,
  !.

%% Uid, Gid, Domain should all be instantiated, Folder and ExeFileType not instantiated
se_proc_can_trojan2(proc(Uid, Gid, Domain), Folder, ExeFileType) :-
  %% there exist a folder
  file_info(path(Folder), type(dir), owner(Fuid), group(Fgid), Uper, Gper, Oper, _, _, _, _, _, se_type(Type)),
  %% the process can write to this folder (plant a file) by DAC
  dac_can_access_solid(Uid, Gid, Fuid, Fgid, write, Uper, Gper, Oper),
  %% the process can write to this folder by SELinux policy
  se_proc_write_folder(Domain, Type, ExeFileType),
  %% a normal user can execute the file
  se_can_execute_type(unconfined_t, ExeFileType, unconfined_t).
  
%-------------------------------------------------

trojan2_goal(Proc) :-
  se_memo_trojan2_succeed(Proc),
  !.

trojan2_goal(Proc) :-
  se_memo_trojan2_fail(Proc),
  !, fail.

trojan2_goal(Proc) :-
  se_proc_can_trojan2(Proc, _, _),
  !,
  assert(se_memo_trojan2_succeed(Proc)).

trojan2_goal(Proc) :-
  assert(se_memo_trojan2_fail(Proc)),
  fail.

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

ppp_goal(proc(_, _, postfix_smtp_t)).
ppp_goal(proc(_, _, postfix_cleanup_t)).
ppp_goal(proc(_, _, mailman_mail_t)).
ppp_goal(proc(_, _, procmail_t)).
ppp_goal(proc(_, _, postfix_showq_t)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% generate represent list
add_file_represent_list(path(Program), FileType, Owner, Group, Uper, Gper, Oper, SUid, SGid, Sticky, SEUser, SERole, SEType) :-
	FileProperty = file_property(FileType, Owner, Group, Uper, Gper, Oper, SUid, SGid, Sticky, SEUser, SERole, SEType),
	se_represent_prog(FileProperty, Rprog),
	!,
	uniq_assert(se_similar_prog(Rprog, Program)).

add_file_represent_list(path(Program), FileType, Owner, Group, Uper, Gper, Oper, SUid, SGid, Sticky, SEUser, SERole, SEType) :-
	FileProperty = file_property(FileType, Owner, Group, Uper, Gper, Oper, SUid, SGid, Sticky, SEUser, SERole, SEType),
	assert(se_represent_prog(FileProperty, Program)),
	SEType = se_type(Type),
	assert(se_file_type_represent(Program, Type)),
	assert(se_similar_prog(Program, Program)).

do_generate_represent_list :-
	file_info(Path, FileType, Owner, Group, Uper, Gper, Oper, SUid, SGid, Sticky, SEUser, SERole, SEType),
	add_file_represent_list(Path, FileType, Owner, Group, Uper, Gper, Oper, SUid, SGid, Sticky, SEUser, SERole, SEType),
	fail.

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

generate_represent_list :-
	retractall(se_file_type_represent(_,_)),
	retractall(se_represent_prog(_,_)),
	retractall(se_similar_prog(_,_)),
	do_generate_represent_list.

generate_represent_list.

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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% se_generate_graph generates all the nodes and edges in the graph
se_generate_graph(InitPred, GoalPred) :-
  %% generate represent list
  generate_represent_list,
  %% clear the scratch pad
  retractall(se_node(_)),
  retractall(se_edge(_, _, _)),
  retractall(se_memo_trojan2_succeed(_)),
  retractall(se_memo_trojan2_fail(_)),
  uniq_assert(se_node(init)),
  call(InitPred, Proc, Program),
  uniq_assert(se_edge(init, Proc, Program)),
  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_prog(Domain, NewProgram, NewDomain),
  dac_can_execute(Uid, Gid, NewProgram),
  dac_execve(Uid, Gid, NewUid, NewGid, NewProgram),
  %
  privilege_enhancing(Uid, Gid, Domain, NewUid, NewGid, NewDomain),
  %
  uniq_assert(se_edge(proc(Uid, Gid, Domain), proc(NewUid, NewGid, NewDomain), NewProgram)),
  %
  se_generate_graph_node(proc(NewUid, NewGid, NewDomain), GoalPred),
  fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% policy only predicates

po_net_init(Domain, Program) :-
  process_networking(Pid),
  process_running(Pid, _Uid, _Gid, Program, _, _, Domain).

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

po_local_init(unconfined_t, none).

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

po_load_module_goal(Domain) :-
  se_domain_privilege(domain(Domain), _, class(capability), op(sys_module)).

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

po_trojan_goal(Domain) :-
  trojan_type(Type),
  create_executable(Domain, Type).

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

se_po_generate_graph(InitPred, GoalPred) :-
  %% generate represent list
  generate_represent_list,
  %% clear the scratch pad
  retractall(se_node(_)),
  retractall(se_edge(_, _, _)),
  uniq_assert(se_node(init)),
  call(InitPred, Domain, Program),
  uniq_assert(se_edge(init, Domain, Program)),
  se_po_generate_graph_node(Domain, GoalPred).

se_po_generate_graph_node(Domain, _GoalPred) :-
  se_node(Domain), !, fail.

se_po_generate_graph_node(Domain, GoalPred) :-
  uniq_assert(se_node(Domain)),
  write(po_assert_node(Domain)), nl,
  call(GoalPred, Domain),
  !, fail.

se_po_generate_graph_node(Domain, GoalPred) :-
  se_can_execute_prog(Domain, NewProgram, NewDomain),
  Domain \== NewDomain,
  uniq_assert(se_edge(Domain, NewDomain, NewProgram)),
  se_po_generate_graph_node(NewDomain, GoalPred).

%-------------------------------------------------
%% DAC only predicates

daco_net_init(proc(Uid, Gid), Program) :-
  process_networking(Pid),
  process_running(Pid, Uid, Gid, Program, _, _, _).

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

daco_local_init(proc(Uid, Gid), none) :-
  user_info(chen131, Uid, Gid).

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

daco_load_module_goal(proc(0, _Gid)).

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

daco_trojan_goal(proc(Uid, Gid)) :-
  dac_can_access(Uid, Gid, '/bin', dir, write), !.

daco_trojan_goal(proc(Uid, Gid)) :-
  dac_can_access(Uid, Gid, '/home/chen131', dir, write).

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

se_daco_generate_graph(InitPred, GoalPred) :-
  %% generate represent list
  generate_represent_list,
  %% 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, Program)),
  se_daco_generate_graph_node(Proc, GoalPred).

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

se_daco_generate_graph_node(Proc, GoalPred) :-
  uniq_assert(se_node(Proc)),
  write(daco_assert_node(Proc)), nl,
  call(GoalPred, Proc),
  !, fail.

se_daco_generate_graph_node(proc(Uid, Gid), GoalPred) :-
  se_file_type_represent(NewProgram, _Type), 
  dac_can_execute(Uid, Gid, NewProgram),
  dac_execve(Uid, Gid, NewUid, NewGid, NewProgram),
  proc(Uid, Gid) \== proc(NewUid, NewGid),
  uniq_assert(se_edge(proc(Uid, Gid), proc(NewUid, NewGid), NewProgram)),
  se_daco_generate_graph_node(proc(NewUid, NewGid), GoalPred),
  fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
write_graph(EdgeFile, GoalPred) :-
  %%
  findall(se_edge(X, Y, Z), se_edge(X, Y, Z), Edges),

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

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

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

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

write_edge_list([], _).

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

write_edge_list([_ | T], GoalPred) :-
  write_edge_list(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)),
  !.

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% selinux policy inconsistency
se_no_trans_vector(OldDom, NewDom, Type) :-
    se_domain_privilege(domain(OldDom), type(Type), _, op(execute)),
    se_domain_privilege(domain(OldDom), type(NewDom), class(process), op(transition)),
	se_domain_privilege(domain(NewDom), type(Type), class(_), op(entrypoint)),
	!, fail.

se_no_trans_vector(_OldDom, _NewDom, _Type).

se_incon(OldDom, NewDom, Type) :-
  se_typetrans(old_dom(OldDom), new_dom(NewDom), type(Type)),
  se_no_trans_vector(OldDom, NewDom, Type).

