src/HOL/IMP/Sec_Typing.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 45823 fe518d5f3598
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
theory Sec_Typing imports Sec_Type_Expr
kleing@43158
     4
begin
kleing@43158
     5
kleing@43158
     6
subsection "Syntax Directed Typing"
kleing@43158
     7
kleing@43158
     8
inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
kleing@43158
     9
Skip:
kleing@43158
    10
  "l \<turnstile> SKIP" |
kleing@43158
    11
Assign:
kleing@43158
    12
  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
kleing@43158
    13
Semi:
kleing@43158
    14
  "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
kleing@43158
    15
If:
kleing@43158
    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" |
kleing@43158
    17
While:
kleing@43158
    18
  "max (sec_bexp b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
kleing@43158
    19
kleing@43158
    20
code_pred (expected_modes: i => i => bool) sec_type .
kleing@43158
    21
kleing@43158
    22
value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
kleing@43158
    23
value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x''  ::= N 0 ELSE SKIP"
kleing@43158
    24
value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
kleing@43158
    25
kleing@43158
    26
inductive_cases [elim!]:
kleing@43158
    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"
kleing@43158
    28
kleing@43158
    29
kleing@43158
    30
text{* An important property: anti-monotonicity. *}
kleing@43158
    31
kleing@43158
    32
lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
nipkow@45015
    33
