author | nipkow |
Fri, 17 May 2013 08:19:52 +0200 | |
changeset 52046 | bc01725d7918 |
parent 51456 | a6e3a5ec9847 |
child 52382 | 741d10d7f2c1 |
permissions | -rw-r--r-- |
43158 | 1 |
theory Sec_TypingT imports Sec_Type_Expr |
2 |
begin |
|
3 |
||
4 |
subsection "A Termination-Sensitive Syntax Directed System" |
|
5 |
||
6 |
inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where |
|
7 |
Skip: |
|
8 |
"l \<turnstile> SKIP" | |
|
9 |
Assign: |
|
50342 | 10 |
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" | |
47818 | 11 |
Seq: |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51456
diff
changeset
|
12 |
"l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2" | |
43158 | 13 |
If: |
50342 | 14 |
"\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1; max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> |
43158 | 15 |
\<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
16 |
While: |
|
50342 | 17 |
"sec b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c" |
43158 | 18 |
|
19 |
code_pred (expected_modes: i => i => bool) sec_type . |
|
20 |
||
21 |
inductive_cases [elim!]: |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51456
diff
changeset
|
22 |
"l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c" |
43158 | 23 |
|
24 |
||
25 |
lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c" |
|
45015 | 26 |
apply(induction arbitrary: l' rule: sec_type.induct) |
43158 | 27 |
apply (metis sec_type.intros(1)) |
28 |
apply (metis le_trans sec_type.intros(2)) |
|
29 |
apply (metis sec_type.intros(3)) |
|
30 |
apply (metis If le_refl sup_mono sup_nat_def) |
|
31 |
by (metis While le_0_eq) |
|
32 |
||
33 |
||
34 |
lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)" |
|
45015 | 35 |
proof(induction rule: big_step_induct) |
43158 | 36 |
case Skip thus ?case by simp |
37 |
next |
|
38 |
case Assign thus ?case by auto |
|
39 |
next |
|
47818 | 40 |
case Seq thus ?case by auto |
43158 | 41 |
next |
42 |
case (IfTrue b s c1) |
|
50342 | 43 |
hence "max (sec b) l \<turnstile> c1" by auto |
43158 | 44 |
hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono) |
45015 | 45 |
thus ?case using IfTrue.IH by metis |
43158 | 46 |
next |
47 |
case (IfFalse b s c2) |
|
50342 | 48 |
hence "max (sec b) l \<turnstile> c2" by auto |
43158 | 49 |
hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono) |
45015 | 50 |
thus ?case using IfFalse.IH by metis |
43158 | 51 |
next |
52 |
case WhileFalse thus ?case by auto |
|
53 |
next |
|
54 |
case (WhileTrue b s1 c) |
|
55 |
hence "l \<turnstile> c" by auto |
|
56 |
thus ?case using WhileTrue by metis |
|
57 |
qed |
|
58 |
||
59 |
lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t" |
|
45015 | 60 |
apply(induction arbitrary: s rule: sec_type.induct) |
43158 | 61 |
apply (metis big_step.Skip) |
62 |
apply (metis big_step.Assign) |
|
47818 | 63 |
apply (metis big_step.Seq) |
43158 | 64 |
apply (metis IfFalse IfTrue le0 le_antisym le_maxI2) |
65 |
apply simp |
|
66 |
done |
|
67 |
||
68 |
theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> s = t (\<le> l) |
|
69 |
\<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)" |
|
45015 | 70 |
proof(induction arbitrary: t rule: big_step_induct) |
43158 | 71 |
case Skip thus ?case by auto |
72 |
next |
|
73 |
case (Assign x a s) |
|
50342 | 74 |
have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto |
43158 | 75 |
have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto |
76 |
moreover |
|
77 |
have "s(x := aval a s) = t(x := aval a t) (\<le> l)" |
|
78 |
proof auto |
|
79 |
assume "sec x \<le> l" |
|
50342 | 80 |
with `sec x \<ge> sec a` have "sec a \<le> l" by arith |
43158 | 81 |
thus "aval a s = aval a t" |
82 |
by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`]) |
|
83 |
next |
|
84 |
fix y assume "y \<noteq> x" "sec y \<le> l" |
|
85 |
thus "s y = t y" using `s = t (\<le> l)` by simp |
|
86 |
qed |
|
87 |
ultimately show ?case by blast |
|
88 |
next |
|
47818 | 89 |
case Seq thus ?case by blast |
43158 | 90 |
next |
91 |
case (IfTrue b s c1 s' c2) |
|
50342 | 92 |
have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems by auto |
43158 | 93 |
obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
50342 | 94 |
using IfTrue(3)[OF anti_mono[OF `sec b \<turnstile> c1`] IfTrue.prems(2)] by blast |
43158 | 95 |
show ?case |
96 |
proof cases |
|
50342 | 97 |
assume "sec b \<le> l" |
98 |
hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
|
43158 | 99 |
hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le) |
100 |
thus ?thesis by (metis t' big_step.IfTrue) |
|
101 |
next |
|
50342 | 102 |
assume "\<not> sec b \<le> l" |
103 |
hence 0: "sec b \<noteq> 0" by arith |
|
104 |
have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2" |
|
105 |
by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`) |
|
106 |
from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec b \<le> l` |
|
43158 | 107 |
have "s = s' (\<le> l)" by auto |
108 |
moreover |
|
109 |
from termi_if_non0[OF 1 0, of t] obtain t' where |
|
110 |
"(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. |
|
111 |
moreover |
|
50342 | 112 |
from confinement[OF this 1] `\<not> sec b \<le> l` |
43158 | 113 |
have "t = t' (\<le> l)" by auto |
114 |
ultimately |
|
115 |
show ?case using `s = t (\<le> l)` by auto |
|
116 |
qed |
|
117 |
next |
|
118 |
case (IfFalse b s c2 s' c1) |
|
50342 | 119 |
have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems by auto |
43158 | 120 |
obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
50342 | 121 |
using IfFalse(3)[OF anti_mono[OF `sec b \<turnstile> c2`] IfFalse.prems(2)] by blast |
43158 | 122 |
show ?case |
123 |
proof cases |
|
50342 | 124 |
assume "sec b \<le> l" |
125 |
hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
|
43158 | 126 |
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le) |
127 |
thus ?thesis by (metis t' big_step.IfFalse) |
|
128 |
next |
|
50342 | 129 |
assume "\<not> sec b \<le> l" |
130 |
hence 0: "sec b \<noteq> 0" by arith |
|
131 |
have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2" |
|
132 |
by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`) |
|
133 |
from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l` |
|
43158 | 134 |
have "s = s' (\<le> l)" by auto |
135 |
moreover |
|
136 |
from termi_if_non0[OF 1 0, of t] obtain t' where |
|
137 |
"(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. |
|
138 |
moreover |
|
50342 | 139 |
from confinement[OF this 1] `\<not> sec b \<le> l` |
43158 | 140 |
have "t = t' (\<le> l)" by auto |
141 |
ultimately |
|
142 |
show ?case using `s = t (\<le> l)` by auto |
|
143 |
qed |
|
144 |
next |
|
145 |
case (WhileFalse b s c) |
|
50342 | 146 |
hence [simp]: "sec b = 0" by auto |
147 |
have "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto |
|
43158 | 148 |
hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl) |
149 |
with WhileFalse.prems(2) show ?case by auto |
|
150 |
next |
|
151 |
case (WhileTrue b s c s'' s') |
|
152 |
let ?w = "WHILE b DO c" |
|
50342 | 153 |
from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto |
43158 | 154 |
have "0 \<turnstile> c" using WhileTrue.prems(1) by auto |
45015 | 155 |
from WhileTrue.IH(1)[OF this WhileTrue.prems(2)] |
43158 | 156 |
obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast |
45015 | 157 |
from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)] |
43158 | 158 |
obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast |
159 |
from `bval b s` have "bval b t" |
|
160 |
using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto |
|
161 |
show ?case |
|
162 |
using big_step.WhileTrue[OF `bval b t` `(c,t) \<Rightarrow> t''` `(?w,t'') \<Rightarrow> t'`] |
|
163 |
by (metis `s' = t' (\<le> l)`) |
|
164 |
qed |
|
165 |
||
166 |
subsection "The Standard Termination-Sensitive System" |
|
167 |
||
168 |
text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The |
|
169 |
standard formulation, however, is slightly different, replacing the maximum |
|
170 |
computation by an antimonotonicity rule. We introduce the standard system now |
|
171 |
and show the equivalence with our formulation. *} |
|
172 |
||
173 |
inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where |
|
174 |
Skip': |
|
175 |
"l \<turnstile>' SKIP" | |
|
176 |
Assign': |
|
50342 | 177 |
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" | |
47818 | 178 |
Seq': |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51456
diff
changeset
|
179 |
"l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" | |
43158 | 180 |
If': |
50342 | 181 |
"\<lbrakk> sec b \<le> l; l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
43158 | 182 |
While': |
50342 | 183 |
"\<lbrakk> sec b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" | |
43158 | 184 |
anti_mono': |
185 |
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c" |
|
186 |
||
51456 | 187 |
lemma sec_type_sec_type': |
188 |
"l \<turnstile> c \<Longrightarrow> l \<turnstile>' c" |
|
45015 | 189 |
apply(induction rule: sec_type.induct) |
43158 | 190 |
apply (metis Skip') |
191 |
apply (metis Assign') |
|
47818 | 192 |
apply (metis Seq') |
43158 | 193 |
apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono') |
194 |
by (metis While') |
|
195 |
||
196 |
||
51456 | 197 |
lemma sec_type'_sec_type: |
198 |
"l \<turnstile>' c \<Longrightarrow> l \<turnstile> c" |
|
45015 | 199 |
apply(induction rule: sec_type'.induct) |
43158 | 200 |
apply (metis Skip) |
201 |
apply (metis Assign) |
|
47818 | 202 |
apply (metis Seq) |
43158 | 203 |
apply (metis min_max.sup_absorb2 If) |
204 |
apply (metis While) |
|
205 |
by (metis anti_mono) |
|
206 |
||
51456 | 207 |
corollary sec_type_eq: "l \<turnstile> c \<longleftrightarrow> l \<turnstile>' c" |
208 |
by (metis sec_type'_sec_type sec_type_sec_type') |
|
209 |
||
43158 | 210 |
end |