43158

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Sec_Typing imports Sec_Type_Expr


4 
begin


5 


6 
subsection "Syntax Directed Typing"


7 


8 
inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where


9 
Skip:


10 
"l \<turnstile> SKIP" 


11 
Assign:


12 
"\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" 


13 
Semi:


14 
"\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" 


15 
If:


16 
"\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1; max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" 


17 
While:


18 
"max (sec_bexp b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"


19 


20 
code_pred (expected_modes: i => i => bool) sec_type .


21 


22 
value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"


23 
value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x'' ::= N 0 ELSE SKIP"


24 
value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"


25 


26 
inductive_cases [elim!]:


27 
"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"


28 


29 


30 
text{* An important property: antimonotonicity. *}


31 


32 
lemma anti_mono: "\<lbrakk> l \<turnstile> c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"

45015

33 
apply(induction arbitrary: l' rule: sec_type.induct)

43158

34 
apply (metis sec_type.intros(1))


35 
apply (metis le_trans sec_type.intros(2))


36 
apply (metis sec_type.intros(3))


37 
apply (metis If le_refl sup_mono sup_nat_def)


38 
apply (metis While le_refl sup_mono sup_nat_def)


39 
done


40 


41 
lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t; l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"

45015

42 
proof(induction rule: big_step_induct)

43158

43 
case Skip thus ?case by simp


44 
next


45 
case Assign thus ?case by auto


46 
next


47 
case Semi thus ?case by auto


48 
next


49 
case (IfTrue b s c1)


50 
hence "max (sec_bexp b) l \<turnstile> c1" by auto


51 
hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)

45015

52 
thus ?case using IfTrue.IH by metis

43158

53 
next


54 
case (IfFalse b s c2)


55 
hence "max (sec_bexp b) l \<turnstile> c2" by auto


56 
hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)

45015

57 
thus ?case using IfFalse.IH by metis

43158

58 
next


59 
case WhileFalse thus ?case by auto


60 
next


61 
case (WhileTrue b s1 c)


62 
hence "max (sec_bexp b) l \<turnstile> c" by auto


63 
hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)


64 
thus ?case using WhileTrue by metis


65 
qed


66 


67 


68 
theorem noninterference:


69 
"\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t'; 0 \<turnstile> c; s = t (\<le> l) \<rbrakk>


70 
\<Longrightarrow> s' = t' (\<le> l)"

45015

71 
proof(induction arbitrary: t t' rule: big_step_induct)

43158

72 
case Skip thus ?case by auto


73 
next


74 
case (Assign x a s)


75 
have [simp]: "t' = t(x := aval a t)" using Assign by auto


76 
have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto


77 
show ?case


78 
proof auto


79 
assume "sec x \<le> l"


80 
with `sec x >= 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 
next


88 
case Semi thus ?case by blast


89 
next


90 
case (IfTrue b s c1 s' c2)


91 
have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto


92 
show ?case


93 
proof cases


94 
assume "sec_bexp b \<le> l"


95 
hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto


96 
hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)

45015

97 
with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1` anti_mono

43158

98 
show ?thesis by auto


99 
next


100 
assume "\<not> sec_bexp b \<le> l"


101 
have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"


102 
by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)

45823

103 
from confinement[OF IfTrue.hyps(2) `sec_bexp b \<turnstile> c1`] `\<not> sec_bexp b \<le> l`

43158

104 
have "s = s' (\<le> l)" by auto


105 
moreover


106 
from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`


107 
have "t = t' (\<le> l)" by auto


108 
ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto


109 
qed


110 
next


111 
case (IfFalse b s c2 s' c1)


112 
have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems(2) by auto


113 
show ?case


114 
proof cases


115 
assume "sec_bexp b \<le> l"


116 
hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto


117 
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)

45015

118 
with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono

43158

119 
show ?thesis by auto


120 
next


121 
assume "\<not> sec_bexp b \<le> l"


122 
have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"


123 
by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)


124 
from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`


125 
have "s = s' (\<le> l)" by auto


126 
moreover