apply(induction arbitrary: l' rule: sec_type.induct)
kleing@43158
    34
apply (metis sec_type.intros(1))
kleing@43158
    35
apply (metis le_trans sec_type.intros(2))
kleing@43158
    36
apply (metis sec_type.intros(3))
kleing@43158
    37
apply (metis If le_refl sup_mono sup_nat_def)
kleing@43158
    38
apply (metis While le_refl sup_mono sup_nat_def)
kleing@43158
    39
done
kleing@43158
    40
kleing@43158
    41
lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
nipkow@45015
    42
proof(induction rule: big_step_induct)
kleing@43158
    43
  case Skip thus ?case by simp
kleing@43158
    44
next
kleing@43158
    45
  case Assign thus ?case by auto
kleing@43158
    46
next
kleing@43158
    47
  case Semi thus ?case by auto
kleing@43158
    48
next
kleing@43158
    49
  case (IfTrue b s c1)
kleing@43158
    50
  hence "max (sec_bexp b) l \<turnstile> c1" by auto
kleing@43158
    51
  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
nipkow@45015
    52
  thus ?case using IfTrue.IH by metis
kleing@43158
    53
next
kleing@43158
    54
  case (IfFalse b s c2)
kleing@43158
    55
  hence "max (sec_bexp b) l \<turnstile> c2" by auto
kleing@43158
    56
  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
nipkow@45015
    57
  thus ?case using IfFalse.IH by metis
kleing@43158
    58
next
kleing@43158
    59
  case WhileFalse thus ?case by auto
kleing@43158
    60
next
kleing@43158
    61
  case (WhileTrue b s1 c)
kleing@43158
    62
  hence "max (sec_bexp b) l \<turnstile> c" by auto
kleing@43158
    63
  hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
kleing@43158
    64
  thus ?case using WhileTrue by metis
kleing@43158
    65
qed
kleing@43158
    66
kleing@43158
    67
kleing@43158
    68
theorem noninterference:
kleing@43158
    69
  "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
kleing@43158
    70
   \<Longrightarrow> s' = t' (\<le> l)"
nipkow@45015
    71
proof(induction arbitrary: t t' rule: big_step_induct)
kleing@43158
    72
  case Skip thus ?case by auto
kleing@43158
    73
next
kleing@43158
    74
  case (Assign x a s)
kleing@43158
    75
  have [simp]: "t' = t(x := aval a t)" using Assign by auto
kleing@43158
    76
  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
kleing@43158
    77
  show ?case
kleing@43158
    78
  proof auto
kleing@43158
    79
    assume "sec x \<le> l"
kleing@43158
    80
    with `sec x >= sec_aexp a` have "sec_aexp a \<le> l" by arith
kleing@43158
    81
    thus "aval a s = aval a t"
kleing@43158
    82
      by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
kleing@43158
    83
  next
kleing@43158
    84
    fix y assume "y \<noteq> x" "sec y \<le> l"
kleing@43158
    85
    thus "s y = t y" using `s = t (\<le> l)` by simp
kleing@43158
    86
  qed
kleing@43158
    87
next
kleing@43158
    88
  case Semi thus ?case by blast
kleing@43158
    89
next
kleing@43158
    90
  case (IfTrue b s c1 s' c2)
kleing@43158
    91
  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
kleing@43158
    92
  show ?case
kleing@43158
    93
  proof cases
kleing@43158
    94
    assume "sec_bexp b \<le> l"
kleing@43158
    95
    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
kleing@43158
    96
    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
nipkow@45015
    97
    with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
kleing@43158
    98
    show ?thesis by auto
kleing@43158
    99
  next
kleing@43158
   100
    assume "\<not> sec_bexp b \<le> l"
kleing@43158
   101
    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
kleing@43158
   102
      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
kleing@43158
   103
    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   104
    have "s = s' (\<le> l)" by auto
kleing@43158
   105
    moreover
kleing@43158
   106
    from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   107
    have "t = t' (\<le> l)" by auto
kleing@43158
   108
    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
kleing@43158
   109
  qed
kleing@43158
   110
next
kleing@43158
   111
  case (IfFalse b s c2 s' c1)
kleing@43158
   112
  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems(2) by auto
kleing@43158
   113
  show ?case
kleing@43158
   114
  proof cases
kleing@43158
   115
    assume "sec_bexp b \<le> l"
kleing@43158
   116
    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
kleing@43158
   117
    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
nipkow@45015
   118
    with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
kleing@43158
   119
    show ?thesis by auto
kleing@43158
   120
  next
kleing@43158
   121
    assume "\<not> sec_bexp b \<le> l"
kleing@43158
   122
    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
kleing@43158
   123
      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
kleing@43158
   124
    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   125
    have "s = s' (\<le> l)" by auto
kleing@43158
   126
    moreover
kleing@43158
   127
    from confinement[OF IfFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   128
    have "t = t' (\<le> l)" by auto
kleing@43158
   129
    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
kleing@43158
   130
  qed
kleing@43158
   131
next
kleing@43158
   132
  case (WhileFalse b s c)
kleing@43158
   133
  have "sec_bexp b \<turnstile> c" using WhileFalse.prems(2) by auto
kleing@43158
   134
  show ?case
kleing@43158
   135
  proof cases
kleing@43158
   136
    assume "sec_bexp b \<le> l"
kleing@43158
   137
    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
kleing@43158
   138
    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
kleing@43158
   139
    with WhileFalse.prems(1,3) show ?thesis by auto
kleing@43158
   140
  next
kleing@43158
   141
    assume "\<not> sec_bexp b \<le> l"
kleing@43158
   142
    have 1: "sec_bexp b \<turnstile> WHILE b DO c"
kleing@43158
   143
      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
kleing@43158
   144
    from confinement[OF WhileFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   145
    have "t = t' (\<le> l)" by auto
kleing@43158
   146
    thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
kleing@43158
   147
  qed
kleing@43158
   148
next
kleing@43158
   149
  case (WhileTrue b s1 c s2 s3 t1 t3)
kleing@43158
   150
  let ?w = "WHILE b DO c"
kleing@43158
   151
  have "sec_bexp b \<turnstile> c" using WhileTrue.prems(2) by auto
kleing@43158
   152
  show ?case
kleing@43158
   153
  proof cases
kleing@43158
   154
    assume "sec_bexp b \<le> l"
kleing@43158
   155
    hence "s1 = t1 (\<le> sec_bexp b)" using `s1 = t1 (\<le> l)` by auto
kleing@43158
   156
    hence "bval b t1"
kleing@43158
   157
      using `bval b s1` by(simp add: bval_eq_if_eq_le)
kleing@43158
   158
    then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
kleing@43158
   159
      using `(?w,t1) \<Rightarrow> t3` by auto
nipkow@45015
   160
    from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
nipkow@45015
   161
      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
kleing@43158
   162
        `s1 = t1 (\<le> l)`]]
kleing@43158
   163
    show ?thesis by simp
kleing@43158
   164
  next
kleing@43158
   165
    assume "\<not> sec_bexp b \<le> l"
kleing@43158
   166
    have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
nipkow@45015
   167
    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   168
    have "s1 = s3 (\<le> l)" by auto
kleing@43158
   169
    moreover
kleing@43158
   170
    from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
kleing@43158
   171
    have "t1 = t3 (\<le> l)" by auto
kleing@43158
   172
    ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
kleing@43158
   173
  qed
kleing@43158
   174
qed
kleing@43158
   175
kleing@43158
   176
kleing@43158
   177
subsection "The Standard Typing System"
kleing@43158
   178
kleing@43158
   179
text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
kleing@43158
   180
standard formulation, however, is slightly different, replacing the maximum
kleing@43158
   181
computation by an antimonotonicity rule. We introduce the standard system now
kleing@43158
   182
and show the equivalence with our formulation. *}
kleing@43158
   183
kleing@43158
   184
inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
kleing@43158
   185
Skip':
kleing@43158
   186
  "l \<turnstile>' SKIP" |
kleing@43158
   187
Assign':
kleing@43158
   188
  "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
kleing@43158
   189
Semi':
kleing@43158
   190
  "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
kleing@43158
   191
If':
kleing@43158
   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" |
kleing@43158
   193
While':
kleing@43158
   194
  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
kleing@43158
   195
anti_mono':
kleing@43158
   196
  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
kleing@43158
   197
kleing@43158
   198
lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
nipkow@45015
   199
apply(induction rule: sec_type.induct)
kleing@43158
   200
apply (metis Skip')
kleing@43158
   201
apply (metis Assign')
kleing@43158
   202
apply (metis Semi')
kleing@43158
   203
apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
kleing@43158
   204
by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
kleing@43158
   205
kleing@43158
   206
kleing@43158
   207
lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
nipkow@45015
   208
apply(induction rule: sec_type'.induct)
kleing@43158
   209
apply (metis Skip)
kleing@43158
   210
apply (metis Assign)
kleing@43158
   211
apply (metis Semi)
kleing@43158
   212
apply (metis min_max.sup_absorb2 If)
kleing@43158
   213
apply (metis min_max.sup_absorb2 While)
kleing@43158
   214
by (metis anti_mono)
kleing@43158
   215
kleing@43158
   216
subsection "A Bottom-Up Typing System"
kleing@43158
   217
kleing@43158
   218
inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
kleing@43158
   219
Skip2:
kleing@43158
   220
  "\<turnstile> SKIP : l" |
kleing@43158
   221
Assign2:
kleing@43158
   222
  "sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
kleing@43158
   223
Semi2:
kleing@43158
   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 " |
kleing@43158
   225
If2:
kleing@43158
   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>
kleing@43158
   227
  \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
kleing@43158
   228
While2:
kleing@43158
   229
  "\<lbrakk> sec_bexp b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
kleing@43158
   230
kleing@43158
   231
kleing@43158
   232
lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
nipkow@45015
   233
apply(induction rule: sec_type2.induct)
kleing@43158
   234
apply (metis Skip')
kleing@43158
   235
apply (metis Assign' eq_imp_le)
kleing@43158
   236
apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
kleing@43158
   237
apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
kleing@43158
   238
by (metis While')
kleing@43158
   239
kleing@43158
   240
lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
nipkow@45015
   241
apply(induction rule: sec_type'.induct)
kleing@43158
   242
apply (metis Skip2 le_refl)
kleing@43158
   243
apply (metis Assign2)
kleing@43158
   244
apply (metis Semi2 min_max.inf_greatest)
kleing@43158
   245
apply (metis If2 inf_greatest inf_nat_def le_trans)
kleing@43158
   246
apply (metis While2 le_trans)
kleing@43158
   247
by (metis le_trans)
kleing@43158
   248
kleing@43158
   249
end