|
1 theory final_theorems |
|
2 imports Main rc_theory del_vs_del_s tainted_vs_tainted_s |
|
3 begin |
|
4 |
|
5 context tainting_s_complete begin |
|
6 |
|
7 theorem static_complete: |
|
8 assumes undel: "undeletable obj" and tbl: "taintable obj" |
|
9 shows "taintable_s obj" |
|
10 proof- |
|
11 from tbl obtain s where tainted: "obj \<in> tainted s" |
|
12 by (auto simp:taintable_def) |
|
13 hence vs: "valid s" by (simp add:tainted_is_valid) |
|
14 from undel vs have "\<not> deleted obj s" and "exists [] obj" |
|
15 by (auto simp:undeletable_def) |
|
16 moreover from tainted have "valid s" by (rule tainted_is_valid) |
|
17 ultimately have "source_of_sobj (obj2sobj s obj) = Some obj" |
|
18 using init_obj_keeps_source by auto |
|
19 with tainted t2ts |
|
20 show ?thesis unfolding taintable_s_def |
|
21 by (rule_tac x = "obj2sobj s obj" in exI, simp) |
|
22 qed |
|
23 |
|
24 theorem undeletable_s_complete: |
|
25 "undeletable_s obj \<Longrightarrow> undeletable obj" |
|
26 apply (clarsimp simp:undeletable_s_def undeletable_def) |
|
27 apply (drule deleted_imp_deletable_s, simp+) |
|
28 done |
|
29 |
|
30 theorem final_offer: |
|
31 "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; exists [] obj\<rbrakk> \<Longrightarrow> \<not> taintable obj" |
|
32 apply (erule swap) |
|
33 by (simp add:static_complete undeletable_s_complete) |
|
34 |
|
35 end |
|
36 |
|
37 context tainting_s_sound begin |
|
38 |
|
39 theorem static_sound: |
|
40 assumes tbl_s: "taintable_s obj" |
|
41 shows "taintable obj" |
|
42 proof- |
|
43 from tbl_s obtain sobj where ts: "sobj \<in> tainted_s" |
|
44 and sreq: "source_of_sobj sobj = Some obj" |
|
45 by (auto simp:taintable_s_def) |
|
46 from ts obtain obj' \<tau> where t: "obj' \<in> tainted \<tau>" |
|
47 and vs: "valid \<tau>" and sreq': "sobj_source_eq_obj sobj obj'" |
|
48 by (auto dest!:tainted_s2tainted dest:tainted_is_valid) |
|
49 from sreq' sreq have "obj = obj'" by (simp add:source_eq) |
|
50 with vs t |
|
51 show ?thesis by (auto simp:taintable_def) |
|
52 qed |
|
53 |
|
54 end |
|
55 |
|
56 end |