Mercurial Mercurial > hg > selinux / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
S2ss_prop2.thy
changeset 60 03d173288afe
parent 59 89770d3c8a9b 
--- a/S2ss_prop2.thy	Wed Oct 16 13:38:31 2013 +0800
+++ b/S2ss_prop2.thy	Wed Oct 16 14:43:28 2013 +0800
@@ -332,12 +332,117 @@
 done
 
 
+(* 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)
+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_createshm s2ss_detach s2ss_deleteshm s2ss_attach
-
+  s2ss_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send 
+  s2ss_recv s2ss_shutdown
 
 end
selinux