43158

1 
theory Sec_TypingT imports Sec_Type_Expr


2 
begin


3 


4 
subsection "A TerminationSensitive 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"

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


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)

45015

45 
thus ?case using IfTrue.IH by metis

43158

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)

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)


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

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)


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

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

45015

188 
apply(induction rule: sec_type.induct)

43158

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"

45015

197 
apply(induction rule: sec_type'.induct)

43158

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
