diff -r f27ba31b7e96 -r 6f7b9039715f no_shm_selinux/S2ss_prop2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/no_shm_selinux/S2ss_prop2.thy	Tue Dec 17 13:30:21 2013 +0800
@@ -0,0 +1,123 @@
+(*<*)
+theory S2ss_prop2
+imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop S2ss_prop
+begin
+(*>*)
+
+context tainting_s begin
+
+(* should be modified when socket is model in static *)
+lemma s2ss_createsock:
+  "valid (CreateSock p af st fd inum # s) \<Longrightarrow> s2ss (CreateSock p af st fd inum # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+thm co2sobj_other
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_bind:
+  "valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_connect:
+  "valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_listen:
+  "valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_accept:
+  "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_send:
+  "valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_recv:
+  "valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_shutdown:
+  "valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s"
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_other)
+apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_other)
+apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+done
+
+lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
+  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
+  s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg
+  s2ss_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send 
+  s2ss_recv s2ss_shutdown
+
+end
+
+end
\ No newline at end of file