src/HOL/IMP/Sec_Typing.thy
author nipkow
Tue Dec 04 12:19:19 2012 +0100 (2012-12-04)
changeset 50342 e77b0dbcae5b
parent 47818 151d137f1095
child 51412 c475a3983431
permissions -rw-r--r--
tuned defs of sec_xyz
     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 a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
    13 Seq:
    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 b) l \<turnstile> c\<^isub>1;  max (sec 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 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: anti-monotonicity. *}
    31 
    32 lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
    33 apply(induction arbitrary: l' rule: sec_type.induct)
    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)"
    42 proof(induction rule: big_step_induct)
    43   case Skip thus ?case by simp
    44 next
    45   case Assign thus ?case by auto
    46 next
    47   case Seq thus ?case by auto
    48 next
    49   case (IfTrue b s c1)
    50   hence "max (sec b) l \<turnstile> c1" by auto
    51   hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
    52   thus ?case using IfTrue.IH by metis
    53 next
    54   case (IfFalse b s c2)
    55   hence "max (sec b) l \<turnstile> c2" by auto
    56   hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
    57   thus ?case using IfFalse.IH by metis
    58 next
    59   case WhileFalse thus ?case by auto
    60 next
    61   case (WhileTrue b s1 c)
    62   hence "max (sec 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)"
    71 proof(induction arbitrary: t t' rule: big_step_induct)
    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 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 a` have "sec 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 Seq thus ?case by blast
    89 next
    90   case (IfTrue b s c1 s' c2)
    91   have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems(2) by auto
    92   show ?case
    93   proof cases
    94     assume "sec b \<le> l"
    95     hence "s = t (\<le> sec 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)
    97     with IfTrue.IH IfTrue.prems(1,3) `sec b \<turnstile> c1`  anti_mono
    98     show ?thesis by auto
    99   next
   100     assume "\<not> sec b \<le> l"
   101     have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
   102       by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
   103     from confinement[OF IfTrue.hyps(2) `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
   104     have "s = s' (\<le> l)" by auto
   105     moreover
   106     from confinement[OF IfTrue.prems(1) 1] `\<not> sec 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 b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems(2) by auto
   113   show ?case
   114   proof cases
   115     assume "sec b \<le> l"
   116     hence "s = t (\<le> sec 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)
   118     with IfFalse.IH IfFalse.prems(1,3) `sec b \<turnstile> c2` anti_mono
   119     show ?thesis by auto
   120   next
   121     assume "\<not> sec b \<le> l"
   122     have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
   123       by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
   124     from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
   125     have "s = s' (\<le> l)" by auto
   126     moreover
   127     from confinement[OF IfFalse.prems(1) 1] `\<not> sec 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 b \<turnstile> c" using WhileFalse.prems(2) by auto
   134   show ?case
   135   proof cases
   136     assume "sec b \<le> l"
   137     hence "s = t (\<le> sec 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 b \<le> l"
   142     have 1: "sec b \<turnstile> WHILE b DO c"
   143       by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
   144     from confinement[OF WhileFalse.prems(1) 1] `\<not> sec 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 b \<turnstile> c" using WhileTrue.prems(2) by auto
   152   show ?case
   153   proof cases
   154     assume "sec b \<le> l"
   155     hence "s1 = t1 (\<le> sec 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
   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 b \<turnstile> c`]
   162         `s1 = t1 (\<le> l)`]]
   163     show ?thesis by simp
   164   next
   165     assume "\<not> sec b \<le> l"
   166     have 1: "sec b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
   167     from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec b \<le> l`
   168     have "s1 = s3 (\<le> l)" by auto
   169     moreover
   170     from confinement[OF WhileTrue.prems(1) 1] `\<not> sec 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 a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
   189 Seq':
   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 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 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"
   199 apply(induction rule: sec_type.induct)
   200 apply (metis Skip')
   201 apply (metis Assign')
   202 apply (metis Seq')
   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"
   208 apply(induction rule: sec_type'.induct)
   209 apply (metis Skip)
   210 apply (metis Assign)
   211 apply (metis Seq)
   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 Bottom-Up 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 a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
   223 Seq2:
   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 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 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"
   233 apply(induction rule: sec_type2.induct)
   234 apply (metis Skip')
   235 apply (metis Assign' eq_imp_le)
   236 apply (metis Seq' 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'"
   241 apply(induction rule: sec_type'.induct)
   242 apply (metis Skip2 le_refl)
   243 apply (metis Assign2)
   244 apply (metis Seq2 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