Theory Concrete

section ‹Concrete setting›

theory Concrete
imports Syntactic_Criteria
begin

(* We instatiate the parameters according to Examples 1 and 2 from the paper. *)

(* Security levels: *)
datatype level = Lo | Hi

lemma [simp]: "⋀ l. l ≠ Hi ⟷ l = Lo" and
      [simp]: "⋀ l. Hi ≠ l ⟷ Lo = l" and
      [simp]: "⋀ l. l ≠ Lo ⟷ l = Hi" and
      [simp]: "⋀ l. Lo ≠ l ⟷ Hi = l"
by (metis level.exhaust level.simps(2))+

lemma [dest]: "⋀ l A. ⟦l ∈ A; Lo ∉ A⟧ ⟹ l = Hi" and
      [dest]: "⋀ l A. ⟦l ∈ A; Hi ∉ A⟧ ⟹ l = Lo"
by (metis level.exhaust)+

declare level.split[split]

instantiation level :: complete_lattice
begin
  definition top_level: "top ≡ Hi"
  definition bot_level: "bot ≡ Lo"
  definition inf_level: "inf l1 l2 ≡ if Lo ∈ {l1,l2} then Lo else Hi"
  definition sup_level: "sup l1 l2 ≡ if Hi ∈ {l1,l2} then Hi else Lo"
  definition less_eq_level: "less_eq l1 l2 ≡ (l1 = Lo ∨ l2 = Hi)"
  definition less_level: "less l1 l2 ≡ l1 = Lo ∧ l2 = Hi"
  definition Inf_level: "Inf L ≡ if Lo ∈ L then Lo else Hi"
  definition Sup_level: "Sup L ≡ if Hi ∈ L then Hi else Lo"
instance
  proof qed (auto simp: top_level bot_level inf_level sup_level
                        less_eq_level less_level Inf_level Sup_level)
end

lemma sup_eq_Lo[simp]: "sup a b = Lo ⟷ a = Lo ∧ b = Lo"
  by (auto simp: sup_level)

datatype var = h | h' | l | l'
datatype exp = Ct nat | Var var | Plus exp exp | Minus exp exp
datatype test = Tr | Eq exp exp | Gt exp exp | Non test
datatype atom = Assign var exp
type_synonym choice = "real + test"
type_synonym state = "var ⇒ nat"

syntax
 "_assign" :: "'a ⇒ 'a ⇒ 'a"  (‹_ ::= _› [1000, 61] 61)

syntax_consts
  "_assign" == Assign

translations
  "x ::= expr" == "CONST Atm (CONST Assign x expr)"

primrec sec where
  "sec h  = Hi"
| "sec h' = Hi"
| "sec l  = Lo"
| "sec l' = Lo"

fun eval where
 "eval (Ct n) s = n"
|"eval (Var x) s = s x"
|"eval (Plus e1 e2) s = eval e1 s + eval e2 s"
|"eval (Minus e1 e2) s = eval e1 s - eval e2 s"

fun tval where
 "tval Tr s = True"
|"tval (Eq e1 e2) s = (eval e1 s = eval e2 s)"
|"tval (Gt e1 e2) s = (eval e1 s > eval e2 s)"
|"tval (Non e) s = (¬ tval e s)"

fun aval where
"aval (Assign x e) s = (s (x := eval e s))"

fun cval where
 "cval (Inl p) s = min 1 (max 0 p)"
|"cval (Inr tst) s = (if tval tst s then 1 else 0)"

definition indis :: "(state * state) set"where
"indis ≡ {(s,t). ALL x. sec x = Lo ⟶ s x = t x}"

interpretation Example_PL: PL_Indis aval tval cval indis
proof
  fix ch :: choice and  s show "0 ≤ cval ch s ∧ cval ch s ≤ 1"
    by (cases ch) auto
next
  show "equiv UNIV indis"
    unfolding refl_on_def sym_def trans_def equiv_def indis_def by auto
qed

(* The security level of expressions: *)
fun exprSec where
 "exprSec (Ct n) = Lo"
|"exprSec (Var x) = sec x"
|"exprSec (Plus e1 e2) = sup (exprSec e1) (exprSec e2)"
|"exprSec (Minus e1 e2) = sup (exprSec e1) (exprSec e2)"

(* The security level of tests: *)
fun tstSec where
 "tstSec Tr = Lo"
