selinux: S2ss_prop.thy@e7f850d1e08e (annotated)

32 705e1e41faf7 add event-trace simpset for s2ss chunhan parents: diff changeset	1	(<)
705e1e41faf7 add event-trace simpset for s2ss chunhan parents: diff changeset	2	theory S2ss_prop
705e1e41faf7 add event-trace simpset for s2ss chunhan parents: diff changeset	3	imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop
705e1e41faf7 add event-trace simpset for s2ss chunhan parents: diff changeset	4	begin
705e1e41faf7 add event-trace simpset for s2ss chunhan parents: diff changeset	5	(>)
705e1e41faf7 add event-trace simpset for s2ss chunhan parents: diff changeset	6
33 6884b3c9284b fix bug of static.thy for the static of recvmsg case chunhan parents: 32 diff changeset	7	context tainting_s begin
6884b3c9284b fix bug of static.thy for the static of recvmsg case chunhan parents: 32 diff changeset	8
6884b3c9284b fix bug of static.thy for the static of recvmsg case chunhan parents: 32 diff changeset	9	(* simpset for s2ss*)
6884b3c9284b fix bug of static.thy for the static of recvmsg case chunhan parents: 32 diff changeset	10
6884b3c9284b fix bug of static.thy for the static of recvmsg case chunhan parents: 32 diff changeset	11	lemma s2ss_execve:
34 e7f850d1e08e remove O_msg from co2sobj/init_obj2sobj chunhan parents: 33 diff changeset	12	"valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
e7f850d1e08e remove O_msg from co2sobj/init_obj2sobj chunhan parents: 33 diff changeset	13	if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
e7f850d1e08e remove O_msg from co2sobj/init_obj2sobj chunhan parents: 33 diff changeset	14	then (case (cp2sproc (Execve p f fds # s) s2ss s \<union> {} "

author	chunhan
	Thu, 29 Aug 2013 13:29:32 +0800
changeset 34	e7f850d1e08e
parent 33	6884b3c9284b
child 35	f2e620d799cf
permissions	-rw-r--r--