|
77
|
1 |
(*<*)
|
|
|
2 |
theory S2ss_prop2
|
|
|
3 |
imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop S2ss_prop
|
|
|
4 |
begin
|
|
|
5 |
(*>*)
|
|
|
6 |
|
|
|
7 |
context tainting_s begin
|
|
|
8 |
|
|
|
9 |
(* should be modified when socket is model in static *)
|
|
|
10 |
lemma s2ss_createsock:
|
|
|
11 |
"valid (CreateSock p af st fd inum # s) \<Longrightarrow> s2ss (CreateSock p af st fd inum # s) = s2ss s"
|
|
|
12 |
apply (simp add:s2ss_def)
|
|
|
13 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
14 |
apply (rule_tac x = obj in exI)
|
|
|
15 |
thm co2sobj_other
|
|
|
16 |
apply (simp add:co2sobj_other)
|
|
92
|
17 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
18 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
19 |
apply (rule_tac x = obj in exI)
|
|
|
20 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
21 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
22 |
done
|
|
|
23 |
|
|
|
24 |
lemma s2ss_bind:
|
|
|
25 |
"valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s"
|
|
|
26 |
apply (simp add:s2ss_def)
|
|
|
27 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
28 |
apply (rule_tac x = obj in exI)
|
|
|
29 |
apply (simp add:co2sobj_other)
|
|
92
|
30 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
31 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
32 |
apply (rule_tac x = obj in exI)
|
|
|
33 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
34 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
35 |
done
|
|
|
36 |
|
|
|
37 |
lemma s2ss_connect:
|
|
|
38 |
"valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s"
|
|
|
39 |
apply (simp add:s2ss_def)
|
|
|
40 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
41 |
apply (rule_tac x = obj in exI)
|
|
|
42 |
apply (simp add:co2sobj_other)
|
|
92
|
43 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
44 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
45 |
apply (rule_tac x = obj in exI)
|
|
|
46 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
47 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
48 |
done
|
|
|
49 |
|
|
|
50 |
lemma s2ss_listen:
|
|
|
51 |
"valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s"
|
|
|
52 |
apply (simp add:s2ss_def)
|
|
|
53 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
54 |
apply (rule_tac x = obj in exI)
|
|
|
55 |
apply (simp add:co2sobj_other)
|
|
92
|
56 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
57 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
58 |
apply (rule_tac x = obj in exI)
|
|
|
59 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
60 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
61 |
done
|
|
|
62 |
|
|
|
63 |
lemma s2ss_accept:
|
|
|
64 |
"valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s"
|
|
|
65 |
apply (simp add:s2ss_def)
|
|
|
66 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
67 |
apply (rule_tac x = obj in exI)
|
|
|
68 |
apply (simp add:co2sobj_other)
|
|
92
|
69 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
70 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
71 |
apply (rule_tac x = obj in exI)
|
|
|
72 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
73 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
74 |
done
|
|
|
75 |
|
|
|
76 |
lemma s2ss_send:
|
|
|
77 |
"valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s"
|
|
|
78 |
apply (simp add:s2ss_def)
|
|
|
79 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
80 |
apply (rule_tac x = obj in exI)
|
|
|
81 |
apply (simp add:co2sobj_other)
|
|
92
|
82 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
83 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
84 |
apply (rule_tac x = obj in exI)
|
|
|
85 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
86 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
87 |
done
|
|
|
88 |
|
|
|
89 |
lemma s2ss_recv:
|
|
|
90 |
"valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s"
|
|
|
91 |
apply (simp add:s2ss_def)
|
|
|
92 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
93 |
apply (rule_tac x = obj in exI)
|
|
|
94 |
apply (simp add:co2sobj_other)
|
|
92
|
95 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
96 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
97 |
apply (rule_tac x = obj in exI)
|
|
|
98 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
99 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
100 |
done
|
|
|
101 |
|
|
|
102 |
lemma s2ss_shutdown:
|
|
|
103 |
"valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s"
|
|
|
104 |
apply (simp add:s2ss_def)
|
|
|
105 |
apply (tactic {*my_seteq_tac 1*})
|
|
|
106 |
apply (rule_tac x = obj in exI)
|
|
|
107 |
apply (simp add:co2sobj_other)
|
|
92
|
108 |
apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
109 |
apply (tactic {*my_setiff_tac 1*})
|
|
|
110 |
apply (rule_tac x = obj in exI)
|
|
|
111 |
apply (frule_tac obj = obj in co2sobj_other)
|
|
92
|
112 |
apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
|
|
77
|
113 |
done
|
|
|
114 |
|
|
|
115 |
lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
|
|
|
116 |
s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
|
|
|
117 |
s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg
|
|
|
118 |
s2ss_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send
|
|
|
119 |
s2ss_recv s2ss_shutdown
|
|
|
120 |
|
|
|
121 |
end
|
|
|
122 |
|
|
|
123 |
end |