equal
deleted
inserted
replaced
1 theory Dynamic_static |
1 theory Dynamic_static |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
|
3 Temp |
3 begin |
4 begin |
4 |
5 |
5 context tainting_s begin |
6 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 |
7 |
30 |
8 |
31 |
9 |
32 |
10 |
33 |
11 |
52 "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s" |
30 "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s" |
53 |
31 |
54 lemma is_inited_eq_not_created: |
32 lemma is_inited_eq_not_created: |
55 "is_inited s obj = (\<not> is_created s obj)" |
33 "is_inited s obj = (\<not> is_created s obj)" |
56 by (auto simp:is_created_def is_inited_def) |
34 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 |
35 |
69 |
36 |
70 |
37 |
71 |
38 |
72 |
39 |
93 lemma many_sq_imp_sms: |
60 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" |
61 "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm" |
95 sorry |
62 sorry |
96 |
63 |
97 |
64 |
|
65 (* recorded in our static world *) |
|
66 fun recorded :: "t_object \<Rightarrow> bool" |
|
67 where |
|
68 "recorded (O_proc p) = True" |
|
69 | "recorded (O_file f) = True" |
|
70 | "recorded (O_dir f) = True" |
|
71 | "recorded (O_node n) = False" (* cause socket is temperary not considered *) |
|
72 | "recorded (O_shm h) = True" |
|
73 | "recorded (O_msgq q) = True" |
|
74 | "recorded _ = False" |
98 |
75 |
99 lemma enrichability: |
76 lemma enrichability: |
100 "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk> |
77 "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk> |
101 \<Longrightarrow> enrichable s objs" |
78 \<Longrightarrow> enrichable s objs" |
102 proof (induct s arbitrary:objs) |
79 proof (induct s arbitrary:objs) |