|"tstSec (Eq e1 e2) = sup (exprSec e1) (exprSec e2)"
|"tstSec (Gt e1 e2) = sup (exprSec e1) (exprSec e2)"
|"tstSec (Non e) = tstSec e"

lemma exprSec_Lo_eval_eq: "exprSec expr = Lo ⟹ (s, t) ∈ indis ⟹ eval expr s = eval expr t"
  by (induct expr) (auto simp: indis_def)

lemma compatAtmSyntactic[simp]: "exprSec expr = Lo ∨ sec v = Hi ⟹ Example_PL.compatAtm (Assign v expr)"
  unfolding Example_PL.compatAtm_def
  by (induct expr)
     (auto simp: indis_def intro!: arg_cong2[where f="(+)"] arg_cong2[where f="(-)"] exprSec_Lo_eval_eq)

lemma presAtmSyntactic[simp]: "sec v = Hi ⟹ Example_PL.presAtm (Assign v expr)"
  unfolding Example_PL.presAtm_def by (simp add: indis_def)

lemma compatTstSyntactic[simp]: "tstSec tst = Lo ⟹ Example_PL.compatTst tst"
  unfolding Example_PL.compatTst_def
  by (induct tst)
     (simp_all, safe del: iffI
              intro!: arg_cong2[where f="(=)"] arg_cong2[where f="(<) :: nat ⇒ nat ⇒ bool"] exprSec_Lo_eval_eq)

(* Stateless choices are always compatible: *)
lemma compatPrchSyntactic[simp]: "Example_PL.compatCh (Inl p)"
  unfolding Example_PL.compatCh_def by auto

(* A test-choice is compatible iff its test is compatible: *)
lemma compatIfchSyntactic[simp]: "Example_PL.compatCh (Inr tst) ⟷ Example_PL.compatTst tst"
  unfolding Example_PL.compatCh_def Example_PL.compatTst_def by auto

abbreviation Ch_half (‹Ch½›) where "Ch½ ≡ Ch (Inl (1/2))"
abbreviation If where "If tst ≡ Ch (Inr tst)"

abbreviation "siso c ≡ Example_PL.siso c"
abbreviation "discr c ≡ Example_PL.discr c"
abbreviation Sbis_abbrev (infix ‹≈s› 55) where "c1 ≈s c2 ≡ (c1,c2) ∈ Example_PL.Sbis"
abbreviation ZObis_abbrev (infix ‹≈01› 55) where "c1 ≈01 c2 ≡ (c1,c2) ∈ Example_PL.ZObis"

abbreviation "SC_siso c ≡ Example_PL.SC_siso c"
abbreviation "SC_discr c ≡ Example_PL.SC_discr c"
abbreviation "SC_Sbis c ≡ Example_PL.SC_Sbis c"
abbreviation "SC_ZObis c ≡ Example_PL.SC_ZObis c"

lemma "SC_discr (h ::= Ct 0)"
  by (simp add: Example_PL.SC_discr.simps)


subsection ‹The secure programs from the paper's Example 3›

definition [simp]: "d0 =
  h' ::= Ct 0 ;;
  While (Gt (Var h) (Ct 0))
    (Ch½ (h ::= Ct 0)
         (h' ::= Plus (Var h') (Ct 1)))"

definition [simp]: "d1 =
  While (Gt (Var h) (Ct 0))
    (Ch½ (h ::= Minus (Var h) (Ct 1))
         (h ::= Plus (Var h) (Ct 1)))"

definition [simp]: "d2 =
  If (Eq (Var l) (Ct 0))
    (l' ::= Ct 1)
    d0"

definition [simp]: "d3 =
  h ::= Ct 5 ;;
  ParT [d0, (l ::= Ct 1)]"

(* The syntactic criteria are checked automatically: *)
theorem "SC_discr d0"
        "SC_discr d1"
        "SC_Sbis d2"
        "SC_ZObis d2"
  by (auto simp: Example_PL.SC_discr.simps Example_PL.SC_Sbis.simps Example_PL.SC_ZObis.simps)

(* Alternatively, the semantic notions follow directly from the compositionality facts
used as intro rules: *)
theorem "discr d0"
        "discr d1"
        "d2 ≈s d2"
        "d3 ≈01 d3"
  by (auto intro!: compatAtmSyntactic
                   Example_PL.ZObis Example_PL.proper_intros
                   Example_PL.Atm_Sbis)


end