src/HOL/IMP/Sec_Typing.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 54864 a064732223ad
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
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:
nipkow@50342
    12
  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
nipkow@47818
    13
Seq:
wenzelm@53015
    14
  "\<lbrakk> l \<turnstile> c\<^sub>1;  l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^sub>1;;c\<^sub>2" |
kleing@43158
    15
If:
wenzelm@53015
    16
  "\<lbrakk> max (sec b) l \<turnstile> c\<^sub>1;  max (sec b) l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
kleing@43158
    17
While:
nipkow@50342
    18
  "max (sec 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!]:
wenzelm@53015
    27
  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^sub>1;;c\<^sub>2"  "l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>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
nipkow@47818
    47
  case Seq thus ?case by auto
kleing@43158
    48
next
kleing@43158
    49
  case (IfTrue b s c1)
nipkow@50342
    50
  hence "max (sec b) l \<turnstile> c1" by auto
haftmann@54863
    51
  hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
nipkow@45015
    52
  thus ?case using IfTrue.IH by metis
kleing@43158
    53
next
kleing@43158
    54
  case (IfFalse b s c2)
nipkow@50342
    55
  hence "max (sec b) l \<turnstile> c2" by auto
haftmann@54863
    56
  hence "l \<turnstile> c2" by (metis max.cobounded2 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)
nipkow@50342
    62
  hence "max (sec b) l \<turnstile> c" by auto
haftmann@54863
    63
  hence "l \<turnstile> c" by (metis max.cobounded2 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
nipkow@50342
    76
  have "sec x >= sec 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"
nipkow@50342
    80
    with `sec x >= sec a` have "sec 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
nipkow@47818
    88
  case Seq thus ?case by blast
kleing@43158
    89
next
kleing@43158
    90
  case (IfTrue b s c1 s' c2)
nipkow@52382
    91
  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
kleing@43158
    92
  show ?case
kleing@43158
    93
  proof cases
nipkow@50342
    94
    assume "sec b \<le> l"
nipkow@50342
    95
    hence "s = t (\<le> sec 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@50342
    97
    with IfTrue.IH IfTrue.prems(1,3) `sec b \<turnstile> c1`  anti_mono
kleing@43158
    98
    show ?thesis by auto
kleing@43158
    99
  next
nipkow@50342
   100
    assume "\<not> sec b \<le> l"
nipkow@50342
   101
    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
nipkow@50342
   102
      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
nipkow@52382
   103
    from confinement[OF `(c1, s) \<Rightarrow> s'` `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
kleing@43158
   104
    have "s = s' (\<le> l)" by auto
kleing@43158
   105
    moreover
nipkow@52382
   106
    from confinement[OF `(IF b THEN c1 ELSE c2, t) \<Rightarrow> t'` 1] `\<not> sec 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)
nipkow@52382
   112
  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
kleing@43158
   113
  show ?case
kleing@43158
   114
  proof cases
nipkow@50342
   115
    assume "sec b \<le> l"
nipkow@50342
   116
    hence "s = t (\<le> sec 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@50342
   118
    with IfFalse.IH IfFalse.prems(1,3) `sec b \<turnstile> c2` anti_mono
kleing@43158
   119
    show ?thesis by auto
kleing@43158
   120
  next
nipkow@50342
   121
    assume "\<not> sec b \<le> l"
nipkow@50342
   122
    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
nipkow@50342
   123
      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
nipkow@50342
   124
    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
kleing@43158
   125
    have "s = s' (\<le> l)" by auto
kleing@43158
   126
    moreover
nipkow@52382
   127
    from confinement[OF `(IF b THEN c1 ELSE c2, t) \<Rightarrow> t'` 1] `\<not> sec 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)
nipkow@50342
   133
  have "sec b \<turnstile> c" using WhileFalse.prems(2) by auto
kleing@43158
   134
  show ?case
kleing@43158
   135
  proof cases
nipkow@50342
   136
    assume "sec b \<le> l"
nipkow@50342
   137
    hence "s = t (\<le> sec 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
nipkow@50342
   141
    assume "\<not> sec b \<le> l"
nipkow@50342
   142
    have 1: "sec b \<turnstile> WHILE b DO c"
nipkow@50342
   143
      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
nipkow@52382
   144
    from confinement[OF `(WHILE b DO c, t) \<Rightarrow> t'` 1] `\<not> sec 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"
nipkow@52382
   151
  have "sec b \<turnstile> c" using `0 \<turnstile> WHILE b DO c` by auto
kleing@43158
   152
  show ?case
kleing@43158
   153
  proof cases
nipkow@50342
   154
    assume "sec b \<le> l"
nipkow@50342
   155
    hence "s1 = t1 (\<le> sec 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@50342
   161
      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec b \<turnstile> c`]
kleing@43158
   162
        `s1 = t1 (\<le> l)`]]
kleing@43158
   163
    show ?thesis by simp
kleing@43158
   164
  next
nipkow@50342
   165
    assume "\<not> sec b \<le> l"
nipkow@50342
   166
    have 1: "sec b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
nipkow@50342
   167
    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec b \<le> l`
kleing@43158
   168
    have "s1 = s3 (\<le> l)" by auto
kleing@43158
   169
    moreover
nipkow@52382
   170
    from confinement[OF `(WHILE b DO c, t1) \<Rightarrow> t3` 1] `\<not> sec 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':
nipkow@50342
   188
  "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
nipkow@47818
   189
Seq':
wenzelm@53015
   190
  "\<lbrakk> l \<turnstile>' c\<^sub>1;  l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^sub>1;;c\<^sub>2" |
kleing@43158
   191
If':
wenzelm@53015
   192
  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^sub>1;  l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
kleing@43158
   193
While':
nipkow@50342
   194
  "\<lbrakk> sec 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')
nipkow@47818
   202
apply (metis Seq')
haftmann@54864
   203
apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
haftmann@54863
   204
by (metis less_or_eq_imp_le max.absorb1 max.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)
nipkow@47818
   211
apply (metis Seq)
haftmann@54863
   212
apply (metis max.absorb2 If)
haftmann@54863
   213
apply (metis max.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:
nipkow@50342
   222
  "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
nipkow@47818
   223
Seq2:
wenzelm@53015
   224
  "\<lbrakk> \<turnstile> c\<^sub>1 : l\<^sub>1;  \<turnstile> c\<^sub>2 : l\<^sub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^sub>1;;c\<^sub>2 : min l\<^sub>1 l\<^sub>2 " |
kleing@43158
   225
If2:
wenzelm@53015
   226
  "\<lbrakk> sec b \<le> min l\<^sub>1 l\<^sub>2;  \<turnstile> c\<^sub>1 : l\<^sub>1;  \<turnstile> c\<^sub>2 : l\<^sub>2 \<rbrakk>
wenzelm@53015
   227
  \<Longrightarrow> \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2 : min l\<^sub>1 l\<^sub>2" |
kleing@43158
   228
While2:
nipkow@50342
   229
  "\<lbrakk> sec 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)
haftmann@54863
   236
apply (metis Seq' anti_mono' min.cobounded1 min.cobounded2)
haftmann@54863
   237
apply (metis If' anti_mono' min.absorb2 min.absorb_iff1 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)
haftmann@54863
   244
apply (metis Seq2 min.boundedI)
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