author | chunhan |
Mon, 02 Dec 2013 10:52:40 +0800 | |
changeset 74 | 271e9818b6f6 |
permissions | -rw-r--r-- |
74
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
1 |
(*<*) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
2 |
theory S2ss_prop2 |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
3 |
imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop S2ss_prop |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
4 |
begin |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
5 |
(*>*) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
6 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
7 |
context tainting_s begin |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
8 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
9 |
definition unbackuped_sprocs :: "t_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_sobject set" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
10 |
where |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
11 |
"unbackuped_sprocs s e procs \<equiv> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
12 |
{sp | p sp. p \<in> procs \<and> co2sobj s (O_proc p) = Some sp \<and> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
13 |
(\<forall> p' \<in> procs. co2sobj (e # s) (O_proc p') \<noteq> Some sp) \<and> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
14 |
(\<forall> p' \<in> (current_procs s - procs). co2sobj s (O_proc p') \<noteq> Some sp)}" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
15 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
16 |
definition update_s2ss_procs :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_static_state" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
17 |
where |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
18 |
"update_s2ss_procs s ss e procs \<equiv> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
19 |
ss \<union> {sp | p sp. p \<in> procs \<and> co2sobj (e # s) (O_proc p) = Some sp} |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
20 |
- unbackuped_sprocs s e procs" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
21 |
(* new sp after event may exists as same before the event in procs *) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
22 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
23 |
lemma unbked_sps_D: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
24 |
"\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<in> procs\<rbrakk> \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
25 |
by (auto simp add:unbackuped_sprocs_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
26 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
27 |
lemma unbked_sps_D': |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
28 |
"\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<notin> procs; p \<in> current_procs s; |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
29 |
co2sobj (e # s) (O_proc p) = co2sobj s (O_proc p)\<rbrakk> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
30 |
\<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
31 |
by (auto simp:unbackuped_sprocs_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
32 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
33 |
lemma not_unbked_sps_D: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
34 |
"\<lbrakk>x \<notin> unbackuped_sprocs s e procs; p \<in> procs; co2sobj s (O_proc p) = Some x\<rbrakk> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
35 |
\<Longrightarrow> (\<exists> p' \<in> procs. co2sobj (e # s) (O_proc p') = Some x) \<or> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
36 |
(\<exists> p' \<in> current_procs s - procs. co2sobj s (O_proc p') = Some x)" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
37 |
by (auto simp:unbackuped_sprocs_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
38 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
39 |
lemma unbked_sps_I: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
40 |
"\<lbrakk>co2sobj s obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> unbackuped_sprocs s' e procs" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
41 |
apply (case_tac obj) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
42 |
apply (auto simp add:unbackuped_sprocs_def co2sobj.simps split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
43 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
44 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
45 |
lemma co2sobj_proc_deleteshm: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
46 |
"\<lbrakk>valid (DeleteShM p h # s); \<forall>flag. (pa, flag) \<notin> procs_of_shm s h; pa \<in> current_procs s\<rbrakk> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
47 |
\<Longrightarrow> co2sobj (DeleteShM p h # s) (O_proc pa) = co2sobj s (O_proc pa)" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
48 |
thm co2sobj_deleteshm |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
49 |
apply (frule_tac obj = "O_proc pa" in co2sobj_deleteshm, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
50 |
apply (frule vd_cons, frule_tac p = pa in current_proc_has_sp, simp, erule exE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
51 |
apply (auto dest!:current_proc_has_sp' current_has_sec' current_shm_has_sh' |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
52 |
split:t_object.splits option.splits if_splits dest:flag_of_proc_shm_prop1 |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
53 |
simp:co2sobj.simps tainted_eq_Tainted cp2sproc_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
54 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
55 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
56 |
lemma s2ss_deleteshm: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
57 |
"valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s) = |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
58 |
(case ch2sshm s h of |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
59 |
Some sh \<Rightarrow> del_s2ss_obj s |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
60 |
(update_s2ss_procs s (s2ss s) (DeleteShM p h) {p'| p' flag. (p', flag) \<in> procs_of_shm s h}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
61 |
(O_shm h) (S_shm sh) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
62 |
| _ \<Rightarrow> {})" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
63 |
apply (frule vt_grant_os, frule vd_cons) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
64 |
apply (case_tac "ch2sshm s h") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
65 |
apply (drule current_shm_has_sh', simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
66 |
apply (simp add:del_s2ss_obj_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
67 |
apply (tactic {*my_clarify_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
68 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
69 |
unfolding update_s2ss_procs_def |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
70 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
71 |
apply (erule_tac obj = obj in co2sobj_some_caseD) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
72 |
apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
73 |
apply (erule exE, rule DiffI, rule UnI2, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
74 |
apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
75 |
apply (rule notI, drule_tac p = pa in unbked_sps_D, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
76 |
apply (rule_tac x = flag in exI, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
77 |
apply (rule DiffI, rule UnI1, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
78 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
79 |
apply (simp add:cp2sproc_deleteshm split:option.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
80 |
apply (simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
81 |
apply (drule current_has_sec', simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
82 |
apply (simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
83 |
apply (drule flag_of_proc_shm_prop1, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
84 |
apply (drule flag_of_proc_shm_prop1, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
85 |
apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
86 |
apply (simp add:co2sobj_proc_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
87 |
apply (simp add:co2sobj_proc_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
88 |
apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
89 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
90 |
apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
91 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
92 |
apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
93 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
94 |
apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
95 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
96 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
97 |
apply (erule DiffE, erule UnE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
98 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
99 |
apply (erule_tac obj = obj in co2sobj_some_caseD) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
100 |
apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
101 |
apply (drule_tac p = pa in not_unbked_sps_D, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
102 |
apply (rule_tac x = flag in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
103 |
apply (simp, erule disjE, clarsimp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
104 |
apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
105 |
apply (erule bexE, simp, (erule conjE)+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
106 |
apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
107 |
apply (rule_tac x = "O_proc p'" in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
108 |
apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
109 |
apply (rule_tac x = "O_proc pa" in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
110 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
111 |
apply (frule_tac co2sobj_sshm_imp, erule exE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
112 |
apply (case_tac "ha = h") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
113 |
apply (rule_tac x = obj' in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
114 |
apply (simp add:co2sobj.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
115 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
116 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
117 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
118 |
apply (tactic {*my_setiff_tac 1*}, clarsimp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
119 |
apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
120 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
121 |
apply (tactic {*my_clarify_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
122 |
unfolding update_s2ss_procs_def |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
123 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
124 |
apply (erule_tac obj = obj in co2sobj_some_caseD) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
125 |
apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
126 |
apply (erule exE, rule DiffI, rule DiffI, rule UnI2, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
127 |
apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
128 |
apply (rule notI, drule_tac p = pa in unbked_sps_D, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
129 |
apply (rule_tac x = flag in exI, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
130 |
apply (rule notI, simp add:co2sobj.simps split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
131 |
apply (rule DiffI, rule DiffI, rule UnI1, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
132 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
133 |
apply (simp add:cp2sproc_deleteshm split:option.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
134 |
apply (simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
135 |
apply (drule current_has_sec', simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
136 |
apply (simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
137 |
apply (drule flag_of_proc_shm_prop1, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
138 |
apply (drule flag_of_proc_shm_prop1, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
139 |
apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
140 |
apply (simp add:co2sobj_proc_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
141 |
apply (simp add:co2sobj_proc_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
142 |
apply (rule notI, simp add:co2sobj.simps split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
143 |
apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
144 |
apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
145 |
apply (case_tac "ha = h", simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
146 |
apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
147 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
148 |
apply (rule notI, simp add:co2sobj_deleteshm, erule_tac x = "O_shm ha" in allE, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
149 |
apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
150 |
apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
151 |
apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
152 |
apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
153 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
154 |
apply (erule DiffE, erule DiffE, erule UnE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
155 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
156 |
apply (erule_tac obj = obj in co2sobj_some_caseD) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
157 |
apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
158 |
apply (drule_tac p = pa in not_unbked_sps_D, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
159 |
apply (rule_tac x = flag in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
160 |
apply (simp, erule disjE, clarsimp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
161 |
apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
162 |
apply (erule bexE, simp, (erule conjE)+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
163 |
apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
164 |
apply (rule_tac x = "O_proc p'" in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
165 |
apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
166 |
apply (rule_tac x = "O_proc pa" in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
167 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
168 |
apply (case_tac "ha = h", simp add:co2sobj.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
169 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
170 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
171 |
apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
172 |
apply (tactic {*my_setiff_tac 1*}, clarsimp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
173 |
apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
174 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
175 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
176 |
lemma s2ss_detach: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
177 |
"valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = ( |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
178 |
case (cp2sproc s p, cp2sproc (Detach p h # s) p) of |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
179 |
(Some sp, Some sp') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
180 |
(S_proc sp (O_proc p \<in> Tainted s)) (S_proc sp' (O_proc p \<in> Tainted s)) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
181 |
| _ \<Rightarrow> {} )" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
182 |
apply (frule vd_cons, frule vt_grant_os) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
183 |
apply (case_tac "cp2sproc s p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
184 |
apply (drule current_proc_has_sp', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
185 |
apply (case_tac "cp2sproc (Detach p h # s) p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
186 |
apply (drule current_proc_has_sp', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
187 |
apply (erule exE|erule conjE)+ |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
188 |
apply (simp add:update_s2ss_obj_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
189 |
apply (tactic {*my_clarify_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
190 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
191 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
192 |
apply (case_tac "obj = O_proc p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
193 |
apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
194 |
apply (rule disjI2, simp, rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
195 |
apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
196 |
apply (simp add:is_file_simps is_dir_simps split:t_object.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
197 |
apply (simp add:co2sobj.simps, simp add:co2sobj.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
198 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
199 |
apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
200 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
201 |
apply (case_tac "obj = O_proc p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
202 |
apply (rule_tac x = obj' in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
203 |
apply (frule_tac obj = obj' in co2sobj_detach, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
204 |
apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
205 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
206 |
apply (simp add:co2sobj_detach) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
207 |
apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
208 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
209 |
apply (tactic {*my_clarify_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
210 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
211 |
apply (case_tac "obj = O_proc p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
212 |
apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
213 |
apply (rule disjI2, rule DiffI, simp, rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
214 |
apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
215 |
apply (simp add:is_file_simps is_dir_simps split:t_object.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
216 |
apply (simp add:co2sobj.simps, simp add:co2sobj.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
217 |
apply (rule notI, simp, erule_tac x = obj in allE, erule impE, simp add:alive_simps, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
218 |
apply (frule_tac obj = obj in co2sobj_detach) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
219 |
apply (simp add:alive_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
220 |
apply (simp split:t_object.splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
221 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
222 |
apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
223 |
apply (tactic {*my_setiff_tac 1*}, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
224 |
apply (case_tac "obj = O_proc p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
225 |
apply (simp add:co2sobj.simps tainted_eq_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
226 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
227 |
apply (simp add:co2sobj_detach) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
228 |
apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
229 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
230 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
231 |
definition attach_Tainted_procs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag \<Rightarrow> t_process set" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
232 |
where |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
233 |
"attach_Tainted_procs s p h flag \<equiv> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
234 |
(if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
235 |
then {p''. \<exists> p' flag'. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p'' \<and> |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
236 |
O_proc p'' \<notin> Tainted s} |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
237 |
else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
238 |
then {p'. info_flow_shm s p p' \<and> O_proc p' \<notin> Tainted s} |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
239 |
else {})" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
240 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
241 |
lemma attach_Tainted_procs_prop1: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
242 |
"valid s \<Longrightarrow> Tainted (Attach p h flag # s) = Tainted s \<union> {O_proc p' | p'. p' \<in> attach_Tainted_procs s p h flag}" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
243 |
apply (auto simp:attach_Tainted_procs_def intro:info_flow_shm_Tainted) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
244 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
245 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
246 |
lemma attach_Tainted_procs_prop2: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
247 |
"valid (Attach p h flag # s) \<Longrightarrow> {O_proc p'| p'. p' \<in> attach_Tainted_procs s p h flag} \<inter> Tainted s = {}" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
248 |
by (auto simp:attach_Tainted_procs_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
249 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
250 |
lemma attach_Tainted_procs_prop3: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
251 |
"\<lbrakk>p' \<in> attach_Tainted_procs s p h flag; valid s\<rbrakk> \<Longrightarrow> p' \<in> current_procs s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
252 |
by (auto simp:attach_Tainted_procs_def info_shm_flow_in_procs split:if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
253 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
254 |
lemma co2sobj_attach': |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
255 |
"\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
256 |
(case obj of |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
257 |
O_proc p' \<Rightarrow> if (p' = p) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
258 |
then (case cp2sproc (Attach p h flag # s) p of |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
259 |
Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> p \<in> attach_Tainted_procs s p h flag)) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
260 |
| _ \<Rightarrow> None) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
261 |
else if (p' \<in> attach_Tainted_procs s p h flag) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
262 |
then case cp2sproc s p' of |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
263 |
None \<Rightarrow> None |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
264 |
| Some sp \<Rightarrow> Some (S_proc sp True) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
265 |
else co2sobj s obj |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
266 |
| _ \<Rightarrow> co2sobj s obj)" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
267 |
apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
268 |
apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted co2sobj.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
269 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
270 |
apply (frule current_proc_has_sp, simp, erule exE, (erule conjE)+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
271 |
apply (case_tac "cp2sproc (Attach p h flag # s) nat", drule current_proc_has_sp', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
272 |
apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
273 |
apply (simp add:tainted_eq_Tainted attach_Tainted_procs_prop1 del:Tainted.simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
274 |
apply (simp add:cp2sproc_attach split:if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
275 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
276 |
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
277 |
simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
278 |
same_inode_files_prop6 |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
279 |
dest:is_file_in_current is_dir_in_current) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
280 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
281 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
282 |
lemma s2ss_attach: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
283 |
"valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
284 |
update_s2ss_procs s (s2ss s) (Attach p h flag) (attach_Tainted_procs s p h flag \<union> {p})" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
285 |
apply (frule vt_grant_os, frule vd_cons) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
286 |
apply (case_tac "cp2sproc s p", drule current_proc_has_sp', simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
287 |
apply (case_tac "ch2sshm s h", drule current_shm_has_sh', simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
288 |
apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
289 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
290 |
unfolding update_s2ss_procs_def |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
291 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
292 |
apply (erule_tac obj = obj in co2sobj_some_caseD) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
293 |
apply (case_tac "pa = p") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
294 |
apply (rule DiffI, rule UnI2, simp, rule_tac x = pa in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
295 |
apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
296 |
apply (case_tac "pa \<in> attach_Tainted_procs s p h flag") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
297 |
apply (rule DiffI, rule UnI2, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
298 |
apply (rule_tac x = pa in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
299 |
apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
300 |
apply (rule DiffI, rule UnI1, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
301 |
apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
302 |
apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
303 |
apply (simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
304 |
apply (simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
305 |
apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
306 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
307 |
apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
308 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
309 |
apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
310 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
311 |
apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
312 |
apply (erule unbked_sps_I, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
313 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
314 |
apply (erule DiffE, erule UnE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
315 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
316 |
apply (erule_tac obj = obj in co2sobj_some_caseD) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
317 |
apply (case_tac "pa \<in> attach_Tainted_procs s p h flag \<union> {p}") |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
318 |
apply (drule_tac p = pa in not_unbked_sps_D, simp, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
319 |
apply (erule disjE, erule bexE) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
320 |
apply (rule_tac x = "O_proc p'" in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
321 |
apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
322 |
apply (erule bexE, simp, (erule conjE)+) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
323 |
apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
324 |
apply (rule_tac x = "O_proc pa" in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
325 |
apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
326 |
apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
327 |
apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
328 |
apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
329 |
apply (tactic {*my_setiff_tac 1*}, clarsimp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
330 |
apply (rule_tac x = "O_proc pa" in exI, simp) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
331 |
apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
332 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
333 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
334 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
335 |
(* should be modified when socket is model in static *) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
336 |
lemma s2ss_createsock: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
337 |
"valid (CreateSock p af st fd inum # s) \<Longrightarrow> s2ss (CreateSock p af st fd inum # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
338 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
339 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
340 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
341 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
342 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
343 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
344 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
345 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
346 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
347 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
348 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
349 |
lemma s2ss_bind: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
350 |
"valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
351 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
352 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
353 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
354 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
355 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
356 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
357 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
358 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
359 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
360 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
361 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
362 |
lemma s2ss_connect: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
363 |
"valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
364 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
365 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
366 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
367 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
368 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
369 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
370 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
371 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
372 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
373 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
374 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
375 |
lemma s2ss_listen: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
376 |
"valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
377 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
378 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
379 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
380 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
381 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
382 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
383 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
384 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
385 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
386 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
387 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
388 |
lemma s2ss_accept: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
389 |
"valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
390 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
391 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
392 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
393 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
394 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
395 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
396 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
397 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
398 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
399 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
400 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
401 |
lemma s2ss_send: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
402 |
"valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
403 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
404 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
405 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
406 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
407 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
408 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
409 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
410 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
411 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
412 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
413 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
414 |
lemma s2ss_recv: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
415 |
"valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
416 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
417 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
418 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
419 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
420 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
421 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
422 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
423 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
424 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
425 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
426 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
427 |
lemma s2ss_shutdown: |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
428 |
"valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s" |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
429 |
apply (simp add:s2ss_def) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
430 |
apply (tactic {*my_seteq_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
431 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
432 |
apply (simp add:co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
433 |
apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
434 |
apply (tactic {*my_setiff_tac 1*}) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
435 |
apply (rule_tac x = obj in exI) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
436 |
apply (frule_tac obj = obj in co2sobj_other) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
437 |
apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
438 |
done |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
439 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
440 |
lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
441 |
s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
442 |
s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
443 |
s2ss_createshm s2ss_detach s2ss_deleteshm s2ss_attach |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
444 |
s2ss_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
445 |
s2ss_recv s2ss_shutdown |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
446 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
447 |
end |
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
448 |
|
271e9818b6f6
remove shm and linkhard, make a simplified version of selinux
chunhan
parents:
diff
changeset
|
449 |
end |