Theory Preliminaries

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
header {* Preliminaries *}
theory Preliminaries
imports Main "~~/src/HOL/Library/Lattice_Syntax"
begin

text {* Possible modes for variables: *}
datatype Mode = AsmNoRead | AsmNoWrite | GuarNoRead | GuarNoWrite

text {* We consider a two-element security lattice: *}
datatype Sec = High | Low

notation
  less_eq  (infix "\<sqsubseteq>" 50) and
  less  (infix "\<sqsubset>" 50)

text {* @{term Sec} forms a (complete) lattice: *}
instantiation Sec :: complete_lattice
begin

definition top_Sec_def: "\<top> = High"
definition sup_Sec_def: "d1 \<squnion> d2 = (if (d1 = High ∨ d2 = High) then High else Low)"
definition inf_Sec_def: "d1 \<sqinter> d2 = (if (d1 = Low ∨ d2 = Low) then Low else High)"
definition bot_Sec_def: "⊥ = Low"
definition less_eq_Sec_def: "d1 ≤ d2 = (d1 = d2 ∨ d1 = Low)"
definition less_Sec_def: "d1 < d2 = (d1 = Low ∧ d2 = High)"
definition Sup_Sec_def: "\<Squnion>S = (if (High ∈ S) then High else Low)"
definition Inf_Sec_def: "\<Sqinter>S = (if (Low ∈ S) then Low else High)"

instance
  apply (intro_classes)
  apply (metis Sec.exhaust Sec.simps(2) less_Sec_def less_eq_Sec_def)
  apply (metis less_eq_Sec_def)
  apply (metis less_eq_Sec_def)
  apply (metis less_eq_Sec_def)
  apply (metis Sec.exhaust inf_Sec_def less_eq_Sec_def)
  apply (metis Sec.exhaust inf_Sec_def less_eq_Sec_def)
  apply (metis Sec.exhaust inf_Sec_def less_eq_Sec_def)
  apply (metis Sec.exhaust less_eq_Sec_def sup_Sec_def)
  apply (metis Sec.exhaust less_eq_Sec_def sup_Sec_def)
  apply (metis Sec.exhaust Sec.simps(2) less_eq_Sec_def sup_Sec_def)
  apply (metis (full_types) Inf_Sec_def Sec.exhaust less_eq_Sec_def)
  apply (metis Inf_Sec_def Sec.exhaust less_eq_Sec_def)
  apply (metis Sec.exhaust Sup_Sec_def less_eq_Sec_def)
  apply (metis (full_types) Sup_Sec_def less_eq_Sec_def)
  apply (metis (hide_lams, mono_tags) Inf_Sec_def empty_iff top_Sec_def)
  by (metis (hide_lams, mono_tags) Sup_Sec_def bot_Sec_def empty_iff)
end

text {* Memories are mappings from variables to values *}
type_synonym ('var, 'val) Mem = "'var => 'val"

text {* A mode state maps modes to the set of variables for which the
  given mode is set. *}
type_synonym 'var Mds = "Mode => 'var set"

text {* Local configurations: *}
type_synonym ('com, 'var, 'val) LocalConf = "('com × 'var Mds) × ('var, 'val) Mem"

text {* Global configurations: *}
type_synonym ('com, 'var, 'val) GlobalConf = "('com × 'var Mds) list × ('var, 'val) Mem"

text {* A locale to fix various parametric components in Mantel et. al, and assumptions
  about them: *}
locale sifum_security =
  fixes dma :: "'Var => Sec"
  fixes stop :: "'Com"
  fixes eval :: "('Com, 'Var, 'Val) LocalConf rel"
  fixes some_val :: "'Val"
  fixes some_val' :: "'Val"
  assumes stop_no_eval: "¬ ((((stop, mds), mem), ((c', mds'), mem')) ∈ eval)"
  assumes deterministic: "[| (lc, lc') ∈ eval; (lc, lc'') ∈ eval |] ==> lc' = lc''"
  assumes finite_memory: "finite {(x::'Var). True}"
  assumes different_values: "some_val ≠ some_val'"

end