|
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: |
|
10 "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" | |
|
11 Semi: |
|
12 "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" | |
|
13 If: |
|
14 "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1; max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk> |
|
15 \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" | |
|
16 While: |
|
17 "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c" |
|
18 |
|
19 code_pred (expected_modes: i => i => bool) sec_type . |
|
20 |
|
21 inductive_cases [elim!]: |
|
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" |
|
23 |
|
24 |
|
25 lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c" |
|
26 apply(induct arbitrary: l' rule: sec_type.induct) |
|
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)" |
|
35 proof(induct rule: big_step_induct) |
|
36 case Skip thus ?case by simp |
|
37 next |
|
38 case Assign thus ?case by auto |
|
39 next |
|
40 case Semi thus ?case by auto |
|
41 next |
|
42 case (IfTrue b s c1) |
|
43 hence "max (sec_bexp b) l \<turnstile> c1" by auto |
|
44 hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono) |
|
45 thus ?case using IfTrue.hyps by metis |
|
46 next |
|
47 case (IfFalse b s c2) |
|
48 hence "max (sec_bexp b) l \<turnstile> c2" by auto |
|
49 hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono) |
|
50 thus ?case using IfFalse.hyps by metis |
|
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" |
|
60 apply(induct arbitrary: s rule: sec_type.induct) |
|
61 apply (metis big_step.Skip) |
|
62 apply (metis big_step.Assign) |
|
63 apply (metis big_step.Semi) |
|
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)" |
|
70 proof(induct arbitrary: t rule: big_step_induct) |
|
71 case Skip thus ?case by auto |
|
72 next |
|
73 case (Assign x a s) |
|
74 have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto |
|
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" |
|
80 with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith |
|
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 |
|
89 case Semi thus ?case by blast |
|
90 next |
|
91 case (IfTrue b s c1 s' c2) |
|
92 have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto |
|
93 obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
|
94 using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast |
|
95 show ?case |
|
96 proof cases |
|
97 assume "sec_bexp b \<le> l" |
|
98 hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto |
|
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 |
|
102 assume "\<not> sec_bexp b \<le> l" |
|
103 hence 0: "sec_bexp b \<noteq> 0" by arith |
|
104 have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2" |
|
105 by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`) |
|
106 from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l` |
|
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 |
|
112 from confinement[OF this 1] `\<not> sec_bexp b \<le> l` |
|
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) |
|
119 have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto |
|
120 obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
|
121 using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast |
|
122 show ?case |
|
123 proof cases |
|
124 assume "sec_bexp b \<le> l" |
|
125 hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto |
|
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 |
|
129 assume "\<not> sec_bexp b \<le> l" |
|
130 hence 0: "sec_bexp b \<noteq> 0" by arith |
|
131 have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2" |
|
132 by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`) |
|
133 from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l` |
|
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 |
|
139 from confinement[OF this 1] `\<not> sec_bexp b \<le> l` |
|
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) |
|
146 hence [simp]: "sec_bexp b = 0" by auto |
|
147 have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto |
|
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" |
|
153 from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto |
|
154 have "0 \<turnstile> c" using WhileTrue.prems(1) by auto |
|
155 from WhileTrue(3)[OF this WhileTrue.prems(2)] |
|
156 obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast |
|
157 from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)] |
|
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': |
|
177 "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" | |
|
178 Semi': |
|
179 "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" | |
|
180 If': |
|
181 "\<lbrakk> sec_bexp 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" | |
|
182 While': |
|
183 "\<lbrakk> sec_bexp b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" | |
|
184 anti_mono': |
|
185 "\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c" |
|
186 |
|
187 lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c" |
|
188 apply(induct rule: sec_type.induct) |
|
189 apply (metis Skip') |
|
190 apply (metis Assign') |
|
191 apply (metis Semi') |
|
192 apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono') |
|
193 by (metis While') |
|
194 |
|
195 |
|
196 lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c" |
|
197 apply(induct rule: sec_type'.induct) |
|
198 apply (metis Skip) |
|
199 apply (metis Assign) |
|
200 apply (metis Semi) |
|
201 apply (metis min_max.sup_absorb2 If) |
|
202 apply (metis While) |
|
203 by (metis anti_mono) |
|
204 |
|
205 end |