selinux: S2ss_prop.thy@6884b3c9284b (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:
6884b3c9284b fix bug of static.thy for the static of recvmsg case chunhan parents: 32 diff changeset	12	"valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = s2ss s "