127 
from confinement[OF IfFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`


128 
have "t = t' (\<le> l)" by auto


129 
ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto


130 
qed


131 
next


132 
case (WhileFalse b s c)


133 
have "sec_bexp b \<turnstile> c" using WhileFalse.prems(2) by auto


134 
show ?case


135 
proof cases


136 
assume "sec_bexp b \<le> l"


137 
hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto


138 
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)


139 
with WhileFalse.prems(1,3) show ?thesis by auto


140 
next


141 
assume "\<not> sec_bexp b \<le> l"


142 
have 1: "sec_bexp b \<turnstile> WHILE b DO c"


143 
by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)


144 
from confinement[OF WhileFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`


145 
have "t = t' (\<le> l)" by auto


146 
thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto


147 
qed


148 
next


149 
case (WhileTrue b s1 c s2 s3 t1 t3)


150 
let ?w = "WHILE b DO c"


151 
have "sec_bexp b \<turnstile> c" using WhileTrue.prems(2) by auto


152 
show ?case


153 
proof cases


154 
assume "sec_bexp b \<le> l"


155 
hence "s1 = t1 (\<le> sec_bexp b)" using `s1 = t1 (\<le> l)` by auto


156 
hence "bval b t1"


157 
using `bval b s1` by(simp add: bval_eq_if_eq_le)


158 
then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"


159 
using `(?w,t1) \<Rightarrow> t3` by auto

45015

160 
from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`


161 
WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]

43158

162 
`s1 = t1 (\<le> l)`]]


163 
show ?thesis by simp


164 
next


165 
assume "\<not> sec_bexp b \<le> l"


166 
have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)

45015

167 
from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`

43158

168 
have "s1 = s3 (\<le> l)" by auto


169 
moreover


170 
from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`


171 
have "t1 = t3 (\<le> l)" by auto


172 
ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto


173 
qed


174 
qed


175 


176 


177 
subsection "The Standard Typing System"


178 


179 
text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The


180 
standard formulation, however, is slightly different, replacing the maximum


181 
computation by an antimonotonicity rule. We introduce the standard system now


182 
and show the equivalence with our formulation. *}


183 


184 
inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where


185 
Skip':


186 
"l \<turnstile>' SKIP" 


187 
Assign':


188 
"\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" 


189 
Semi':


190 
"\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" 


191 
If':


192 
"\<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" 


193 
While':


194 
"\<lbrakk> sec_bexp b \<le> l; l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" 


195 
anti_mono':


196 
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"


197 


198 
lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"

45015

199 
apply(induction rule: sec_type.induct)

43158

200 
apply (metis Skip')


201 
apply (metis Assign')


202 
apply (metis Semi')


203 
apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')


204 
by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')


205 


206 


207 
lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"

45015

208 
apply(induction rule: sec_type'.induct)

43158

209 
apply (metis Skip)


210 
apply (metis Assign)


211 
apply (metis Semi)


212 
apply (metis min_max.sup_absorb2 If)


213 
apply (metis min_max.sup_absorb2 While)


214 
by (metis anti_mono)


215 


216 
subsection "A BottomUp Typing System"


217 


218 
inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where


219 
Skip2:


220 
"\<turnstile> SKIP : l" 


221 
Assign2:


222 
"sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" 


223 
Semi2:


224 
"\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " 


225 
If2:


226 
"\<lbrakk> sec_bexp b \<le> min l\<^isub>1 l\<^isub>2; \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>


227 
\<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" 


228 
While2:


229 
"\<lbrakk> sec_bexp b \<le> l; \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"


230 


231 


232 
lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"

45015

233 
apply(induction rule: sec_type2.induct)

43158

234 
apply (metis Skip')


235 
apply (metis Assign' eq_imp_le)


236 
apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)


237 
apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)


238 
by (metis While')


239 


240 
lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"

45015

241 
apply(induction rule: sec_type'.induct)

43158

242 
apply (metis Skip2 le_refl)


243 
apply (metis Assign2)


244 
apply (metis Semi2 min_max.inf_greatest)


245 
apply (metis If2 inf_greatest inf_nat_def le_trans)


246 
apply (metis While2 le_trans)


247 
by (metis le_trans)


248 


249 
end
