|
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) |
|
17 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
18 apply (tactic {*my_setiff_tac 1*}) |
|
19 apply (rule_tac x = obj in exI) |
|
20 apply (frule_tac obj = obj in co2sobj_other) |
|
21 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
30 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
31 apply (tactic {*my_setiff_tac 1*}) |
|
32 apply (rule_tac x = obj in exI) |
|
33 apply (frule_tac obj = obj in co2sobj_other) |
|
34 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
43 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
44 apply (tactic {*my_setiff_tac 1*}) |
|
45 apply (rule_tac x = obj in exI) |
|
46 apply (frule_tac obj = obj in co2sobj_other) |
|
47 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
56 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
57 apply (tactic {*my_setiff_tac 1*}) |
|
58 apply (rule_tac x = obj in exI) |
|
59 apply (frule_tac obj = obj in co2sobj_other) |
|
60 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
69 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
70 apply (tactic {*my_setiff_tac 1*}) |
|
71 apply (rule_tac x = obj in exI) |
|
72 apply (frule_tac obj = obj in co2sobj_other) |
|
73 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
82 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
83 apply (tactic {*my_setiff_tac 1*}) |
|
84 apply (rule_tac x = obj in exI) |
|
85 apply (frule_tac obj = obj in co2sobj_other) |
|
86 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
95 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
96 apply (tactic {*my_setiff_tac 1*}) |
|
97 apply (rule_tac x = obj in exI) |
|
98 apply (frule_tac obj = obj in co2sobj_other) |
|
99 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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) |
|
108 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
109 apply (tactic {*my_setiff_tac 1*}) |
|
110 apply (rule_tac x = obj in exI) |
|
111 apply (frule_tac obj = obj in co2sobj_other) |
|
112 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
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 |