Theory Preliminaries

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
section ‹Preliminaries›
theory Preliminaries
imports Main
begin

unbundle lattice_syntax

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 "⊑" 50) and
  less  (infix "⊏" 50)

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

definition top_Sec_def: "⊤ = High"
definition sup_Sec_def: "d1 ⊔ d2 = (if (d1 = High ∨ d2 = High) then High else Low)"
definition inf_Sec_def: "d1 ⊓ 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: "⨆S = (if (High ∈ S) then High else Low)"
definition Inf_Sec_def: "⨅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 (opaque_lifting, mono_tags) Inf_Sec_def empty_iff top_Sec_def)
  by (metis (opaque_lifting, 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