| author | chunhan |
| Wed, 04 Sep 2013 15:13:54 +0800 | |
| changeset 41 | db15ef2ee18c |
| parent 39 | 13bba99ca090 |
| child 42 | 021672ec28f5 |
| permissions | -rw-r--r-- |
| 32 | 1 |
(*<*) |
2 |
theory S2ss_prop |
|
3 |
imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop |
|
4 |
begin |
|
5 |
(*>*) |
|
6 |
||
|
33
6884b3c9284b
fix bug of static.thy for the static of recvmsg case
chunhan
parents:
32
diff
changeset
|
7 |
context tainting_s begin |
|
6884b3c9284b
fix bug of static.thy for the static of recvmsg case
chunhan
parents:
32
diff
changeset
|
8 |
|
| 41 | 9 |
(* simpset for s2ss*) |
| 39 | 10 |
|
11 |
lemma co2sobj_createshm: |
|
| 41 | 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)" |
|
| 39 | 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 |
||
|
33
6884b3c9284b
fix bug of static.thy for the static of recvmsg case
chunhan
parents:
32
diff
changeset
|
28 |
lemma s2ss_execve: |
| 34 | 29 |
"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)) |
|
|
35
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
31 |
then (case (cp2sproc (Execve p f fds # s) p) of |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
32 |
Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
33 |
| _ \<Rightarrow> s2ss s) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
34 |
else (case (cp2sproc (Execve p f fds # s) p) of |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
35 |
Some sp \<Rightarrow> s2ss s - {S_proc sp (O_proc p \<in> Tainted s)}
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
36 |
\<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
37 |
| _ \<Rightarrow> s2ss s) )" |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
38 |
apply (frule vd_cons, frule vt_grant_os, simp split:if_splits) |
| 41 | 39 |
apply (rule conjI, rule impI, (erule exE|erule conjE)+) |
40 |
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) |
|
42 |
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) |
|
44 |
apply (erule exE, simp) |
|
45 |
apply (simp add:s2ss_def, rule set_eqI, rule iffI) |
|
46 |
apply (drule CollectD, (erule exE|erule conjE)+) |
|
47 |
apply (case_tac "obj = O_proc p") |
|
48 |
apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits) |
|
49 |
||
50 |
apply (case_tac obj, simp_all add:co2sobj_execve alive_simps) |
|
51 |
thm alive_execve |
|
52 |
thm co2sobj_execve |
|
53 |
apply (simp add:co2sobj_execve, rule disjI2) |
|
54 |
apply (rule_tac x = obj in exI, simp split:t_object.splits) |
|
55 |
thm co2sobj_execve |
|
56 |
apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1] |
|
57 |
apply (simp add:co2sobj_execve) |
|
58 |
apply clarsimp |
|
59 |
thm current_proc_has_sp |
|
60 |
||
61 |
apply (auto simp:s2ss_def co2sobj_execve split:option.splits) |
|
62 |
||
63 |
||
64 |
||
|
35
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
65 |
apply (rule conjI, clarify) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
66 |
apply (frule_tac p = p in current_proc_has_sp, simp, erule exE) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
67 |
apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
68 |
apply (simp, (erule conjE)+) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
69 |
apply (split option.splits, rule conjI, rule impI, drule current_proc_has_sp', simp, simp) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
70 |
apply (rule allI, rule impI) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
71 |
apply (rule set_eqI, rule iffI) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
72 |
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
73 |
apply (simp split:option.splits) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
74 |
apply (frule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
75 |
thm current_proc_has_sp |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
76 |
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
77 |
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
78 |
apply (simp split:option.splits) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
79 |
apply (drule current_proc_has_sp', simp, simp) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
80 |
apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
81 |
apply (simp add:s2ss_def) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
82 |
apply (rule allI|rule impI)+ |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
83 |
apply (rule set_eqI, rule iffI) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
84 |
apply (auto simp:alive_simps) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
85 |
apply (case_tac obj, auto split:option.splits simp:cp2sproc_execve) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
86 |
apply (auto split:if_splits) |