|
1 theory Dynamic_static |
|
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
|
3 begin |
|
4 |
|
5 context tainting_s begin |
|
6 |
|
7 definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100) |
|
8 where |
|
9 "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss" |
|
10 |
|
11 lemma [simp]: "ss \<doteq> ss" |
|
12 by (auto simp:init_ss_eq_def) |
|
13 |
|
14 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101) |
|
15 where |
|
16 "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'" |
|
17 |
|
18 lemma s2ss_included_sobj: |
|
19 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
|
20 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
|
21 |
|
22 lemma init_ss_in_prop: |
|
23 "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk> |
|
24 \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss" |
|
25 apply (simp add:init_ss_in_def init_ss_eq_def) |
|
26 apply (erule bexE, erule conjE) |
|
27 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj) |
|
28 done |
|
29 |
|
30 |
|
31 |
|
32 |
|
33 |
|
34 definition enrich:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool" |
|
35 where |
|
36 "enrich s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. obj' \<notin> objs \<and> alive s' obj \<and> co2sobj s' obj' = co2sobj s' obj" |
|
37 |
|
38 definition reserve:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool" |
|
39 where |
|
40 "reserve s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj" |
|
41 |
|
42 definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool" |
|
43 where |
|
44 "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enrich s objs s' \<and> reserve s objs s'" |
|
45 |
|
46 definition is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool" |
|
47 where |
|
48 "is_created s obj \<equiv> init_alive obj \<longrightarrow> deleted obj s" |
|
49 |
|
50 definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool" |
|
51 where |
|
52 "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s" |
|
53 |
|
54 lemma is_inited_eq_not_created: |
|
55 "is_inited s obj = (\<not> is_created s obj)" |
|
56 by (auto simp:is_created_def is_inited_def) |
|
57 |
|
58 (* recorded in our static world *) |
|
59 fun recorded :: "t_object \<Rightarrow> bool" |
|
60 where |
|
61 "recorded (O_proc p) = True" |
|
62 | "recorded (O_file f) = True" |
|
63 | "recorded (O_dir f) = True" |
|
64 | "recorded (O_node n) = False" (* cause socket is temperary not considered *) |
|
65 | "recorded (O_shm h) = True" |
|
66 | "recorded (O_msgq q) = True" |
|
67 | "recorded _ = False" |
|
68 |
|
69 |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 lemma d2s_main_execve: |
|
75 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static" |
|
76 apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve) |
|
77 sorry |
|
78 |
|
79 lemma d2s_main: |
|
80 "valid s \<Longrightarrow> s2ss s \<propto> static" |
|
81 apply (induct s, simp add:s2ss_nil_prop init_ss_in_def) |
|
82 apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init) |
|
83 apply (frule vd_cons, frule vt_grant_os, simp) |
|
84 apply (case_tac a) |
|
85 apply (clarsimp simp add:s2ss_execve) |
|
86 apply (rule conjI, rule impI) |
|
87 |
|
88 |
|
89 |
|
90 sorry |
|
91 |
|
92 |
|
93 lemma many_sq_imp_sms: |
|
94 "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm" |
|
95 sorry |
|
96 |
|
97 |
|
98 |
|
99 lemma enrichability: |
|
100 "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk> |
|
101 \<Longrightarrow> enrichable s objs" |
|
102 proof (induct s arbitrary:objs) |
|
103 case Nil |
|
104 hence "objs = {}" |
|
105 apply (auto simp:is_created_def) |
|
106 apply (erule_tac x = x in ballE) |
|
107 apply (auto simp:init_alive_prop) |
|
108 done |
|
109 thus ?case using Nil unfolding enrichable_def enrich_def reserve_def |
|
110 by (rule_tac x = "[]" in exI, auto) |
|
111 next |
|
112 case (Cons e s) |
|
113 hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj \<Longrightarrow> enrichable s objs" |
|
114 and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj" |
|
115 and os: "os_grant s e" and se: "grant s e" and vd: "valid s" |
|
116 by (auto dest:vt_grant_os vd_cons vt_grant) |
|
117 show ?case sorry (* |
|
118 proof (cases e) |
|
119 case (Execve p f fds) |
|
120 hence p4: "e = Execve p f fds" by simp |
|
121 from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs" |
|
122 by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"]) |
|
123 show "enrichable (e # s) objs" |
|
124 proof (case "is_inited s (O_proc p)") |
|
125 apply (simp add:enrichable_def p4) |
|
126 |
|
127 |
|
128 |
|
129 apply auto |
|
130 apply (auto simp:enrichable_def) |
|
131 apply (induct s) |
|
132 |
|
133 |
|
134 |
|
135 done |
|
136 *) |
|
137 qed |
|
138 |
|
139 lemma s2d_main: |
|
140 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
|
141 apply (erule static.induct) |
|
142 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
|
143 |
|
144 apply (erule exE|erule conjE)+ |
|
145 |
|
146 apply (simp add:update_ss_def) |
|
147 |
|
148 sorry |
|
149 |
|
150 |
|
151 end |
|
152 |
|
153 end |