| author | chunhan |
| Thu, 05 Sep 2013 13:23:03 +0800 | |
| changeset 42 | 021672ec28f5 |
| parent 41 | db15ef2ee18c |
| child 43 | 137358bd4921 |
| 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 |
||
|
33
6884b3c9284b
fix bug of static.thy for the static of recvmsg case
chunhan
parents:
32
diff
changeset
|
12 |
lemma s2ss_execve: |
| 34 | 13 |
"valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( |
14 |
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
|
15 |
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
|
16 |
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
|
17 |
| _ \<Rightarrow> s2ss s) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
\<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
|
21 |
| _ \<Rightarrow> s2ss s) )" |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
22 |
apply (frule vd_cons, frule vt_grant_os, simp split:if_splits) |
| 42 | 23 |
|
| 41 | 24 |
apply (rule conjI, rule impI, (erule exE|erule conjE)+) |
25 |
apply (frule_tac p = p in current_proc_has_sp, simp, erule exE) |
|
26 |
apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp) |
|
27 |
apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") |
|
28 |
apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp) |
|
29 |
apply (erule exE, simp) |
|
30 |
apply (simp add:s2ss_def, rule set_eqI, rule iffI) |
|
31 |
apply (drule CollectD, (erule exE|erule conjE)+) |
|
32 |
apply (case_tac "obj = O_proc p") |
|
33 |
apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits) |
|
| 42 | 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) |
|
| 41 | 42 |
|
43 |
apply (case_tac obj, simp_all add:co2sobj_execve alive_simps) |
|
44 |
thm alive_execve |
|
45 |
thm co2sobj_execve |
|
46 |
apply (simp add:co2sobj_execve, rule disjI2) |
|
47 |
apply (rule_tac x = obj in exI, simp split:t_object.splits) |
|
48 |
thm co2sobj_execve |
|
49 |
apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1] |
|
50 |
apply (simp add:co2sobj_execve) |
|
51 |
apply clarsimp |
|
52 |
thm current_proc_has_sp |
|
53 |
||
54 |
apply (auto simp:s2ss_def co2sobj_execve split:option.splits) |
|
55 |
||
56 |
||
57 |
||
|
35
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
58 |
apply (rule conjI, clarify) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
apply (simp, (erule conjE)+) |
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
70 |
|
|
f2e620d799cf
in the middle of building simpset for co2sobj, therefore we can deal with s2ss
chunhan
parents:
34
diff
changeset
|
71 |
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
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
apply (auto split:if_splits) |