selinux: Tainted_prop.thy@9b42765ce554 (annotated)

18 9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	1	theory Tainted_prop
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	2	imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	3	begin
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	4
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	5	context tainting begin
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	6
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	7	lemma tainted_in_current:
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	8	"\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	9	apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	10
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	11
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	12
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	13
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	14	end
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	15
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	16	end
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	17
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	18
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	19
9b42765ce554 info_flow did NOT guarantee in current_procs chunhan parents: diff changeset	20

author	chunhan
	Tue, 04 Jun 2013 15:51:02 +0800
changeset 18	9b42765ce554
child 19	ced0fcfbcf8e
permissions	-rw-r--r--