Theory Preliminaries
section ‹Preliminaries›
theory Preliminaries
imports Main
begin
text ‹Possible modes for variables:›
datatype Mode = AsmNoReadOrWrite | AsmNoWrite | GuarNoReadOrWrite | GuarNoWrite
text ‹We consider a two-element security lattice:›
datatype Sec = High | Low
text ‹@{term Sec} forms a (complete) lattice:›
instantiation Sec :: complete_lattice
begin
definition top_Sec_def: "top = High"
definition sup_Sec_def: "sup d1 d2 = (if (d1 = High ∨ d2 = High) then High else Low)"
definition inf_Sec_def: "inf d1 d2 = (if (d1 = Low ∨ d2 = Low) then Low else High)"
definition bot_Sec_def: "bot = 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: "Sup S = (if (High ∈ S) then High else Low)"
definition Inf_Sec_def: "Inf S = (if (Low ∈ S) then Low else High)"
instance
apply (intro_classes)
using Sec.exhaust less_Sec_def less_eq_Sec_def inf_Sec_def sup_Sec_def apply auto[10]
apply (metis Inf_Sec_def Sec.exhaust less_eq_Sec_def)
apply (metis Inf_Sec_def Sec.exhaust less_eq_Sec_def)
using Sec.exhaust less_Sec_def less_eq_Sec_def inf_Sec_def sup_Sec_def Inf_Sec_def Sup_Sec_def top_Sec_def bot_Sec_def
by auto
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_init =
fixes dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
fixes 𝒞_vars :: "'Var ⇒ 'Var set"
fixes 𝒞 :: "'Var set"
fixes eval :: "('Com, 'Var, 'Val) LocalConf rel"
fixes some_val :: "'Val"
fixes INIT :: "('Var,'Val) Mem ⇒ bool"
assumes deterministic: "⟦ (lc, lc') ∈ eval; (lc, lc'') ∈ eval ⟧ ⟹ lc' = lc''"
assumes finite_memory: "finite {(x::'Var). True}"
defines "𝒞 ≡ ⋃x. 𝒞_vars x"
assumes 𝒞_vars_𝒞: "x ∈ 𝒞 ⟹ 𝒞_vars x = {}"
assumes dma_𝒞_vars: "∀x∈𝒞_vars y. mem⇩1 x = mem⇩2 x ⟹ dma mem⇩1 y = dma mem⇩2 y"
assumes 𝒞_Low: "∀x∈𝒞. dma mem x = Low"
locale sifum_security = sifum_security_init dma 𝒞_vars 𝒞 eval some_val "λ_.True"
for dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
and 𝒞_vars :: "'Var ⇒ 'Var set"
and 𝒞 :: "'Var set"
and eval :: "('Com, 'Var, 'Val) LocalConf rel"
and some_val :: "'Val"
context sifum_security_init begin
lemma 𝒞_vars_subset_𝒞:
"𝒞_vars x ⊆ 𝒞"
by(force simp: 𝒞_def)
lemma dma_𝒞:
"∀x∈𝒞. mem⇩1 x = mem⇩2 x ⟹ dma mem⇩1 = dma mem⇩2"
proof
fix y
assume "∀x∈𝒞. mem⇩1 x = mem⇩2 x"
hence "∀x∈𝒞_vars y. mem⇩1 x = mem⇩2 x"
using 𝒞_vars_subset_𝒞 by blast
thus "dma mem⇩1 y = dma mem⇩2 y"
by(rule dma_𝒞_vars)
qed
end
lemma my_trancl_induct [consumes 1, case_names base step]:
"⟦(a, b) ∈ r⇧+;
P a ;
⋀x y. ⟦(x, y) ∈ r; P x⟧ ⟹ P y⟧ ⟹ P b"
by (induct rule: trancl.induct, blast+)
lemma my_trancl_step_induct [consumes 1, case_names base step]:
"⟦(a, b) ∈ r⇧+;
⋀x y. (x, y) ∈ r ⟹ P x y;
⋀x y z. P x y ⟹ (y, z) ∈ r ⟹ P x z⟧ ⟹ P a b"
by (induct rule: trancl_induct, blast+)
lemma my_trancl_big_step_induct [consumes 1, case_names base step]:
"⟦(a, b) ∈ r⇧+;
⋀x y. (x, y) ∈ r ⟹ P x y;
⋀x y z. (x, y) ∈ r⇧+ ⟹ P x y ⟹ (y, z) ∈ r ⟹ P y z ⟹ P x z⟧ ⟹ P a b"
by (induct rule: trancl.induct, blast+)
lemmas my_trancl_step_induct3 =
my_trancl_step_induct[of "((ax,ay), az)" "((bx,by), bz)", split_format (complete),
consumes 1, case_names step]
lemmas my_trancl_big_step_induct3 =
my_trancl_big_step_induct[of "((ax,ay), az)" "((bx,by), bz)", split_format (complete),
consumes 1, case_names base step]
end