6 |
6 |
7 context tainting_s begin |
7 context tainting_s begin |
8 |
8 |
9 (* simpset for s2ss*) |
9 (* simpset for s2ss*) |
10 |
10 |
11 lemma co2sobj_createshm: |
|
12 "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = ( |
|
13 case obj of |
|
14 O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of |
|
15 Some sh \<Rightarrow> Some (S_shm sh) |
|
16 | _ \<Rightarrow> None) |
|
17 else co2sobj s obj |
|
18 | _ \<Rightarrow> co2sobj s obj)" |
|
19 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
20 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
21 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
22 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
23 same_inode_files_prop6 ch2sshm_simps |
|
24 dest!:current_shm_has_sh' |
|
25 dest:is_file_in_current is_dir_in_current) |
|
26 done |
|
27 |
11 |
28 lemma s2ss_execve: |
12 lemma s2ss_execve: |
29 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( |
13 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( |
30 if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p)) |
14 if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p)) |
31 then (case (cp2sproc (Execve p f fds # s) p) of |
15 then (case (cp2sproc (Execve p f fds # s) p) of |
34 else (case (cp2sproc (Execve p f fds # s) p) of |
18 else (case (cp2sproc (Execve p f fds # s) p) of |
35 Some sp \<Rightarrow> s2ss s - {S_proc sp (O_proc p \<in> Tainted s)} |
19 Some sp \<Rightarrow> s2ss s - {S_proc sp (O_proc p \<in> Tainted s)} |
36 \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)} |
20 \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)} |
37 | _ \<Rightarrow> s2ss s) )" |
21 | _ \<Rightarrow> s2ss s) )" |
38 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits) |
22 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits) |
|
23 |
39 apply (rule conjI, rule impI, (erule exE|erule conjE)+) |
24 apply (rule conjI, rule impI, (erule exE|erule conjE)+) |
40 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE) |
25 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE) |
41 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp) |
26 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp) |
42 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") |
27 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") |
43 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp) |
28 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp) |
44 apply (erule exE, simp) |
29 apply (erule exE, simp) |
45 apply (simp add:s2ss_def, rule set_eqI, rule iffI) |
30 apply (simp add:s2ss_def, rule set_eqI, rule iffI) |
46 apply (drule CollectD, (erule exE|erule conjE)+) |
31 apply (drule CollectD, (erule exE|erule conjE)+) |
47 apply (case_tac "obj = O_proc p") |
32 apply (case_tac "obj = O_proc p") |
48 apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits) |
33 apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits) |
|
34 apply (simp add:co2sobj_execve, rule disjI2) |
|
35 apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1] |
|
36 apply (simp, erule disjE) |
|
37 apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) |
|
38 apply (erule exE| erule conjE)+ |
|
39 apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)") |
|
40 apply (rule_tac x = "O_proc p'" in exI) |
|
41 apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve) |
49 |
42 |
50 apply (case_tac obj, simp_all add:co2sobj_execve alive_simps) |
43 apply (case_tac obj, simp_all add:co2sobj_execve alive_simps) |
51 thm alive_execve |
44 thm alive_execve |
52 thm co2sobj_execve |
45 thm co2sobj_execve |
53 apply (simp add:co2sobj_execve, rule disjI2) |
46 apply (simp add:co2sobj_execve, rule disjI2) |