Theory Monads
section ‹Basic Monad Theory for Sequential Computations›
theory
Monads
imports
Main
begin
subsection‹General Framework for Monad-based Sequence-Test›
text‹
As such, Higher-order Logic as a purely functional specification formalism has no built-in
mechanism for state and state-transitions. Forms of testing involving state require therefore
explicit mechanisms for their treatment inside the logic; a well-known technique to model
states inside purely functional languages are \emph{monads} made popular by Wadler and Moggi
and extensively used in Haskell. \HOL is powerful enough to represent the most important
standard monads; however, it is not possible to represent monads as such due to well-known
limitations of the Hindley-Milner type-system.
Here is a variant for state-exception monads, that models precisely transition functions with
preconditions. Next, we declare the state-backtrack-monad. In all of them, our concept of
i/o-stepping functions can be formulated; these are functions mapping input to a given monad.
Later on, we will build the usual concepts of:
\begin{enumerate}
\item deterministic i/o automata,
\item non-deterministic i/o automata, and
\item labelled transition systems (LTS)
\end{enumerate}
›
subsubsection‹State Exception Monads›
type_synonym ('o, 'σ) MON⇩S⇩E = "'σ ⇀ ('o × 'σ)"
definition bind_SE :: "('o,'σ)MON⇩S⇩E ⇒ ('o ⇒ ('o','σ)MON⇩S⇩E) ⇒ ('o','σ)MON⇩S⇩E"
where "bind_SE f g = (λσ. case f σ of None ⇒ None
| Some (out, σ') ⇒ g out σ')"
notation bind_SE ("bind⇩S⇩E")
syntax
"_bind_SE" :: "[pttrn,('o,'σ)MON⇩S⇩E,('o','σ)MON⇩S⇩E] ⇒ ('o','σ)MON⇩S⇩E"
("(2 _ ← _; _)" [5,8,8]8)
translations
"x ← f; g" ⇌ "CONST bind_SE f (% x . g)"
definition unit_SE :: "'o ⇒ ('o, 'σ)MON⇩S⇩E" ("(return _)" 8)
where "unit_SE e = (λσ. Some(e,σ))"
notation unit_SE ("unit⇩S⇩E")
definition fail⇩S⇩E :: "('o, 'σ)MON⇩S⇩E"
where "fail⇩S⇩E = (λσ. None)"
notation fail⇩S⇩E ("fail⇩S⇩E")
definition assert_SE :: "('σ ⇒ bool) ⇒ (bool, 'σ)MON⇩S⇩E"
where "assert_SE P = (λσ. if P σ then Some(True,σ) else None)"
notation assert_SE ("assert⇩S⇩E")
definition assume_SE :: "('σ ⇒ bool) ⇒ (unit, 'σ)MON⇩S⇩E"
where "assume_SE P = (λσ. if ∃σ . P σ then Some((), SOME σ . P σ) else None)"
notation assume_SE ("assume⇩S⇩E")
definition if_SE :: "['σ ⇒ bool, ('α, 'σ)MON⇩S⇩E, ('α, 'σ)MON⇩S⇩E] ⇒ ('α, 'σ)MON⇩S⇩E"
where "if_SE c E F = (λσ. if c σ then E σ else F σ)"
notation if_SE ("if⇩S⇩E")
text‹
The standard monad theorems about unit and associativity:
›
lemma bind_left_unit : "(x ← return a; k) = k"
apply (simp add: unit_SE_def bind_SE_def)
done
lemma bind_right_unit: "(x ← m; return x) = m"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
subgoal for "σ"
apply (case_tac "m σ")
apply ( simp_all)
done
done
lemma bind_assoc: "(y ← (x ← m; k); h) = (x ← m; (y ← k; h))"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
subgoal for "σ"
apply (case_tac "m σ", simp_all)
subgoal for a
apply (case_tac "a", simp_all)
done
done
done
text‹
In order to express test-sequences also on the object-level and to make our theory amenable to
formal reasoning over test-sequences, we represent them as lists of input and generalize the
bind-operator of the state-exception monad accordingly. The approach is straightforward, but
comes with a price: we have to encapsulate all input and output data into one type. Assume that
we have a typed interface to a module with the operations $op_1$, $op_2$, \ldots, $op_n$ with
the inputs $\iota_1$, $\iota_2$, \ldots, $\iota_n$ (outputs are treated analogously). Then we
can encode for this interface the general input - type:
\begin{displaymath}
\texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
\end{displaymath}
Obviously, we loose some type-safety in this approach; we have to express that in traces only
\emph{corresponding} input and output belonging to the same operation will occur; this form
of side-conditions have to be expressed inside \HOL. From the user perspective, this will not
make much difference, since junk-data resulting from too weak typing can be ruled out by adopted
front-ends.
›
text‹
In order to express test-sequences also on the object-level and to make our theory amenable to
formal reasoning over test-sequences, we represent them as lists of input and generalize the
bind-operator of the state-exception monad accordingly. Thus, the notion of test-sequence
is mapped to the notion of a \emph{computation}, a semantic notion; at times we will use
reifications of computations, \ie{} a data-type in order to make computation amenable to
case-splitting and meta-theoretic reasoning. To this end, we have to encapsulate all input
and output data into one type. Assume that we have a typed interface to a module with
the operations $op_1$, $op_2$, \ldots, $op_n$ with the inputs $\iota_1$, $\iota_2$, \ldots,
$\iota_n$ (outputs are treated analogously).
Then we can encode for this interface the general input - type:
\begin{displaymath}
\texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
\end{displaymath}
Obviously, we loose some type-safety in this approach; we have to express
that in traces only \emph{corresponding} input and output belonging to the
same operation will occur; this form of side-conditions have to be expressed
inside \HOL. From the user perspective, this will not make much difference,
since junk-data resulting from too weak typing can be ruled out by adopted
front-ends.›
text‹Note that the subsequent notion of a test-sequence allows the io stepping
function (and the special case of a program under test) to stop execution
\emph{within} the sequence; such premature terminations are characterized by an
output list which is shorter than the input list. Note that our primary
notion of multiple execution ignores failure and reports failure
steps only by missing results ...›
fun mbind :: "'ι list ⇒ ('ι ⇒ ('o,'σ) MON⇩S⇩E) ⇒ ('o list,'σ) MON⇩S⇩E"
where "mbind [] iostep σ = Some([], σ)" |
"mbind (a#H) iostep σ =
(case iostep a σ of
None ⇒ Some([], σ)
| Some (out, σ') ⇒ (case mbind H iostep σ' of
None ⇒ Some([out],σ')
| Some(outs,σ'') ⇒ Some(out#outs,σ'')))"
text‹As mentioned, this definition is fail-safe; in case of an exception,
the current state is maintained, no result is reported.
An alternative is the fail-strict variant ‹mbind'› defined below.›
lemma mbind_unit [simp]: "mbind [] f = (return [])"
by(rule ext, simp add: unit_SE_def)
lemma mbind_nofailure [simp]: "mbind S f σ ≠ None"
apply (rule_tac x=σ in spec)
apply (induct S)
using mbind.simps(1) apply force
apply(simp add:unit_SE_def)
apply(safe)[1]
subgoal for a S x
apply (case_tac "f a x")
apply(simp)
apply(safe)[1]
subgoal for aa b
apply (erule_tac x="b" in allE)
apply (erule exE)+
apply (simp)
done
done
done
text‹The fail-strict version of ‹mbind'› looks as follows:›
fun mbind' :: "'ι list ⇒ ('ι ⇒ ('o,'σ) MON⇩S⇩E) ⇒ ('o list,'σ) MON⇩S⇩E"
where "mbind' [] iostep σ = Some([], σ)" |
"mbind' (a#H) iostep σ =
(case iostep a σ of
None ⇒ None
| Some (out, σ') ⇒ (case mbind H iostep σ' of
None ⇒ None
| Some(outs,σ'') ⇒ Some(out#outs,σ'')))"
text‹
mbind' as failure strict operator can be seen as a foldr on bind---if the types would
match \ldots
›
definition try_SE :: "('o,'σ) MON⇩S⇩E ⇒ ('o option,'σ) MON⇩S⇩E"
where "try_SE ioprog = (λσ. case ioprog σ of
None ⇒ Some(None, σ)
| Some(outs, σ') ⇒ Some(Some outs, σ'))"
text‹In contrast @{term mbind} as a failure safe operator can roughly be seen
as a @{term foldr} on bind - try:
‹m1 ; try m2 ; try m3; ...›. Note, that the rough equivalence only holds for
certain predicates in the sequence - length equivalence modulo None,
for example. However, if a conditional is added, the equivalence
can be made precise:›
lemma mbind_try:
"(x ← mbind (a#S) F; M x) =
(a' ← try_SE(F a);
if a' = None
then (M [])
else (x ← mbind S F; M (the a' # x)))"
apply (rule ext)
apply (simp add: bind_SE_def try_SE_def)
subgoal for x
apply (case_tac "F a x")
apply(simp)
apply (safe)[1]
apply (simp add: bind_SE_def try_SE_def)
subgoal for aa b
apply (case_tac "mbind S F b")
apply (auto)
done
done
done
text‹On this basis, a symbolic evaluation scheme can be established
that reduces @{term mbind}-code to @{term try_SE}-code and If-cascades.›
definition alt_SE :: "[('o, 'σ)MON⇩S⇩E, ('o, 'σ)MON⇩S⇩E] ⇒ ('o, 'σ)MON⇩S⇩E" (infixl "⊓⇩S⇩E" 10)
where "(f ⊓⇩S⇩E g) = (λ σ. case f σ of None ⇒ g σ
| Some H ⇒ Some H)"
definition malt_SE :: "('o, 'σ)MON⇩S⇩E list ⇒ ('o, 'σ)MON⇩S⇩E"
where "malt_SE S = foldr alt_SE S fail⇩S⇩E"
notation malt_SE ("⨅⇩S⇩E")
lemma malt_SE_mt [simp]: "⨅⇩S⇩E [] = fail⇩S⇩E"
by(simp add: malt_SE_def)
lemma malt_SE_cons [simp]: "⨅⇩S⇩E (a # S) = (a ⊓⇩S⇩E (⨅⇩S⇩E S))"
by(simp add: malt_SE_def)
subsubsection‹State-Backtrack Monads›
text‹This subsection is still rudimentary and as such an interesting
formal analogue to the previous monad definitions. It is doubtful that it is
interesting for testing and as a computational structure at all.
Clearly more relevant is ``sequence'' instead of ``set,'' which would
rephrase Isabelle's internal tactic concept.
›
type_synonym ('o, 'σ) MON⇩S⇩B = "'σ ⇒ ('o × 'σ) set"
definition bind_SB :: "('o, 'σ)MON⇩S⇩B ⇒ ('o ⇒ ('o', 'σ)MON⇩S⇩B) ⇒ ('o', 'σ)MON⇩S⇩B"
where "bind_SB f g σ = ⋃ ((λ(out, σ). (g out σ)) ` (f σ))"
notation bind_SB ("bind⇩S⇩B")
definition unit_SB :: "'o ⇒ ('o, 'σ)MON⇩S⇩B" ("(returns _)" 8)
where "unit_SB e = (λσ. {(e,σ)})"
notation unit_SB ("unit⇩S⇩B")
syntax "_bind_SB" :: "[pttrn,('o,'σ)MON⇩S⇩B,('o','σ)MON⇩S⇩B] ⇒ ('o','σ)MON⇩S⇩B"
("(2 _ := _; _)" [5,8,8]8)
translations
"x := f; g" ⇌ "CONST bind_SB f (% x . g)"
lemma bind_left_unit_SB : "(x := returns a; m) = m"
apply (rule ext)
apply (simp add: unit_SB_def bind_SB_def)
done
lemma bind_right_unit_SB: "(x := m; returns x) = m"
apply (rule ext)
apply (simp add: unit_SB_def bind_SB_def)
done
lemma bind_assoc_SB: "(y := (x := m; k); h) = (x := m; (y := k; h))"
apply (rule ext)
apply (simp add: unit_SB_def bind_SB_def split_def)
done
subsubsection‹State Backtrack Exception Monad›
text‹
The following combination of the previous two Monad-Constructions allows for the semantic
foundation of a simple generic assertion language in the style of Schirmer's Simpl-Language or
Rustan Leino's Boogie-PL language. The key is to use the exceptional element None for violations
of the assert-statement.
›
type_synonym ('o, 'σ) MON⇩S⇩B⇩E = "'σ ⇒ (('o × 'σ) set) option"
definition bind_SBE :: "('o,'σ)MON⇩S⇩B⇩E ⇒ ('o ⇒ ('o','σ)MON⇩S⇩B⇩E) ⇒ ('o','σ)MON⇩S⇩B⇩E"
where "bind_SBE f g = (λσ. case f σ of None ⇒ None
| Some S ⇒ (let S' = (λ(out, σ'). g out σ') ` S
in if None ∈ S' then None
else Some(⋃ (the ` S'))))"
syntax "_bind_SBE" :: "[pttrn,('o,'σ)MON⇩S⇩B⇩E,('o','σ)MON⇩S⇩B⇩E] ⇒ ('o','σ)MON⇩S⇩B⇩E"
("(2 _ :≡ _; _)" [5,8,8]8)
translations
"x :≡ f; g" ⇌ "CONST bind_SBE f (% x . g)"
definition unit_SBE :: "'o ⇒ ('o, 'σ)MON⇩S⇩B⇩E" ("(returning _)" 8)
where "unit_SBE e = (λσ. Some({(e,σ)}))"
definition assert_SBE :: "('σ ⇒ bool) ⇒ (unit, 'σ)MON⇩S⇩B⇩E"
where "assert_SBE e = (λσ. if e σ then Some({((),σ)})
else None)"
notation assert_SBE ("assert⇩S⇩B⇩E")
definition assume_SBE :: "('σ ⇒ bool) ⇒ (unit, 'σ)MON⇩S⇩B⇩E"
where "assume_SBE e = (λσ. if e σ then Some({((),σ)})
else Some {})"
notation assume_SBE ("assume⇩S⇩B⇩E")
definition havoc_SBE :: " (unit, 'σ)MON⇩S⇩B⇩E"
where "havoc_SBE = (λσ. Some({x. True}))"
notation havoc_SBE ("havoc⇩S⇩B⇩E")
lemma bind_left_unit_SBE : "(x :≡ returning a; m) = m"
apply (rule ext)
apply (simp add: unit_SBE_def bind_SBE_def)
done
lemma bind_right_unit_SBE: "(x :≡ m; returning x) = m"
apply (rule ext)
apply (simp add: unit_SBE_def bind_SBE_def)
subgoal for x
apply (case_tac "m x")
apply (simp_all add:Let_def)
apply (rule HOL.ccontr)
apply (simp add: Set.image_iff)
done
done
lemmas aux = trans[OF HOL.neq_commute,OF Option.not_None_eq]
lemma bind_assoc_SBE: "(y :≡ (x :≡ m; k); h) = (x :≡ m; (y :≡ k; h))"
proof (rule ext, simp add: unit_SBE_def bind_SBE_def, rename_tac x,
case_tac "m x", simp_all add: Let_def Set.image_iff, safe,goal_cases)
case (1 x a aa b ab ba a b)
then show ?case by(rule_tac x="(a, b)" in bexI, simp_all)
next
case (2 x a aa b ab ba)
then show ?case
apply (rule_tac x="(aa, b)" in bexI, simp_all add:split_def)
apply (erule_tac x="(aa,b)" in ballE)
apply (auto simp: aux image_def split_def intro!: rev_bexI)
done
next
case (3 x a a b)
then show ?case by(rule_tac x="(a, b)" in bexI, simp_all)
next
case (4 x a aa b)
then show ?case
apply (erule_tac Q="None = X" for X in contrapos_pp)
apply (erule_tac x="(aa,b)" and P="λ x. None ≠ case_prod (λout. k) x" in ballE)
apply (auto simp: aux image_def split_def intro!: rev_bexI)
done
next
case (5 x a aa b ab ba a b)
then show ?case apply simp apply ((erule_tac x="(ab,ba)" in ballE)+)
apply (simp_all add: aux, (erule exE)+, simp add:split_def)
apply (erule rev_bexI, case_tac "None∈(λp. h(snd p))`y",auto simp:split_def)
done
next
case (6 x a aa b a b)
then show ?case apply simp apply ((erule_tac x="(a,b)" in ballE)+)
apply (simp_all add: aux, (erule exE)+, simp add:split_def)
apply (erule rev_bexI, case_tac "None∈(λp. h(snd p))`y",auto simp:split_def)
done
qed
subsection‹Valid Test Sequences in the State Exception Monad›
text‹
This is still an unstructured merge of executable monad concepts and specification oriented
high-level properties initiating test procedures.
›
definition valid_SE :: "'σ ⇒ (bool,'σ) MON⇩S⇩E ⇒ bool" (infix "⊨" 15)
where "(σ ⊨ m) = (m σ ≠ None ∧ fst(the (m σ)))"
text‹
This notation consideres failures as valid---a definition inspired by I/O conformance.
Note that it is not possible to define this concept once and for all in a Hindley-Milner
type-system. For the moment, we present it only for the state-exception monad, although for
the same definition, this notion is applicable to other monads as well.
›
lemma syntax_test :
"σ ⊨ (os ← (mbind ιs ioprog); return(length ιs = length os))"
oops
lemma valid_true[simp]: "(σ ⊨ (s ← return x ; return (P s))) = P x"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)
text‹Recall mbind\_unit for the base case.›
lemma valid_failure: "ioprog a σ = None ⟹
(σ ⊨ (s ← mbind (a#S) ioprog ; M s)) =
(σ ⊨ (M []))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)
lemma valid_failure': "A σ = None ⟹ ¬(σ ⊨ ((s ← A ; M s)))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)
lemma valid_successElem:
"M σ = Some(f σ,σ) ⟹ (σ ⊨ M) = f σ"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )
lemma valid_success: "ioprog a σ = Some(b,σ') ⟹
(σ ⊨ (s ← mbind (a#S) ioprog ; M s)) =
(σ' ⊨ (s ← mbind S ioprog ; M (b#s)))"
apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
apply (cases "mbind S ioprog σ'", auto)
done
lemma valid_success'': "ioprog a σ = Some(b,σ') ⟹
(σ ⊨ (s ← mbind (a#S) ioprog ; return (P s))) =
(σ' ⊨ (s ← mbind S ioprog ; return (P (b#s))))"
apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
apply (cases "mbind S ioprog σ'")
apply (simp_all)
apply (auto)
done
lemma valid_success': "A σ = Some(b,σ') ⟹ (σ ⊨ ((s ← A ; M s))) = (σ' ⊨ (M b))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )
lemma valid_both: "(σ ⊨ (s ← mbind (a#S) ioprog ; return (P s))) =
(case ioprog a σ of
None ⇒ (σ ⊨ (return (P [])))
| Some(b,σ') ⇒ (σ' ⊨ (s ← mbind S ioprog ; return (P (b#s)))))"
apply (case_tac "ioprog a σ")
apply (simp_all add: valid_failure valid_success'' split: prod.splits)
done
lemma valid_propagate_1 [simp]: "(σ ⊨ (return P)) = (P)"
by(auto simp: valid_SE_def unit_SE_def)
lemma valid_propagate_2: "σ ⊨ ((s ← A ; M s)) ⟹ ∃ v σ'. the(A σ) = (v,σ') ∧ σ' ⊨ (M v)"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A σ")
apply (simp_all)
apply (drule_tac x="A σ" and f=the in arg_cong)
apply (simp)
apply (rename_tac a b aa )
apply (rule_tac x="fst aa" in exI)
apply (rule_tac x="snd aa" in exI)
by (auto)
lemma valid_propagate_2': "σ ⊨ ((s ← A ; M s)) ⟹ ∃ a. (A σ) = Some a ∧ (snd a) ⊨ (M (fst a))"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A σ")
apply (simp_all)
apply (simp_all split: prod.splits)
apply (drule_tac x="A σ" and f=the in arg_cong)
apply (simp)
apply (rename_tac a b aa x1 x2)
apply (rule_tac x="fst aa" in exI)
apply (rule_tac x="snd aa" in exI)
apply (auto)
done
lemma valid_propagate_2'': "σ ⊨ ((s ← A ; M s)) ⟹ ∃ v σ'. A σ = Some(v,σ') ∧ σ' ⊨ (M v)"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A σ")
apply (simp_all)
apply (drule_tac x="A σ" and f=the in arg_cong)
apply (simp)
apply (rename_tac a b aa )
apply (rule_tac x="fst aa" in exI)
apply (rule_tac x="snd aa" in exI)
apply (auto)
done
lemma valid_propoagate_3[simp]: "(σ⇩0 ⊨ (λσ. Some (f σ, σ))) = (f σ⇩0)"
by(simp add: valid_SE_def )
lemma valid_propoagate_3'[simp]: "¬(σ⇩0 ⊨ (λσ. None))"
by(simp add: valid_SE_def )
lemma assert_disch1 :" P σ ⟹ (σ ⊨ (x ← assert⇩S⇩E P; M x)) = (σ ⊨ (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
lemma assert_disch2 :" ¬ P σ ⟹ ¬ (σ ⊨ (x ← assert⇩S⇩E P ; M s))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
lemma assert_disch3 :" ¬ P σ ⟹ ¬ (σ ⊨ (assert⇩S⇩E P))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
lemma assert_D : "(σ ⊨ (x ← assert⇩S⇩E P; M x)) ⟹ P σ ∧ (σ ⊨ (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm)
lemma assume_D : "(σ ⊨ (x ← assume⇩S⇩E P; M x)) ⟹ ∃ σ. (P σ ∧ σ ⊨ (M ()))"
apply (auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.if_split_asm)
apply (rule_tac x="Eps P" in exI)
apply (auto)[1]
subgoal for x a b
apply (rule_tac x="True" in exI, rule_tac x="b" in exI)
apply (subst Hilbert_Choice.someI)
apply (assumption)
apply (simp)
done
apply (subst Hilbert_Choice.someI,assumption)
apply (simp)
done
text‹
These two rule prove that the SE Monad in connection with the notion of valid sequence is
actually sufficient for a representation of a Boogie-like language. The SBE monad with explicit
sets of states---to be shown below---is strictly speaking not necessary (and will therefore
be discontinued in the development).
›
lemma if_SE_D1 : "P σ ⟹ (σ ⊨ if⇩S⇩E P B⇩1 B⇩2) = (σ ⊨ B⇩1)"
by(auto simp: if_SE_def valid_SE_def)
lemma if_SE_D2 : "¬ P σ ⟹ (σ ⊨ if⇩S⇩E P B⇩1 B⇩2) = (σ ⊨ B⇩2)"
by(auto simp: if_SE_def valid_SE_def)
lemma if_SE_split_asm : " (σ ⊨ if⇩S⇩E P B⇩1 B⇩2) = ((P σ ∧ (σ ⊨ B⇩1)) ∨ (¬ P σ ∧ (σ ⊨ B⇩2)))"
by(cases "P σ",auto simp: if_SE_D1 if_SE_D2)
lemma if_SE_split : " (σ ⊨ if⇩S⇩E P B⇩1 B⇩2) = ((P σ ⟶ (σ ⊨ B⇩1)) ∧ (¬ P σ ⟶ (σ ⊨ B⇩2)))"
by(cases "P σ", auto simp: if_SE_D1 if_SE_D2)
lemma [code]: "(σ ⊨ m) = (case (m σ) of None ⇒ False | (Some (x,y)) ⇒ x)"
apply (simp add: valid_SE_def)
apply (cases "m σ = None")
apply (simp_all)
apply (insert not_None_eq)
apply (auto)
done
subsection‹Valid Test Sequences in the State Exception Backtrack Monad›
text‹
This is still an unstructured merge of executable monad concepts and specification oriented
high-level properties initiating test procedures.
›
definition valid_SBE :: "'σ ⇒ ('a,'σ) MON⇩S⇩B⇩E ⇒ bool" (infix "⊨⇩S⇩B⇩E" 15)
where "σ ⊨⇩S⇩B⇩E m ≡ (m σ ≠ None)"
text‹
This notation considers all non-failures as valid.
›
lemma assume_assert: "(σ ⊨⇩S⇩B⇩E ( _ :≡ assume⇩S⇩B⇩E P ; assert⇩S⇩B⇩E Q)) = (P σ ⟶ Q σ)"
by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
lemma assert_intro: "Q σ ⟹ σ ⊨⇩S⇩B⇩E (assert⇩S⇩B⇩E Q)"
by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
end
Theory UPFCore
section‹The Core of the Unified Policy Framework (UPF)›
theory
UPFCore
imports
Monads
begin
subsection‹Foundation›
text‹
The purpose of this theory is to formalize a somewhat non-standard view
on the fundamental concept of a security policy which is worth outlining.
This view has arisen from prior experience in the modelling of network
(firewall) policies. Instead of regarding policies as relations on resources,
sets of permissions, etc., we emphasise the view that a policy is a policy
decision function that grants or denies access to resources, permissions, etc.
In other words, we model the concrete function that implements the policy
decision point in a system, and which represents a "wrapper" around the
business logic. An advantage of this view is that it is compatible
with many different policy models, enabling a uniform modelling framework to be
defined. Furthermore, this function is typically a large cascade of nested
conditionals, using conditions referring to an internal state and security
contexts of the system or a user. This cascade of conditionals can easily be
decomposed into a set of test cases similar to transformations used for binary
decision diagrams (BDD), and motivate equivalence class testing for unit test and
sequence test scenarios. From the modelling perspective, using \HOL as
its input language, we will consequently use the expressive power of its
underlying functional programming language, including the possibility to
define higher-order combinators.
In more detail, we model policies as partial functions based on input
data $\alpha$ (arguments, system state, security context, ...) to output
data $\beta$:
›
datatype 'α decision = allow 'α | deny 'α
type_synonym ('α,'β) policy = "'α ⇀ 'β decision" (infixr "|->" 0)
text‹In the following, we introduce a number of shortcuts and alternative notations.
The type of policies is represented as:›
translations (type) "'α |-> 'β" <= (type) "'α ⇀ 'β decision"
type_notation "policy" (infixr "↦" 0)
text‹... allowing the notation @{typ "'α ↦ 'β"} for the policy type and the
alternative notations for @{term None} and @{term Some} of the \HOL library
@{typ "'α option"} type:›
notation "None" ("⊥")
notation "Some" ("⌊_⌋" 80)
text‹Thus, the range of a policy may consist of @{term "⌊accept x⌋"} data,
of @{term "⌊deny x⌋"} data, as well as @{term "⊥"} modeling the undefinedness
of a policy, i.e. a policy is considered as a partial function. Partial
functions are used since we describe elementary policies by partial system
behaviour, which are glued together by operators such as function override and
functional composition.
›
text‹We define the two fundamental sets, the allow-set $Allow$ and the
deny-set $Deny$ (written $A$ and $D$ set for short), to characterize these
two main sets of the range of a policy.
›
definition Allow :: "('α decision) set"
where "Allow = range allow"
definition Deny :: "('α decision) set"
where "Deny = range deny"
subsection‹Policy Constructors›
text‹
Most elementary policy constructors are based on the
update operation @{thm [source] "Fun.fun_upd_def"} @{thm Fun.fun_upd_def}
and the maplet-notation @{term "a(x ↦ y)"} used for @{term "a(x:=⌊y⌋)"}.
Furthermore, we add notation adopted to our problem domain:›
nonterminal policylets and policylet
syntax
"_policylet1" :: "['a, 'a] => policylet" ("_ /↦⇩+/ _")
"_policylet2" :: "['a, 'a] => policylet" ("_ /↦⇩-/ _")
"" :: "policylet => policylets" ("_")
"_Maplets" :: "[policylet, policylets] => policylets" ("_,/ _")
"_Maplets" :: "[policylet, policylets] => policylets" ("_,/ _")
"_MapUpd" :: "['a |-> 'b, policylets] => 'a |-> 'b" ("_/'(_')" [900,0]900)
"_emptypolicy" :: "'a |-> 'b" ("∅")
translations
"_MapUpd m (_Maplets xy ms)" ⇌ "_MapUpd (_MapUpd m xy) ms"
"_MapUpd m (_policylet1 x y)" ⇌ "m(x := CONST Some (CONST allow y))"
"_MapUpd m (_policylet2 x y)" ⇌ "m(x := CONST Some (CONST deny y))"
"∅" ⇌ "CONST Map.empty"
text‹Here are some lemmas essentially showing syntactic equivalences:›
lemma test: "∅(x↦⇩+a, y↦⇩-b) = ∅(x ↦⇩+ a, y ↦⇩- b)" by simp
lemma test2: "p(x↦⇩+a,x↦⇩-b) = p(x↦⇩-b)" by simp
text‹
We inherit a fairly rich theory on policy updates from Map here. Some examples are:
›
lemma pol_upd_triv1: "t k = ⌊allow x⌋ ⟹ t(k↦⇩+x) = t"
by (rule ext) simp
lemma pol_upd_triv2: "t k = ⌊deny x⌋ ⟹ t(k↦⇩-x) = t"
by (rule ext) simp
lemma pol_upd_allow_nonempty: "t(k↦⇩+x) ≠ ∅"
by simp
lemma pol_upd_deny_nonempty: "t(k↦⇩-x) ≠ ∅"
by simp
lemma pol_upd_eqD1 : "m(a↦⇩+x) = n(a↦⇩+y) ⟹ x = y"
by(auto dest: map_upd_eqD1)
lemma pol_upd_eqD2 : "m(a↦⇩-x) = n(a↦⇩-y) ⟹ x = y"
by(auto dest: map_upd_eqD1)
lemma pol_upd_neq1 [simp]: "m(a↦⇩+x) ≠ n(a↦⇩-y)"
by(auto dest: map_upd_eqD1)
subsection‹Override Operators›
text‹
Key operators for constructing policies are the override operators. There are four different
versions of them, with one of them being the override operator from the Map theory. As it is
common to compose policy rules in a ``left-to-right-first-fit''-manner, that one is taken as
default, defined by a syntax translation from the provided override operator from the Map
theory (which does it in reverse order).
›
syntax
"_policyoverride" :: "['a ↦ 'b, 'a ↦ 'b] ⇒ 'a ↦ 'b" (infixl "⨁" 100)
translations
"p ⨁ q" ⇌ "q ++ p"
text‹
Some elementary facts inherited from Map are:
›
lemma override_empty: "p ⨁ ∅ = p"
by simp
lemma empty_override: "∅ ⨁ p = p"
by simp
lemma override_assoc: "p1 ⨁ (p2 ⨁ p3) = (p1 ⨁ p2) ⨁ p3"
by simp
text‹
The following two operators are variants of the standard override. For override\_A,
an allow of wins over a deny. For override\_D, the situation is dual.
›
definition override_A :: "['α↦'β, 'α↦'β] ⇒ 'α↦'β" (infixl "++'_A" 100)
where "m2 ++_A m1 =
(λx. (case m1 x of
⌊allow a⌋ ⇒ ⌊allow a⌋
| ⌊deny a⌋ ⇒ (case m2 x of ⌊allow b⌋ ⇒ ⌊allow b⌋
| _ ⇒ ⌊deny a⌋)
| ⊥ ⇒ m2 x)
)"
syntax
"_policyoverride_A" :: "['a ↦ 'b, 'a ↦ 'b] ⇒ 'a ↦ 'b" (infixl "⨁⇩A" 100)
translations
"p ⨁⇩A q" ⇌ "p ++_A q"
lemma override_A_empty[simp]: "p ⨁⇩A ∅ = p"
by(simp add:override_A_def)
lemma empty_override_A[simp]: "∅ ⨁⇩A p = p"
apply (rule ext)
apply (simp add:override_A_def)
subgoal for x
apply (case_tac "p x")
apply (simp_all)
subgoal for a
apply (case_tac a)
apply (simp_all)
done
done
done
lemma override_A_assoc: "p1 ⨁⇩A (p2 ⨁⇩A p3) = (p1 ⨁⇩A p2) ⨁⇩A p3"
by (rule ext, simp add: override_A_def split: decision.splits option.splits)
definition override_D :: "['α↦'β, 'α↦'β] ⇒ 'α↦'β" (infixl "++'_D" 100)
where "m1 ++_D m2 =
(λx. case m2 x of
⌊deny a⌋ ⇒ ⌊deny a⌋
| ⌊allow a⌋ ⇒ (case m1 x of ⌊deny b⌋ ⇒ ⌊deny b⌋
| _ ⇒ ⌊allow a⌋)
| ⊥ ⇒ m1 x
)"
syntax
"_policyoverride_D" :: "['a ↦ 'b, 'a ↦ 'b] ⇒ 'a ↦ 'b" (infixl "⨁⇩D" 100)
translations
"p ⨁⇩D q" ⇌ "p ++_D q"
lemma override_D_empty[simp]: "p ⨁⇩D ∅ = p"
by(simp add:override_D_def)
lemma empty_override_D[simp]: "∅ ⨁⇩D p = p"
apply (rule ext)
apply (simp add:override_D_def)
subgoal for x
apply (case_tac "p x", simp_all)
subgoal for a
apply (case_tac a, simp_all)
done
done
done
lemma override_D_assoc: "p1 ⨁⇩D (p2 ⨁⇩D p3) = (p1 ⨁⇩D p2) ⨁⇩D p3"
apply (rule ext)
apply (simp add: override_D_def split: decision.splits option.splits)
done
subsection‹Coercion Operators›
text‹
Often, especially when combining policies of different type, it is necessary to
adapt the input or output domain of a policy to a more refined context.
›
text‹
An analogous for the range of a policy is defined as follows:
›
definition policy_range_comp :: "['β⇒'γ, 'α↦'β] ⇒ 'α ↦'γ" (infixl "o'_f" 55)
where
"f o_f p = (λx. case p x of
⌊allow y⌋ ⇒ ⌊allow (f y)⌋
| ⌊deny y⌋ ⇒ ⌊deny (f y)⌋
| ⊥ ⇒ ⊥)"
syntax
"_policy_range_comp" :: "['β⇒'γ, 'α↦'β] ⇒ 'α ↦'γ" (infixl "o⇩f" 55)
translations
"p o⇩f q" ⇌ "p o_f q"
lemma policy_range_comp_strict : "f o⇩f ∅ = ∅"
apply (rule ext)
apply (simp add: policy_range_comp_def)
done
text‹
A generalized version is, where separate coercion functions are applied to the result
depending on the decision of the policy is as follows:
›
definition range_split :: "[('β⇒'γ)×('β⇒'γ),'α ↦ 'β] ⇒ 'α ↦ 'γ"
(infixr "∇" 100)
where "(P) ∇ p = (λx. case p x of
⌊allow y⌋ ⇒ ⌊allow ((fst P) y)⌋
| ⌊deny y⌋ ⇒ ⌊deny ((snd P) y)⌋
| ⊥ ⇒ ⊥)"
lemma range_split_strict[simp]: "P ∇ ∅ = ∅"
apply (rule ext)
apply (simp add: range_split_def)
done
lemma range_split_charn:
"(f,g) ∇ p = (λx. case p x of
⌊allow x⌋ ⇒ ⌊allow (f x)⌋
| ⌊deny x⌋ ⇒ ⌊deny (g x)⌋
| ⊥ ⇒ ⊥)"
apply (simp add: range_split_def)
apply (rule ext)
subgoal for x
apply (case_tac "p x")
apply (simp_all)
subgoal for a
apply (case_tac "a")
apply (simp_all)
done
done
done
text‹
The connection between these two becomes apparent if considering the following lemma:
›
lemma range_split_vs_range_compose: "(f,f) ∇ p = f o⇩f p"
by(simp add: range_split_charn policy_range_comp_def)
lemma range_split_id [simp]: "(id,id) ∇ p = p"
apply (rule ext)
apply (simp add: range_split_charn id_def)
subgoal for x
apply (case_tac "p x")
apply (simp_all)
subgoal for a
apply (case_tac "a")
apply (simp_all)
done
done
done
lemma range_split_bi_compose [simp]: "(f1,f2) ∇ (g1,g2) ∇ p = (f1 o g1,f2 o g2) ∇ p"
apply (rule ext)
apply (simp add: range_split_charn comp_def)
subgoal for x
apply (case_tac "p x")
apply (simp_all)
subgoal for a
apply (case_tac "a")
apply (simp_all)
done
done
done
text‹
The next three operators are rather exotic and in most cases not used.
›
text ‹
The following is a variant of range\_split, where the change in the decision depends
on the input instead of the output.
›
definition dom_split2a :: "[('α ⇀ 'γ) × ('α ⇀'γ),'α ↦ 'β] ⇒ 'α ↦ 'γ" (infixr "Δa" 100)
where "P Δa p = (λx. case p x of
⌊allow y⌋ ⇒ ⌊allow (the ((fst P) x))⌋
| ⌊deny y⌋ ⇒ ⌊deny (the ((snd P) x))⌋
| ⊥ ⇒ ⊥)"
definition dom_split2 :: "[('α ⇒ 'γ) × ('α ⇒'γ),'α ↦ 'β] ⇒ 'α ↦ 'γ" (infixr "Δ" 100)
where "P Δ p = (λx. case p x of
⌊allow y⌋ ⇒ ⌊allow ((fst P) x)⌋
| ⌊deny y⌋ ⇒ ⌊deny ((snd P) x)⌋
| ⊥ ⇒ ⊥)"
definition range_split2 :: "[('α ⇒ 'γ) × ('α ⇒'γ),'α ↦ 'β] ⇒ 'α ↦ ('β ×'γ)" (infixr "∇2" 100)
where "P ∇2 p = (λx. case p x of
⌊allow y⌋ ⇒ ⌊allow (y,(fst P) x)⌋
| ⌊deny y⌋ ⇒ ⌊deny (y,(snd P) x)⌋
| ⊥ ⇒ ⊥)"
text‹
The following operator is used for transition policies only: a transition policy is transformed
into a state-exception monad. Such a monad can for example be used for test case generation using
HOL-Testgen~\cite{brucker.ea:theorem-prover:2012}.
›
definition policy2MON :: "('ι×'σ ↦ 'o×'σ) ⇒ ('ι ⇒('o decision,'σ) MON⇩S⇩E)"
where "policy2MON p = (λ ι σ. case p (ι,σ) of
⌊(allow (outs,σ'))⌋ ⇒ ⌊(allow outs, σ')⌋
| ⌊(deny (outs,σ'))⌋ ⇒ ⌊(deny outs, σ')⌋
| ⊥ ⇒ ⊥)"
lemmas UPFCoreDefs = Allow_def Deny_def override_A_def override_D_def policy_range_comp_def
range_split_def dom_split2_def map_add_def restrict_map_def
end
Theory ElementaryPolicies
section‹Elementary Policies›
theory
ElementaryPolicies
imports
UPFCore
begin
text‹
In this theory, we introduce the elementary policies of UPF that build the basis
for more complex policies. These complex policies, respectively, embedding of
well-known access control or security models, are build by composing the elementary
policies defined in this theory.
›
subsection‹The Core Policy Combinators: Allow and Deny Everything›
definition
deny_pfun :: "('α ⇀'β) ⇒ ('α ↦ 'β)" ("AllD")
where
"deny_pfun pf ≡ (λ x. case pf x of
⌊y⌋ ⇒ ⌊deny (y)⌋
|⊥ ⇒ ⊥)"
definition
allow_pfun :: "('α ⇀'β) ⇒ ('α ↦ 'β)" ( "AllA")
where
"allow_pfun pf ≡ (λ x. case pf x of
⌊y⌋ ⇒ ⌊allow (y)⌋
|⊥ ⇒ ⊥)"
syntax
"_allow_pfun" :: "('α ⇀'β) ⇒ ('α ↦ 'β)" ("A⇩p")
translations
"A⇩p f" ⇌ "AllA f"
syntax
"_deny_pfun" :: "('α ⇀'β) ⇒ ('α ↦ 'β)" ("D⇩p")
translations
"D⇩p f" ⇌ "AllD f"
notation
"deny_pfun" (binder "∀D" 10) and
"allow_pfun" (binder "∀A" 10)
lemma AllD_norm[simp]: "deny_pfun (id o (λx. ⌊x⌋)) = (∀Dx. ⌊x⌋)"
by(simp add:id_def comp_def)
lemma AllD_norm2[simp]: "deny_pfun (Some o id) = (∀Dx. ⌊x⌋)"
by(simp add:id_def comp_def)
lemma AllA_norm[simp]: "allow_pfun (id o Some) = (∀Ax. ⌊x⌋)"
by(simp add:id_def comp_def)
lemma AllA_norm2[simp]: "allow_pfun (Some o id) = (∀Ax. ⌊x⌋)"
by(simp add:id_def comp_def)
lemma AllA_apply[simp]: "(∀Ax. Some (P x)) x = ⌊allow (P x)⌋"
by(simp add:allow_pfun_def)
lemma AllD_apply[simp]: "(∀Dx. Some (P x)) x = ⌊deny (P x)⌋"
by(simp add:deny_pfun_def)
lemma neq_Allow_Deny: "pf ≠ ∅ ⟹ (deny_pfun pf) ≠ (allow_pfun pf)"
apply (erule contrapos_nn)
apply (rule ext)
subgoal for x
apply (drule_tac x=x in fun_cong)
apply (auto simp: deny_pfun_def allow_pfun_def)
apply (case_tac "pf x = ⊥")
apply (auto)
done
done
subsection‹Common Instances›
definition allow_all_fun :: "('α ⇒ 'β) ⇒ ('α ↦ 'β)" ("A⇩f")
where "allow_all_fun f = allow_pfun (Some o f)"
definition deny_all_fun :: "('α ⇒ 'β) ⇒ ('α ↦ 'β)" ("D⇩f")
where "deny_all_fun f ≡ deny_pfun (Some o f)"
definition
deny_all_id :: "'α ↦ 'α" ("D⇩I") where
"deny_all_id ≡ deny_pfun (id o Some)"
definition
allow_all_id :: "'α ↦ 'α" ("A⇩I") where
"allow_all_id ≡ allow_pfun (id o Some)"
definition
allow_all :: "('α ↦ unit)" ("A⇩U") where
"allow_all p = ⌊allow ()⌋"
definition
deny_all :: "('α ↦ unit)" ("D⇩U") where
"deny_all p = ⌊deny ()⌋"
text‹... and resulting properties:›
lemma "A⇩I ⨁ Map.empty = A⇩I"
by simp
lemma "A⇩f f ⨁ Map.empty = A⇩f f"
by simp
lemma "allow_pfun Map.empty = Map.empty"
apply (rule ext)
apply (simp add: allow_pfun_def)
done
lemma allow_left_cancel :"dom pf = UNIV ⟹ (allow_pfun pf) ⨁ x = (allow_pfun pf)"
apply (rule ext)+
apply (auto simp: allow_pfun_def option.splits)
done
lemma deny_left_cancel :"dom pf = UNIV ⟹ (deny_pfun pf) ⨁ x = (deny_pfun pf)"
apply (rule ext)+
by (auto simp: deny_pfun_def option.splits)
subsection‹Domain, Range, and Restrictions›
text‹
Since policies are essentially maps, we inherit the basic definitions for
domain and range on Maps: \\
\verb+Map.dom_def+ : @{thm Map.dom_def} \\
whereas range is just an abrreviation for image:
\begin{verbatim}
abbreviation range :: "('a => 'b) => 'b set"
where -- "of function" "range f == f ` UNIV"
\end{verbatim}
As a consequence, we inherit the following properties on
policies:
\begin{itemize}
\item \verb+Map.domD+ @{thm Map.domD}
\item\verb+Map.domI+ @{thm Map.domI}
\item\verb+Map.domIff+ @{thm Map.domIff}
\item\verb+Map.dom_const+ @{thm Map.dom_const}
\item\verb+Map.dom_def+ @{thm Map.dom_def}
\item\verb+Map.dom_empty+ @{thm Map.dom_empty}
\item\verb+Map.dom_eq_empty_conv+ @{thm Map.dom_eq_empty_conv}
\item\verb+Map.dom_eq_singleton_conv+ @{thm Map.dom_eq_singleton_conv}
\item\verb+Map.dom_fun_upd+ @{thm Map.dom_fun_upd}
\item\verb+Map.dom_if+ @{thm Map.dom_if}
\item\verb+Map.dom_map_add+ @{thm Map.dom_map_add}
\end{itemize}
›
text‹
However, some properties are specific to policy concepts:
›
lemma sub_ran : "ran p ⊆ Allow ∪ Deny"
apply (auto simp: Allow_def Deny_def ran_def full_SetCompr_eq[symmetric])[1]
subgoal for x a
apply (case_tac "x")
apply (simp_all)
done
done
lemma dom_allow_pfun [simp]:"dom(allow_pfun f) = dom f"
apply (auto simp: allow_pfun_def)
subgoal for x y
apply (case_tac "f x", simp_all)
done
done
lemma dom_allow_all: "dom(A⇩f f) = UNIV"
by(auto simp: allow_all_fun_def o_def)
lemma dom_deny_pfun [simp]:"dom(deny_pfun f) = dom f"
apply (auto simp: deny_pfun_def)[1]
apply (case_tac "f x")
apply (simp_all)
done
lemma dom_deny_all: " dom(D⇩f f) = UNIV"
by(auto simp: deny_all_fun_def o_def)
lemma ran_allow_pfun [simp]:"ran(allow_pfun f) = allow `(ran f)"
apply (simp add: allow_pfun_def ran_def)
apply (rule set_eqI)
apply (auto)[1]
subgoal for x a
apply (case_tac "f a")
apply (auto simp: image_def)[1]
apply (auto simp: image_def)[1]
done
subgoal for xa a
apply (rule_tac x=a in exI)
apply (simp)
done
done
lemma ran_allow_all: "ran(A⇩f id) = Allow"
apply (simp add: allow_all_fun_def Allow_def o_def)
apply (rule set_eqI)
apply (auto simp: image_def ran_def)
done
lemma ran_deny_pfun[simp]: "ran(deny_pfun f) = deny ` (ran f)"
apply (simp add: deny_pfun_def ran_def)
apply (rule set_eqI)
apply (auto)[1]
subgoal for x a
apply (case_tac "f a")
apply (auto simp: image_def)[1]
apply (auto simp: image_def)[1]
done
subgoal for xa a
apply (rule_tac x=a in exI)
apply (simp)
done
done
lemma ran_deny_all: "ran(D⇩f id) = Deny"
apply (simp add: deny_all_fun_def Deny_def o_def)
apply (rule set_eqI)
apply (auto simp: image_def ran_def)
done
text‹
Reasoning over \verb+dom+ is most crucial since it paves the way for simplification and
reordering of policies composed by override (i.e. by the normal left-to-right rule composition
method.
\begin{itemize}
\item \verb+Map.dom_map_add+ @{thm Map.dom_map_add}
\item \verb+Map.inj_on_map_add_dom+ @{thm Map.inj_on_map_add_dom}
\item \verb+Map.map_add_comm+ @{thm Map.map_add_comm}
\item \verb+Map.map_add_dom_app_simps(1)+ @{thm Map.map_add_dom_app_simps(1)}
\item \verb+Map.map_add_dom_app_simps(2)+ @{thm Map.map_add_dom_app_simps(2)}
\item \verb+Map.map_add_dom_app_simps(3)+ @{thm Map.map_add_dom_app_simps(3)}
\item \verb+Map.map_add_upd_left+ @{thm Map.map_add_upd_left}
\end{itemize}
The latter rule also applies to allow- and deny-override.
›
definition dom_restrict :: "['α set, 'α↦'β] ⇒ 'α↦'β" (infixr "◃" 55)
where "S ◃ p ≡ (λx. if x ∈ S then p x else ⊥)"
lemma dom_dom_restrict[simp] : "dom(S ◃ p) = S ∩ dom p"
apply (auto simp: dom_restrict_def)
subgoal for x y
apply (case_tac "x ∈ S")
apply (simp_all)
done
subgoal for x y
apply (case_tac "x ∈ S")
apply (simp_all)
done
done
lemma dom_restrict_idem[simp] : "(dom p) ◃ p = p"
apply (rule ext)
apply (auto simp: dom_restrict_def
dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
lemma dom_restrict_inter[simp] : "T ◃ S ◃ p = T ∩ S ◃ p"
apply (rule ext)
apply (auto simp: dom_restrict_def
dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
definition ran_restrict :: "['α↦'β,'β decision set] ⇒ 'α ↦'β" (infixr "▹" 55)
where "p ▹ S ≡ (λx. if p x ∈ (Some`S) then p x else ⊥)"
definition ran_restrict2 :: "['α↦'β,'β decision set] ⇒ 'α ↦'β" (infixr "▹2" 55)
where "p ▹2 S ≡ (λx. if (the (p x)) ∈ (S) then p x else ⊥)"
lemma "ran_restrict = ran_restrict2"
apply (rule ext)+
apply (simp add: ran_restrict_def ran_restrict2_def)
subgoal for x xa xb
apply (case_tac "x xb")
apply simp_all
apply (metis inj_Some inj_image_mem_iff)
done
done
lemma ran_ran_restrict[simp] : "ran(p ▹ S) = S ∩ ran p"
by(auto simp: ran_restrict_def image_def ran_def)
lemma ran_restrict_idem[simp] : "p ▹ (ran p) = p"
apply (rule ext)
apply (auto simp: ran_restrict_def image_def Ball_def ran_def)
apply (erule contrapos_pp)
apply (auto dest!: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
lemma ran_restrict_inter[simp] : "(p ▹ S) ▹ T = p ▹ T ∩ S"
apply (rule ext)
apply (auto simp: ran_restrict_def
dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
lemma ran_gen_A[simp] : "(∀Ax. ⌊P x⌋) ▹ Allow = (∀Ax. ⌊P x⌋)"
apply (rule ext)
apply (auto simp: Allow_def ran_restrict_def)
done
lemma ran_gen_D[simp] : "(∀Dx. ⌊P x⌋) ▹ Deny = (∀Dx. ⌊P x⌋)"
apply (rule ext)
apply (auto simp: Deny_def ran_restrict_def)
done
lemmas ElementaryPoliciesDefs = deny_pfun_def allow_pfun_def allow_all_fun_def deny_all_fun_def
allow_all_id_def deny_all_id_def allow_all_def deny_all_def
dom_restrict_def ran_restrict_def
end
Theory SeqComposition
section‹Sequential Composition›
theory
SeqComposition
imports
ElementaryPolicies
begin
text‹
Sequential composition is based on the idea that two policies are to be combined by applying
the second policy to the output of the first one. Again, there are four possibilities how the
decisions can be combined.›
subsection ‹Flattening›
text‹
A key concept of sequential policy composition is the flattening of nested decisions. There are
four possibilities, and these possibilities will give the various flavours of policy composition.
›
fun flat_orA :: "('α decision) decision ⇒ ('α decision)"
where "flat_orA(allow(allow y)) = allow y"
|"flat_orA(allow(deny y)) = allow y"
|"flat_orA(deny(allow y)) = allow y"
|"flat_orA(deny(deny y)) = deny y"
lemma flat_orA_deny[dest]:"flat_orA x = deny y ⟹ x = deny(deny y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
lemma flat_orA_allow[dest]: "flat_orA x = allow y ⟹ x = allow(allow y)
∨ x = allow(deny y)
∨ x = deny(allow y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
fun flat_orD :: "('α decision) decision ⇒ ('α decision)"
where "flat_orD(allow(allow y)) = allow y"
|"flat_orD(allow(deny y)) = deny y"
|"flat_orD(deny(allow y)) = deny y"
|"flat_orD(deny(deny y)) = deny y"
lemma flat_orD_allow[dest]: "flat_orD x = allow y ⟹ x = allow(allow y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
lemma flat_orD_deny[dest]: "flat_orD x = deny y ⟹ x = deny(deny y)
∨ x = allow(deny y)
∨ x = deny(allow y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
fun flat_1 :: "('α decision) decision ⇒ ('α decision)"
where "flat_1(allow(allow y)) = allow y"
|"flat_1(allow(deny y)) = allow y"
|"flat_1(deny(allow y)) = deny y"
|"flat_1(deny(deny y)) = deny y"
lemma flat_1_allow[dest]: "flat_1 x = allow y ⟹ x = allow(allow y) ∨ x = allow(deny y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
lemma flat_1_deny[dest]: "flat_1 x = deny y ⟹ x = deny(deny y) ∨ x = deny(allow y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
fun flat_2 :: "('α decision) decision ⇒ ('α decision)"
where "flat_2(allow(allow y)) = allow y"
|"flat_2(allow(deny y)) = deny y"
|"flat_2(deny(allow y)) = allow y"
|"flat_2(deny(deny y)) = deny y"
lemma flat_2_allow[dest]: "flat_2 x = allow y ⟹ x = allow(allow y) ∨ x = deny(allow y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
lemma flat_2_deny[dest]: "flat_2 x = deny y ⟹ x = deny(deny y) ∨ x = allow(deny y)"
apply (case_tac "x")
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
apply (rename_tac α)
apply (case_tac "α", simp_all)[1]
done
subsection‹Policy Composition›
text‹
The following definition allows to compose two policies. Denies and allows are transferred.
›
fun lift :: "('α ↦ 'β) ⇒ ('α decision ↦'β decision)"
where "lift f (deny s) = (case f s of
⌊y⌋ ⇒ ⌊deny y⌋
| ⊥ ⇒ ⊥)"
| "lift f (allow s) = (case f s of
⌊y⌋ ⇒ ⌊allow y⌋
| ⊥ ⇒ ⊥)"
lemma lift_mt [simp]: "lift ∅ = ∅"
apply (rule ext)
subgoal for x
apply (case_tac "x")
apply (simp_all)
done
done
text‹
Since policies are maps, we inherit a composition on them. However, this results in nestings
of decisions---which must be flattened. As we now that there are four different forms of
flattening, we have four different forms of policy composition:›
definition
comp_orA :: "['β↦'γ, 'α↦'β] ⇒ 'α↦'γ" (infixl "o'_orA" 55) where
"p2 o_orA p1 ≡ (map_option flat_orA) o (lift p2 ∘⇩m p1)"
notation
comp_orA (infixl "∘⇩∨⇩A" 55)
lemma comp_orA_mt[simp]:"p ∘⇩∨⇩A ∅ = ∅"
by(simp add: comp_orA_def)
lemma mt_comp_orA[simp]:"∅ ∘⇩∨⇩A p = ∅"
by(simp add: comp_orA_def)
definition
comp_orD :: "['β↦'γ, 'α↦'β] ⇒ 'α↦'γ" (infixl "o'_orD" 55) where
"p2 o_orD p1 ≡ (map_option flat_orD) o (lift p2 ∘⇩m p1)"
notation
comp_orD (infixl "∘⇩orD" 55)
lemma comp_orD_mt[simp]:"p o_orD ∅ = ∅"
by(simp add: comp_orD_def)
lemma mt_comp_orD[simp]:"∅ o_orD p = ∅"
by(simp add: comp_orD_def)
definition
comp_1 :: "['β↦'γ, 'α↦'β] ⇒ 'α↦'γ" (infixl "o'_1" 55) where
"p2 o_1 p1 ≡ (map_option flat_1) o (lift p2 ∘⇩m p1)"
notation
comp_1 (infixl "∘⇩1" 55)
lemma comp_1_mt[simp]:"p ∘⇩1 ∅ = ∅"
by(simp add: comp_1_def)
lemma mt_comp_1[simp]:"∅ ∘⇩1 p = ∅"
by(simp add: comp_1_def)
definition
comp_2 :: "['β↦'γ, 'α↦'β] ⇒ 'α↦'γ" (infixl "o'_2" 55) where
"p2 o_2 p1 ≡ (map_option flat_2) o (lift p2 ∘⇩m p1)"
notation
comp_2 (infixl "∘⇩2" 55)
lemma comp_2_mt[simp]:"p ∘⇩2 ∅ = ∅"
by(simp add: comp_2_def)
lemma mt_comp_2[simp]:"∅ ∘⇩2 p = ∅"
by(simp add: comp_2_def)
end
Theory ParallelComposition
section‹Parallel Composition›
theory
ParallelComposition
imports
ElementaryPolicies
begin
text‹
The following combinators are based on the idea that two policies are executed in parallel.
Since both input and the output can differ, we chose to pair them.
The new input pair will often contain repetitions, which can be reduced using the
domain-restriction and domain-reduction operators. Using additional range-modifying operators
such as $\nabla$, decide which result argument is chosen; this might be the first or the latter
or, in case that $\beta = \gamma$, and $\beta$ underlies a lattice structure, the supremum or
infimum of both, or, an arbitrary combination of them.
In any case, although we have strictly speaking a pairing of decisions and not a nesting of
them, we will apply the same notational conventions as for the latter, i.e. as for
flattening.
›
subsection‹Parallel Combinators: Foundations›
text ‹
There are four possible semantics how the decision can be combined, thus there are four
parallel composition operators. For each of them, we prove several properties.
›
definition prod_orA ::"['α↦'β, 'γ ↦'δ] ⇒ ('α×'γ ↦ 'β×'δ)" (infixr "⨂⇩∨⇩A" 55)
where "p1 ⨂⇩∨⇩A p2 =
(λ(x,y). (case p1 x of
⌊allow d1⌋ ⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⌊deny d1⌋⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊deny (d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⊥ ⇒ ⊥))"
lemma prod_orA_mt[simp]:"p ⨂⇩∨⇩A ∅ = ∅"
apply (rule ext)
apply (simp add: prod_orA_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_orA[simp]:"∅ ⨂⇩∨⇩A p = ∅"
apply (rule ext)
apply (simp add: prod_orA_def)
done
lemma prod_orA_quasi_commute: "p2 ⨂⇩∨⇩A p1 = (((λ(x,y). (y,x)) o_f (p1 ⨂⇩∨⇩A p2))) o (λ(a,b).(b,a))"
apply (rule ext)
apply (simp add: prod_orA_def policy_range_comp_def o_def)
apply (auto)[1]
apply (simp split: option.splits decision.splits)
done
definition prod_orD ::"['α ↦ 'β, 'γ ↦ 'δ] ⇒ ('α × 'γ ↦ 'β × 'δ )" (infixr "⨂⇩∨⇩D" 55)
where "p1 ⨂⇩∨⇩D p2 =
(λ(x,y). (case p1 x of
⌊allow d1⌋ ⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊deny(d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⌊deny d1⌋⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊deny(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊deny (d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⊥ ⇒ ⊥))"
lemma prod_orD_mt[simp]:"p ⨂⇩∨⇩D ∅ = ∅"
apply (rule ext)
apply (simp add: prod_orD_def)
apply (auto)[1]
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_orD[simp]:"∅ ⨂⇩∨⇩D p = ∅"
apply (rule ext)
apply (simp add: prod_orD_def)
done
lemma prod_orD_quasi_commute: "p2 ⨂⇩∨⇩D p1 = (((λ(x,y). (y,x)) o_f (p1 ⨂⇩∨⇩D p2))) o (λ(a,b).(b,a))"
apply (rule ext)
apply (simp add: prod_orD_def policy_range_comp_def o_def)
apply (auto)[1]
apply (simp split: option.splits decision.splits)
done
text‹
The following two combinators are by definition non-commutative, but still strict.
›
definition prod_1 :: "['α↦'β, 'γ ↦'δ] ⇒ ('α×'γ ↦ 'β×'δ)" (infixr "⨂⇩1" 55)
where "p1 ⨂⇩1 p2 ≡
(λ(x,y). (case p1 x of
⌊allow d1⌋⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⌊deny d1⌋ ⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊deny(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊deny(d1,d2)⌋
| ⊥ ⇒ ⊥)
|⊥ ⇒ ⊥))"
lemma prod_1_mt[simp]:"p ⨂⇩1 ∅ = ∅"
apply (rule ext)
apply (simp add: prod_1_def)
apply (auto)[1]
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_1[simp]:"∅ ⨂⇩1 p = ∅"
apply (rule ext)
apply (simp add: prod_1_def)
done
definition prod_2 :: "['α↦'β, 'γ ↦'δ] ⇒ ('α×'γ ↦ 'β×'δ)" (infixr "⨂⇩2" 55)
where "p1 ⨂⇩2 p2 ≡
(λ(x,y). (case p1 x of
⌊allow d1⌋ ⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊deny (d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⌊deny d1⌋⇒(case p2 y of
⌊allow d2⌋ ⇒ ⌊allow(d1,d2)⌋
| ⌊deny d2⌋ ⇒ ⌊deny (d1,d2)⌋
| ⊥ ⇒ ⊥)
|⊥ ⇒⊥))"
lemma prod_2_mt[simp]:"p ⨂⇩2 ∅ = ∅"
apply (rule ext)
apply (simp add: prod_2_def)
apply (auto)[1]
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_2[simp]:"∅ ⨂⇩2 p = ∅"
apply (rule ext)
apply (simp add: prod_2_def)
done
definition prod_1_id ::"['α↦'β, 'α↦'γ] ⇒ ('α ↦ 'β×'γ)" (infixr "⨂⇩1⇩I" 55)
where "p ⨂⇩1⇩I q = (p ⨂⇩1 q) o (λx. (x,x))"
lemma prod_1_id_mt[simp]:"p ⨂⇩1⇩I ∅ = ∅"
apply (rule ext)
apply (simp add: prod_1_id_def)
done
lemma mt_prod_1_id[simp]:"∅ ⨂⇩1⇩I p = ∅"
apply (rule ext)
apply (simp add: prod_1_id_def prod_1_def)
done
definition prod_2_id ::"['α↦'β, 'α↦'γ] ⇒ ('α ↦ 'β×'γ)" (infixr "⨂⇩2⇩I" 55)
where"p ⨂⇩2⇩I q = (p ⨂⇩2 q) o (λx. (x,x))"
lemma prod_2_id_mt[simp]:"p ⨂⇩2⇩I ∅ = ∅"
apply (rule ext)
apply (simp add: prod_2_id_def)
done
lemma mt_prod_2_id[simp]:"∅ ⨂⇩2⇩I p = ∅"
apply (rule ext)
apply (simp add: prod_2_id_def prod_2_def)
done
subsection‹Combinators for Transition Policies›
text ‹
For constructing transition policies, two additional combinators are required: one combines
state transitions by pairing the states, the other works equivalently on general maps.
›
definition parallel_map :: "('α ⇀ 'β) ⇒ ('δ ⇀ 'γ) ⇒
('α × 'δ ⇀ 'β × 'γ)" (infixr "⨂⇩M" 60)
where "p1 ⨂⇩M p2 = (λ (x,y). case p1 x of ⌊d1⌋ ⇒
(case p2 y of ⌊d2⌋ ⇒ ⌊(d1,d2)⌋
| ⊥ ⇒ ⊥)
| ⊥ ⇒ ⊥)"
definition parallel_st :: "('i × 'σ ⇀ 'σ) ⇒ ('i × 'σ' ⇀ 'σ') ⇒
('i × 'σ × 'σ' ⇀ 'σ × 'σ')" (infixr "⨂⇩S" 60)
where
"p1 ⨂⇩S p2 = (p1 ⨂⇩M p2) o (λ (a,b,c). ((a,b),a,c))"
subsection‹Range Splitting›
text‹
The following combinator is a special case of both a parallel composition operator and a
range splitting operator. Its primary use case is when combining a policy with state transitions.
›
definition comp_ran_split :: "[('α ⇀ 'γ) × ('α ⇀'γ), 'd ↦ 'β] ⇒ ('d × 'α) ↦ ('β × 'γ)"
(infixr "⨂⇩∇" 100)
where "P ⨂⇩∇ p ≡ λx. case p (fst x) of
⌊allow y⌋ ⇒ (case ((fst P) (snd x)) of ⊥ ⇒ ⊥ | ⌊z⌋ ⇒ ⌊allow (y,z)⌋)
| ⌊deny y⌋ ⇒ (case ((snd P) (snd x)) of ⊥ ⇒ ⊥ | ⌊z⌋ ⇒ ⌊deny (y,z)⌋)
| ⊥ ⇒ ⊥"
text‹An alternative characterisation of the operator is as follows:›
lemma comp_ran_split_charn:
"(f, g) ⨂⇩∇ p = (
(((p ▹ Allow)⨂⇩∨⇩A (A⇩p f)) ⨁
((p ▹ Deny) ⨂⇩∨⇩A (D⇩p g))))"
apply (rule ext)
apply (simp add: comp_ran_split_def map_add_def o_def ran_restrict_def image_def
Allow_def Deny_def dom_restrict_def prod_orA_def
allow_pfun_def deny_pfun_def
split:option.splits decision.splits)
apply (auto)
done
subsection ‹Distributivity of the parallel combinators›
lemma distr_or1_a: "(F = F1 ⨁ F2) ⟹ (((N ⨂⇩1 F) o f) =
(((N ⨂⇩1 F1) o f) ⨁ ((N ⨂⇩1 F2) o f))) "
apply (rule ext)
apply (simp add: prod_1_def map_add_def
split: decision.splits option.splits)
subgoal for x
apply (case_tac "f x")
apply (simp_all add: prod_1_def map_add_def
split: decision.splits option.splits)
done
done
lemma distr_or1: "(F = F1 ⨁ F2) ⟹ ((g o_f ((N ⨂⇩1 F) o f)) =
((g o_f ((N ⨂⇩1 F1) o f)) ⨁ (g o_f ((N ⨂⇩1 F2) o f)))) "
apply (rule ext)+
apply (simp add: prod_1_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
subgoal for x
apply (case_tac "f x")
apply (simp_all add: prod_1_def map_add_def
split: decision.splits option.splits)
done
done
lemma distr_or2_a: "(F = F1 ⨁ F2) ⟹ (((N ⨂⇩2 F) o f) =
(((N ⨂⇩2 F1) o f) ⨁ ((N ⨂⇩2 F2) o f))) "
apply (rule ext)
apply (simp add: prod_2_id_def prod_2_def map_add_def
split: decision.splits option.splits)
subgoal for x
apply (case_tac "f x")
apply (simp_all add: prod_2_def map_add_def
split: decision.splits option.splits)
done
done
lemma distr_or2: "(F = F1 ⨁ F2) ⟹ ((r o_f ((N ⨂⇩2 F) o f)) =
((r o_f ((N ⨂⇩2 F1) o f)) ⨁ (r o_f ((N ⨂⇩2 F2) o f)))) "
apply (rule ext)
apply (simp add: prod_2_id_def prod_2_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
subgoal for x
apply (case_tac "f x")
apply (simp_all add: prod_2_def map_add_def
split: decision.splits option.splits)
done
done
lemma distr_orA: "(F = F1 ⨁ F2) ⟹ ((g o_f ((N ⨂⇩∨⇩A F) o f)) =
((g o_f ((N ⨂⇩∨⇩A F1) o f)) ⨁ (g o_f ((N ⨂⇩∨⇩A F2) o f)))) "
apply (rule ext)+
apply (simp add: prod_orA_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
subgoal for x
apply (case_tac "f x")
apply (simp_all add: map_add_def
split: decision.splits option.splits)
done
done
lemma distr_orD: "(F = F1 ⨁ F2) ⟹ ((g o_f ((N ⨂⇩∨⇩D F) o f)) =
((g o_f ((N ⨂⇩∨⇩D F1) o f)) ⨁ (g o_f ((N ⨂⇩∨⇩D F2) o f)))) "
apply (rule ext)+
apply (simp add: prod_orD_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
subgoal for x
apply (case_tac "f x")
apply (simp_all add: map_add_def
split: decision.splits option.splits)
done
done
lemma coerc_assoc: "(r o_f P) o d = r o_f (P o d)"
apply (simp add: policy_range_comp_def)
apply (rule ext)
apply (simp split: option.splits decision.splits)
done
lemmas ParallelDefs = prod_orA_def prod_orD_def prod_1_def prod_2_def parallel_map_def
parallel_st_def comp_ran_split_def
end
Theory Normalisation
section‹Policy Transformations›
theory
Normalisation
imports
SeqComposition
ParallelComposition
begin
text‹
This theory provides the formalisations required for the transformation of UPF policies.
A typical usage scenario can be observed in the firewall case
study~\cite{brucker.ea:formal-fw-testing:2014}.
›
subsection‹Elementary Operators›
text‹
We start by providing several operators and theorems useful when reasoning about a list of
rules which should eventually be interpreted as combined using the standard override operator.
›
text‹
The following definition takes as argument a list of rules and returns a policy where the
rules are combined using the standard override operator.
›
definition list2policy::"('a ↦ 'b) list ⇒ ('a ↦ 'b)" where
"list2policy l = foldr (λ x y. (x ⨁ y)) l ∅"
text‹
Determine the position of element of a list.
›
fun position :: "'α ⇒ 'α list ⇒ nat" where
"position a [] = 0"
|"(position a (x#xs)) = (if a = x then 1 else (Suc (position a xs)))"
text‹
Provides the first applied rule of a policy given as a list of rules.
›
fun applied_rule where
"applied_rule C a (x#xs) = (if a ∈ dom (C x) then (Some x)
else (applied_rule C a xs))"
|"applied_rule C a [] = None"
text ‹
The following is used if the list is constructed backwards.
›
definition applied_rule_rev where
"applied_rule_rev C a x = applied_rule C a (rev x)"
text‹
The following is a typical policy transformation. It can be applied to any type of policy and
removes all the rules from a policy with an empty domain. It takes two arguments: a semantic
interpretation function and a list of rules.
›
fun rm_MT_rules where
"rm_MT_rules C (x#xs) = (if dom (C x)= {}
then rm_MT_rules C xs
else x#(rm_MT_rules C xs))"
|"rm_MT_rules C [] = []"
text ‹
The following invariant establishes that there are no rules with an empty domain in a list
of rules.
›
fun none_MT_rules where
"none_MT_rules C (x#xs) = (dom (C x) ≠ {} ∧ (none_MT_rules C xs))"
|"none_MT_rules C [] = True"
text‹
The following related invariant establishes that the policy has not a completely empty domain.
›
fun not_MT where
"not_MT C (x#xs) = (if (dom (C x) = {}) then (not_MT C xs) else True)"
|"not_MT C [] = False"
text‹
Next, a few theorems about the two invariants and the transformation:
›
lemma none_MT_rules_vs_notMT: "none_MT_rules C p ⟹ p ≠ [] ⟹ not_MT C p"
apply (induct p)
apply (simp_all)
done
lemma rmnMT: "none_MT_rules C (rm_MT_rules C p)"
apply (induct p)
apply (simp_all)
done
lemma rmnMT2: "none_MT_rules C p ⟹ (rm_MT_rules C p) = p"
apply (induct p)
apply (simp_all)
done
lemma nMTcharn: "none_MT_rules C p = (∀ r ∈ set p. dom (C r) ≠ {})"
apply (induct p)
apply (simp_all)
done
lemma nMTeqSet: "set p = set s ⟹ none_MT_rules C p = none_MT_rules C s"
apply (simp add: nMTcharn)
done
lemma notMTnMT: "⟦a ∈ set p; none_MT_rules C p⟧ ⟹ dom (C a) ≠ {}"
apply (simp add: nMTcharn)
done
lemma none_MT_rulesconc: "none_MT_rules C (a@[b]) ⟹ none_MT_rules C a"
apply (induct a)
apply (simp_all)
done
lemma nMTtail: "none_MT_rules C p ⟹ none_MT_rules C (tl p)"
apply (induct p)
apply (simp_all)
done
lemma not_MTimpnotMT[simp]: "not_MT C p ⟹ p ≠ []"
apply (auto)
done
lemma SR3nMT: "¬ not_MT C p ⟹ rm_MT_rules C p = []"
apply (induct p)
apply (auto simp: if_splits)
done
lemma NMPcharn: "⟦a ∈ set p; dom (C a) ≠ {}⟧ ⟹ not_MT C p"
apply (induct p)
apply (auto simp: if_splits)
done
lemma NMPrm: "not_MT C p ⟹ not_MT C (rm_MT_rules C p)"
apply (induct p)
apply (simp_all)
done
text‹Next, a few theorems about applied\_rule:›
lemma mrconc: "applied_rule_rev C x p = Some a ⟹ applied_rule_rev C x (b#p) = Some a"
proof (induct p rule: rev_induct)
case Nil show ?case using Nil
by (simp add: applied_rule_rev_def)
next
case (snoc xs x) show ?case using snoc
apply (simp add: applied_rule_rev_def if_splits)
by (metis option.inject)
qed
lemma mreq_end: "⟦applied_rule_rev C x b = Some r; applied_rule_rev C x c = Some r⟧ ⟹
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
by (simp add: mrconc)
lemma mrconcNone: "applied_rule_rev C x p = None ⟹
applied_rule_rev C x (b#p) = applied_rule_rev C x [b]"
proof (induct p rule: rev_induct)
case Nil show ?case
by (simp add: applied_rule_rev_def)
next
case (snoc ys y) show ?case using snoc
proof (cases "x ∈ dom (C ys)")
case True show ?thesis using True snoc
by (auto simp: applied_rule_rev_def)
next
case False show ?thesis using False snoc
by (auto simp: applied_rule_rev_def)
qed
qed
lemma mreq_endNone: "⟦applied_rule_rev C x b = None; applied_rule_rev C x c = None⟧ ⟹
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
by (metis mrconcNone)
lemma mreq_end2: "applied_rule_rev C x b = applied_rule_rev C x c ⟹
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
apply (case_tac "applied_rule_rev C x b = None")
apply (auto intro: mreq_end mreq_endNone)
done
lemma mreq_end3: "applied_rule_rev C x p ≠ None ⟹
applied_rule_rev C x (b # p) = applied_rule_rev C x (p)"
by (auto simp: mrconc)
lemma mrNoneMT: "⟦r ∈ set p; applied_rule_rev C x p = None⟧ ⟹
x ∉ dom (C r)"
proof (induct p rule: rev_induct)
case Nil show ?case using Nil
by (simp add: applied_rule_rev_def)
next
case (snoc y ys) show ?case using snoc
proof (cases "r ∈ set ys")
case True show ?thesis using snoc True
by (simp add: applied_rule_rev_def split: if_split_asm)
next
case False show ?thesis using snoc False
by (simp add: applied_rule_rev_def split: if_split_asm)
qed
qed
subsection‹Distributivity of the Transformation.›
text‹
The scenario is the following (can be applied iteratively):
\begin{itemize}
\item Two policies are combined using one of the parallel combinators
\item (e.g. P = P1 P2) (At least) one of the constituent policies has
\item a normalisation procedures, which as output produces a list of
\item policies that are semantically equivalent to the original policy if
\item combined from left to right using the override operator.
\end{itemize}
›
text‹
The following function is crucial for the distribution. Its arguments are a policy, a list
of policies, a parallel combinator, and a range and a domain coercion function.
›
fun prod_list :: "('α ↦'β) ⇒ (('γ ↦'δ) list) ⇒
(('α ↦'β) ⇒ ('γ ↦'δ) ⇒ (('α × 'γ) ↦ ('β × 'δ))) ⇒
(('β × 'δ) ⇒ 'y) ⇒ ('x ⇒ ('α × 'γ)) ⇒
(('x ↦ 'y) list)" (infixr "⨂⇩L" 54) where
"prod_list x (y#ys) par_comb ran_adapt dom_adapt =
((ran_adapt o_f ((par_comb x y) o dom_adapt))#(prod_list x ys par_comb ran_adapt dom_adapt))"
| "prod_list x [] par_comb ran_adapt dom_adapt = []"
text‹
An instance, as usual there are four of them.
›
definition prod_2_list :: "[('α ↦'β), (('γ ↦'δ) list)] ⇒
(('β × 'δ) ⇒ 'y) ⇒ ('x ⇒ ('α × 'γ)) ⇒
(('x ↦ 'y) list)" (infixr "⨂⇩2⇩L" 55) where
"x ⨂⇩2⇩L y = (λ d r. (x ⨂⇩L y) (⨂⇩2) d r)"
lemma list2listNMT: "x ≠ [] ⟹ map sem x ≠ []"
apply (case_tac x)
apply (simp_all)
done
lemma two_conc: "(prod_list x (y#ys) p r d) = ((r o_f ((p x y) o d))#(prod_list x ys p r d))"
by simp
text‹
The following two invariants establish if the law of distributivity holds for a combinator
and if an operator is strict regarding undefinedness.
›
definition is_distr where
"is_distr p = (λ g f. (∀ N P1 P2. ((g o_f ((p N (P1 ⨁ P2)) o f)) =
((g o_f ((p N P1) o f)) ⨁ (g o_f ((p N P2) o f))))))"
definition is_strict where
"is_strict p = (λ r d. ∀ P1. (r o_f (p P1 ∅ ∘ d)) = ∅)"
lemma is_distr_orD: "is_distr (⨂⇩∨⇩D) d r"
apply (simp add: is_distr_def)
apply (rule allI)+
apply (rule distr_orD)
apply (simp)
done
lemma is_strict_orD: "is_strict (⨂⇩∨⇩D) d r"
apply (simp add: is_strict_def)
apply (simp add: policy_range_comp_def)
done
lemma is_distr_2: "is_distr (⨂⇩2) d r"
apply (simp add: is_distr_def)
apply (rule allI)+
apply (rule distr_or2)
by simp
lemma is_strict_2: "is_strict (⨂⇩2) d r"
apply (simp only: is_strict_def)
apply simp
apply (simp add: policy_range_comp_def)
done
lemma domStart: "t ∈ dom p1 ⟹ (p1 ⨁ p2) t = p1 t"
apply (simp add: map_add_dom_app_simps)
done
lemma notDom: "x ∈ dom A ⟹ ¬ A x = None"
apply auto
done
text‹
The following theorems are crucial: they establish the correctness of the distribution.
›
lemma Norm_Distr_1: "((r o_f (((⨂⇩1) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩1) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩1 p) ∘ d))")
case True show ?thesis using True
by (auto simp: list2policy_def policy_range_comp_def prod_1_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: list2policy_def policy_range_comp_def map_add_dom_app_simps(3) prod_1_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_2: "((r o_f (((⨂⇩2) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩2) r d)) x))"proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩2 p) ∘ d))")
case True show ?thesis using True
by (auto simp: list2policy_def prod_2_def policy_range_comp_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_2_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_A: "((r o_f (((⨂⇩∨⇩A) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩∨⇩A) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩∨⇩A p) ∘ d))")
case True show ?thesis using True
by (auto simp: policy_range_comp_def list2policy_def prod_orA_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orA_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_D: "((r o_f (((⨂⇩∨⇩D) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩∨⇩D) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩∨⇩D p) ∘ d))")
case True show ?thesis using True
by (auto simp: policy_range_comp_def list2policy_def prod_orD_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orD_def
split: option.splits decision.splits prod.splits)
qed
qed
text ‹Some domain reasoning›
lemma domSubsetDistr1: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩1 B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_1_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistr2: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩2 B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_2_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistrA: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩∨⇩A B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_orA_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistrD: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩∨⇩D B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_orD_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
end
Theory NormalisationTestSpecification
section ‹Policy Transformation for Testing›
theory
NormalisationTestSpecification
imports
Normalisation
begin
text‹
This theory provides functions and theorems which are useful if one wants to test policy
which are transformed. Most exist in two versions: one where the domains of the rules
of the list (which is the result of a transformation) are pairwise disjoint, and one where
this applies not for the last rule in a list (which is usually a default rules).
The examples in the firewall case study provide a good documentation how these theories can
be applied.
›
text‹
This invariant establishes that the domains of a list of rules are pairwise disjoint.
›
fun disjDom where
"disjDom (x#xs) = ((∀y∈(set xs). dom x ∩ dom y = {}) ∧ disjDom xs)"
|"disjDom [] = True"
fun PUTList :: "('a ↦ 'b) ⇒ 'a ⇒ ('a ↦ 'b) list ⇒ bool"
where
"PUTList PUT x (p#ps) = ((x ∈ dom p ⟶ (PUT x = p x)) ∧ (PUTList PUT x ps))"
|"PUTList PUT x [] = True"
lemma distrPUTL1: "x ∈ dom P ⟹ (list2policy PL) x = P x
⟹ (PUTList PUT x PL ⟹ (PUT x = P x))"
apply (induct PL)
apply (auto simp: list2policy_def dom_def)
done
lemma PUTList_None: "x ∉ dom (list2policy list) ⟹ PUTList PUT x list"
apply (induct list)
apply (auto simp: list2policy_def dom_def)
done
lemma PUTList_DomMT:
"(∀y∈set list. dom a ∩ dom y = {}) ⟹ x ∈ (dom a) ⟹ x ∉ dom (list2policy list)"
apply (induct list)
apply (auto simp: dom_def list2policy_def)
done
lemma distrPUTL2:
"x ∈ dom P ⟹ (list2policy PL) x = P x ⟹ disjDom PL ⟹ (PUT x = P x) ⟹ PUTList PUT x PL "
apply (induct PL)
apply (simp_all add: list2policy_def)
apply (auto)[1]
subgoal for a PL p
apply (case_tac "x ∈ dom a")
apply (case_tac "list2policy PL x = P x")
apply (simp add: list2policy_def)
apply (rule PUTList_None)
apply (rule_tac a = a in PUTList_DomMT)
apply (simp_all add: list2policy_def dom_def)
done
done
lemma distrPUTL:
"⟦x ∈ dom P; (list2policy PL) x = P x; disjDom PL⟧ ⟹ (PUT x = P x) = PUTList PUT x PL "
apply (rule iffI)
apply (rule distrPUTL2)
apply (simp_all)
apply (rule_tac PL = PL in distrPUTL1)
apply (auto)
done
text‹
It makes sense to cater for the common special case where the normalisation returns a list
where the last element is a default-catch-all rule. It seems easier to cater for this globally,
rather than to require the normalisation procedures to do this.
›
fun gatherDomain_aux where
"gatherDomain_aux (x#xs) = (dom x ∪ (gatherDomain_aux xs))"
|"gatherDomain_aux [] = {}"
definition gatherDomain where "gatherDomain p = (gatherDomain_aux (butlast p))"
definition PUTListGD where "PUTListGD PUT x p =
(((x ∉ (gatherDomain p) ∧ x ∈ dom (last p)) ⟶ PUT x = (last p) x) ∧
(PUTList PUT x (butlast p)))"
definition disjDomGD where "disjDomGD p = disjDom (butlast p)"
lemma distrPUTLG1: "⟦x ∈ dom P; (list2policy PL) x = P x; PUTListGD PUT x PL⟧ ⟹ PUT x = P x"
apply (induct PL)
apply (simp_all add: domIff PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def)
apply (auto simp: dom_def domIff split: if_split_asm)
done
lemma distrPUTLG2:
"PL ≠ [] ⟹ x ∈ dom P ⟹ (list2policy (PL)) x = P x ⟹ disjDomGD PL ⟹
(PUT x = P x) ⟹ PUTListGD PUT x (PL)"
apply (simp add: PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def)
apply (induct PL)
apply (auto)
apply (metis PUTList_DomMT PUTList_None domI)
done
lemma distrPUTLG:
"⟦x ∈ dom P; (list2policy PL) x = P x; disjDomGD PL; PL ≠ []⟧ ⟹
(PUT x = P x) = PUTListGD PUT x PL "
apply (rule iffI)
apply (rule distrPUTLG2)
apply (simp_all)
apply (rule_tac PL = PL in distrPUTLG1)
apply (auto)
done
end
Theory Analysis
section‹Properties on Policies›
theory
Analysis
imports
ParallelComposition
SeqComposition
begin
text ‹
In this theory, several standard policy properties are paraphrased in UPF terms.
›
subsection‹Basic Properties›
subsubsection‹A Policy Has no Gaps›
definition gap_free :: "('a ↦ 'b) ⇒ bool"
where "gap_free p = (dom p = UNIV)"
subsubsection‹Comparing Policies›
text ‹Policy p is more defined than q:›
definition more_defined :: "('a ↦ 'b) ⇒('a ↦ 'b) ⇒bool"
where "more_defined p q = (dom q ⊆ dom p)"
definition strictly_more_defined :: "('a ↦ 'b) ⇒('a ↦ 'b) ⇒bool"
where "strictly_more_defined p q = (dom q ⊂ dom p)"
lemma strictly_more_vs_more: "strictly_more_defined p q ⟹ more_defined p q"
unfolding more_defined_def strictly_more_defined_def
by auto
text‹Policy p is more permissive than q:›
definition more_permissive :: "('a ↦ 'b) ⇒ ('a ↦ 'b) ⇒ bool" (infixl "⊑⇩A" 60)
where " p ⊑⇩A q = (∀ x. (case q x of ⌊allow y⌋ ⇒ (∃ z. (p x = ⌊allow z⌋))
| ⌊deny y⌋ ⇒ True
| ⊥ ⇒ True))"
lemma more_permissive_refl : "p ⊑⇩A p "
unfolding more_permissive_def
by(auto split : option.split decision.split)
lemma more_permissive_trans : "p ⊑⇩A p' ⟹ p' ⊑⇩A p'' ⟹ p ⊑⇩A p''"
unfolding more_permissive_def
apply(auto split : option.split decision.split)
subgoal for x y
apply(erule_tac x = x and
P = "λx. case p'' x of ⊥ ⇒ True
| ⌊allow y⌋ ⇒ ∃z. p' x = ⌊allow z⌋
| ⌊deny y⌋ ⇒ True" in allE)
apply(simp, elim exE)
by(erule_tac x = x in allE, simp)
done
text‹Policy p is more rejective than q:›
definition more_rejective :: "('a ↦ 'b) ⇒ ('a ↦ 'b) ⇒ bool" (infixl "⊑⇩D" 60)
where " p ⊑⇩D q = (∀ x. (case q x of ⌊deny y⌋ ⇒ (∃ z. (p x = ⌊deny z⌋))
| ⌊allow y⌋ ⇒ True
| ⊥ ⇒ True))"
lemma more_rejective_trans : "p ⊑⇩D p' ⟹ p' ⊑⇩D p'' ⟹ p ⊑⇩D p''"
unfolding more_rejective_def
apply(auto split : option.split decision.split)
subgoal for x y
apply(erule_tac x = x and
P = "λx. case p'' x of ⊥ ⇒ True
| ⌊allow y⌋ ⇒ True
| ⌊deny y⌋ ⇒ ∃z. p' x = ⌊deny z⌋" in allE)
apply(simp, elim exE)
by(erule_tac x = x in allE, simp)
done
lemma more_rejective_refl : "p ⊑⇩D p "
unfolding more_rejective_def
by(auto split : option.split decision.split)
lemma "A⇩f f ⊑⇩A p"
unfolding more_permissive_def allow_all_fun_def allow_pfun_def
by(auto split: option.split decision.split)
lemma "A⇩I ⊑⇩A p"
unfolding more_permissive_def allow_all_fun_def allow_pfun_def allow_all_id_def
by(auto split: option.split decision.split)
subsection‹Combined Data-Policy Refinement›
definition policy_refinement ::
"('a ↦ 'b) ⇒ ('a' ⇒ 'a) ⇒('b' ⇒ 'b) ⇒ ('a' ↦ 'b') ⇒ bool"
("_ ⊑⇘_⇙⇩,⇘_⇙ _" [50,50,50,50]50)
where "p ⊑⇘abs⇩a⇙⇩,⇘abs⇩b⇙ q ≡
(∀ a. case p a of
⊥ ⇒ True
| ⌊allow y⌋ ⇒ (∀ a'∈{x. abs⇩a x=a}.
∃ b'. q a' = ⌊allow b'⌋
∧ abs⇩b b' = y)
| ⌊deny y⌋ ⇒ (∀ a'∈{x. abs⇩a x=a}.
∃ b'. q a' = ⌊deny b'⌋
∧ abs⇩b b' = y))"
theorem polref_refl: "p ⊑⇘id⇙⇩,⇘id⇙ p"
unfolding policy_refinement_def
by(auto split: option.split decision.split)
theorem polref_trans:
assumes A: "p ⊑⇘f⇙⇩,⇘g⇙ p'"
and B: "p' ⊑⇘f'⇙⇩,⇘g'⇙ p''"
shows "p ⊑⇘f o f'⇙⇩,⇘g o g'⇙ p''"
apply(insert A B)
unfolding policy_refinement_def
apply(auto split: option.split decision.split simp: o_def)[1]
subgoal for a a'
apply(erule_tac x="f (f' a')" in allE, simp)[1]
apply(erule_tac x="f' a'" in allE, auto)[1]
apply(erule_tac x=" (f' a')" in allE, auto)[1]
done
subgoal for a a'
apply(erule_tac x="f (f' a')" in allE, simp)[1]
apply(erule_tac x="f' a'" in allE, auto)[1]
apply(erule_tac x=" (f' a')" in allE, auto)[1]
done
done
subsection ‹Equivalence of Policies›
subsubsection‹Equivalence over domain D›
definition p_eq_dom :: "('a ↦ 'b) ⇒ 'a set ⇒ ('a ↦ 'b) ⇒bool" ("_ ≈⇘_⇙ _" [60,60,60]60)
where "p ≈⇘D⇙ q = (∀x∈D. p x = q x)"
text‹p and q have no conflicts›
definition no_conflicts :: "('a ↦ 'b) ⇒('a ↦ 'b) ⇒bool" where
"no_conflicts p q = (dom p = dom q ∧ (∀x∈(dom p).
(case p x of ⌊allow y⌋ ⇒ (∃z. q x = ⌊allow z⌋)
| ⌊deny y⌋ ⇒ (∃z. q x = ⌊deny z⌋))))"
lemma policy_eq:
assumes p_over_qA: "p ⊑⇩A q "
and q_over_pA: "q ⊑⇩A p"
and p_over_qD: "q ⊑⇩D p"
and q_over_pD: "p ⊑⇩D q"
and dom_eq: "dom p = dom q"
shows "no_conflicts p q"
apply (insert p_over_qA q_over_pA p_over_qD q_over_pD dom_eq)
apply (simp add: no_conflicts_def more_permissive_def more_rejective_def
split: option.splits decision.splits)
apply (safe)
apply (metis domI domIff dom_eq)
apply (metis)+
done
subsubsection‹Miscellaneous›
lemma dom_inter: "⟦dom p ∩ dom q = {}; p x = ⌊y⌋⟧ ⟹ q x = ⊥"
by (auto)
lemma dom_eq: "dom p ∩ dom q = {} ⟹ p ⨁⇩A q = p ⨁⇩D q"
unfolding override_A_def override_D_def
by (rule ext, auto simp: dom_def split: prod.splits option.splits decision.splits )
lemma dom_split_alt_def : "(f, g) Δ p = (dom(p ▹ Allow) ◃ (A⇩f f)) ⨁ (dom(p ▹ Deny) ◃ (D⇩f g))"
apply (rule ext)
apply (simp add: dom_split2_def Allow_def Deny_def dom_restrict_def
deny_all_fun_def allow_all_fun_def map_add_def)
apply (simp split: option.splits decision.splits)
apply (auto simp: map_add_def o_def deny_pfun_def ran_restrict_def image_def)
done
end
Theory UPF
section ‹Putting Everything Together: UPF›
theory
UPF
imports
Normalisation
NormalisationTestSpecification
Analysis
begin
text‹
This is the top-level theory for the Unified Policy Framework (UPF) and, thus,
builds the base theory for using UPF. For the moment, we only define a set of
lemmas for all core UPF definitions that is useful for using UPF:
›
lemmas UPFDefs = UPFCoreDefs ParallelDefs ElementaryPoliciesDefs
end
Theory Service
section ‹Secure Service Specification›
theory
Service
imports
UPF
begin
text ‹
In this section, we model a simple Web service and its access control model
that allows the staff in a hospital to access health care records of patients.
›
subsection‹Datatypes for Modelling Users and Roles›
subsubsection ‹Users›
text‹
First, we introduce a type for users that we use to model that each
staff member has a unique id:
›
type_synonym user = int
text ‹
Similarly, each patient has a unique id:
›
type_synonym patient = int
subsubsection ‹Roles and Relationships›
text‹In our example, we assume three different roles for members of the clinical staff:›
datatype role = ClinicalPractitioner | Nurse | Clerical
text‹
We model treatment relationships (legitimate relationships) between staff and patients
(respectively, their health records. This access control model is inspired by our detailed
NHS model.
›
type_synonym lr_id = int
type_synonym LR = "lr_id ⇀ (user set)"
text‹The security context stores all the existing LRs.›
type_synonym Σ = "patient ⇀ LR"
text‹The user context stores the roles the users are in.›
type_synonym υ = "user ⇀ role"
subsection ‹Modelling Health Records and the Web Service API›
subsubsection ‹Health Records›
text ‹The content and the status of the entries of a health record›
datatype data = dummyContent
datatype status = Open | Closed
type_synonym entry_id = int
type_synonym entry = "status × user × data"
type_synonym SCR = "(entry_id ⇀ entry)"
type_synonym DB = "patient ⇀ SCR"
subsubsection ‹The Web Service API›
text‹The operations provided by the service:›
datatype Operation = createSCR user role patient
| appendEntry user role patient entry_id entry
| deleteEntry user role patient entry_id
| readEntry user role patient entry_id
| readSCR user role patient
| addLR user role patient lr_id "(user set)"
| removeLR user role patient lr_id
| changeStatus user role patient entry_id status
| deleteSCR user role patient
| editEntry user role patient entry_id entry
fun is_createSCR where
"is_createSCR (createSCR u r p) = True"
|"is_createSCR x = False"
fun is_appendEntry where
"is_appendEntry (appendEntry u r p e ei) = True"
|"is_appendEntry x = False"
fun is_deleteEntry where
"is_deleteEntry (deleteEntry u r p e_id) = True"
|"is_deleteEntry x = False"
fun is_readEntry where
"is_readEntry (readEntry u r p e) = True"
|"is_readEntry x = False"
fun is_readSCR where
"is_readSCR (readSCR u r p) = True"
|"is_readSCR x = False"
fun is_changeStatus where
"is_changeStatus (changeStatus u r p s ei) = True"
|"is_changeStatus x = False"
fun is_deleteSCR where
"is_deleteSCR (deleteSCR u r p) = True"
|"is_deleteSCR x = False"
fun is_addLR where
"is_addLR (addLR u r lrid lr us) = True"
|"is_addLR x = False"
fun is_removeLR where
"is_removeLR (removeLR u r p lr) = True"
|"is_removeLR x = False"
fun is_editEntry where
"is_editEntry (editEntry u r p e_id s) = True"
|"is_editEntry x = False"
fun SCROp :: "(Operation × DB) ⇀ SCR" where
"SCROp ((createSCR u r p), S) = S p"
|"SCROp ((appendEntry u r p ei e), S) = S p"
|"SCROp ((deleteEntry u r p e_id), S) = S p"
|"SCROp ((readEntry u r p e), S) = S p"
|"SCROp ((readSCR u r p), S) = S p"
|"SCROp ((changeStatus u r p s ei),S) = S p"
|"SCROp ((deleteSCR u r p),S) = S p"
|"SCROp ((editEntry u r p e_id s),S) = S p"
|"SCROp x = ⊥"
fun patientOfOp :: "Operation ⇒ patient" where
"patientOfOp (createSCR u r p) = p"
|"patientOfOp (appendEntry u r p e ei) = p"
|"patientOfOp (deleteEntry u r p e_id) = p"
|"patientOfOp (readEntry u r p e) = p"
|"patientOfOp (readSCR u r p) = p"
|"patientOfOp (changeStatus u r p s ei) = p"
|"patientOfOp (deleteSCR u r p) = p"
|"patientOfOp (addLR u r p lr ei) = p"
|"patientOfOp (removeLR u r p lr) = p"
|"patientOfOp (editEntry u r p e_id s) = p"
fun userOfOp :: "Operation ⇒ user" where
"userOfOp (createSCR u r p) = u"
|"userOfOp (appendEntry u r p e ei) = u"
|"userOfOp (deleteEntry u r p e_id) = u"
|"userOfOp (readEntry u r p e) = u"
|"userOfOp (readSCR u r p) = u"
|"userOfOp (changeStatus u r p s ei) = u"
|"userOfOp (deleteSCR u r p) = u"
|"userOfOp (editEntry u r p e_id s) = u"
|"userOfOp (addLR u r p lr ei) = u"
|"userOfOp (removeLR u r p lr) = u"
fun roleOfOp :: "Operation ⇒ role" where
"roleOfOp (createSCR u r p) = r"
|"roleOfOp (appendEntry u r p e ei) = r"
|"roleOfOp (deleteEntry u r p e_id) = r"
|"roleOfOp (readEntry u r p e) = r"
|"roleOfOp (readSCR u r p) = r"
|"roleOfOp (changeStatus u r p s ei) = r"
|"roleOfOp (deleteSCR u r p) = r"
|"roleOfOp (editEntry u r p e_id s) = r"
|"roleOfOp (addLR u r p lr ei) = r"
|"roleOfOp (removeLR u r p lr) = r"
fun contentOfOp :: "Operation ⇒ data" where
"contentOfOp (appendEntry u r p ei e) = (snd (snd e))"
|"contentOfOp (editEntry u r p ei e) = (snd (snd e))"
fun contentStatic :: "Operation ⇒ bool" where
"contentStatic (appendEntry u r p ei e) = ((snd (snd e)) = dummyContent)"
|"contentStatic (editEntry u r p ei e) = ((snd (snd e)) = dummyContent)"
|"contentStatic x = True"
fun allContentStatic where
"allContentStatic (x#xs) = (contentStatic x ∧ allContentStatic xs)"
|"allContentStatic [] = True"
subsection‹Modelling Access Control›
text ‹
In the following, we define a rather complex access control model for our
scenario that extends traditional role-based access control
(RBAC)~\cite{sandhu.ea:role-based:1996} with treatment relationships and sealed
envelopes. Sealed envelopes (see~\cite{bruegger:generation:2012} for details)
are a variant of break-the-glass access control (see~\cite{brucker.ea:extending:2009}
for a general motivation and explanation of break-the-glass access control).
›
subsubsection ‹Sealed Envelopes›
type_synonym SEPolicy = "(Operation × DB ↦ unit) "
definition get_entry:: "DB ⇒ patient ⇒ entry_id ⇒ entry option" where
"get_entry S p e_id = (case S p of ⊥ ⇒ ⊥
| ⌊Scr⌋ ⇒ Scr e_id)"
definition userHasAccess:: "user ⇒ entry ⇒ bool" where
"userHasAccess u e = ((fst e) = Open ∨ (fst (snd e) = u))"
definition readEntrySE :: SEPolicy where
"readEntrySE x = (case x of (readEntry u r p e_id,S) ⇒ (case get_entry S p e_id of
⊥ ⇒ ⊥
| ⌊e⌋ ⇒ (if (userHasAccess u e)
then ⌊allow ()⌋
else ⌊deny ()⌋ ))
| x ⇒ ⊥)"
definition deleteEntrySE :: SEPolicy where
"deleteEntrySE x = (case x of (deleteEntry u r p e_id,S) ⇒ (case get_entry S p e_id of
⊥ ⇒ ⊥
| ⌊e⌋ ⇒ (if (userHasAccess u e)
then ⌊allow ()⌋
else ⌊deny ()⌋))
| x ⇒ ⊥)"
definition editEntrySE :: SEPolicy where
"editEntrySE x = (case x of (editEntry u r p e_id s,S) ⇒ (case get_entry S p e_id of
⊥ ⇒ ⊥
| ⌊e⌋ ⇒ (if (userHasAccess u e)
then ⌊allow ()⌋
else ⌊deny ()⌋))
| x ⇒ ⊥)"
definition SEPolicy :: SEPolicy where
"SEPolicy = editEntrySE ⨁ deleteEntrySE ⨁ readEntrySE ⨁ A⇩U"
lemmas SEsimps = SEPolicy_def get_entry_def userHasAccess_def
editEntrySE_def deleteEntrySE_def readEntrySE_def
subsubsection ‹Legitimate Relationships›
type_synonym LRPolicy = "(Operation × Σ, unit) policy"
fun hasLR:: "user ⇒ patient ⇒ Σ ⇒ bool" where
"hasLR u p Σ = (case Σ p of ⊥ ⇒ False
| ⌊lrs⌋ ⇒ (∃lr. lr∈(ran lrs) ∧ u ∈ lr))"
definition LRPolicy :: LRPolicy where
"LRPolicy = (λ(x,y). (if hasLR (userOfOp x) (patientOfOp x) y
then ⌊allow ()⌋
else ⌊deny ()⌋))"
definition createSCRPolicy :: LRPolicy where
"createSCRPolicy x = (if (is_createSCR (fst x))
then ⌊allow ()⌋
else ⊥)"
definition addLRPolicy :: LRPolicy where
"addLRPolicy x = (if (is_addLR (fst x))
then ⌊allow ()⌋
else ⊥)"
definition LR_Policy where "LR_Policy = createSCRPolicy ⨁ addLRPolicy ⨁ LRPolicy ⨁ A⇩U"
lemmas LRsimps = LR_Policy_def createSCRPolicy_def addLRPolicy_def LRPolicy_def
type_synonym FunPolicy = "(Operation × DB × Σ,unit) policy"
fun createFunPolicy :: FunPolicy where
"createFunPolicy ((createSCR u r p),(D,S)) = (if p ∈ dom D
then ⌊deny ()⌋
else ⌊allow ()⌋)"
|"createFunPolicy x = ⊥"
fun addLRFunPolicy :: FunPolicy where
"addLRFunPolicy ((addLR u r p l us),(D,S)) = (if l ∈ dom S
then ⌊deny ()⌋
else ⌊allow ()⌋)"
|"addLRFunPolicy x = ⊥"
fun removeLRFunPolicy :: FunPolicy where
"removeLRFunPolicy ((removeLR u r p l),(D,S)) = (if l ∈ dom S
then ⌊allow ()⌋
else ⌊deny ()⌋)"
|"removeLRFunPolicy x = ⊥"
fun readSCRFunPolicy :: FunPolicy where
"readSCRFunPolicy ((readSCR u r p),(D,S)) = (if p ∈ dom D
then ⌊allow ()⌋
else ⌊deny ()⌋)"
|"readSCRFunPolicy x = ⊥"
fun deleteSCRFunPolicy :: FunPolicy where
"deleteSCRFunPolicy ((deleteSCR u r p),(D,S)) = (if p ∈ dom D
then ⌊allow ()⌋
else ⌊deny ()⌋)"
|"deleteSCRFunPolicy x = ⊥"
fun changeStatusFunPolicy :: FunPolicy where
"changeStatusFunPolicy (changeStatus u r p e s,(d,S)) =
(case d p of ⌊x⌋ ⇒ (if e ∈ dom x
then ⌊allow ()⌋
else ⌊deny ()⌋)
| _ ⇒ ⌊deny ()⌋)"
|"changeStatusFunPolicy x = ⊥"
fun deleteEntryFunPolicy :: FunPolicy where
"deleteEntryFunPolicy (deleteEntry u r p e,(d,S)) =
(case d p of ⌊x⌋ ⇒ (if e ∈ dom x
then ⌊allow ()⌋
else ⌊deny ()⌋)
| _ ⇒ ⌊deny ()⌋)"
|"deleteEntryFunPolicy x = ⊥"
fun readEntryFunPolicy :: FunPolicy where
"readEntryFunPolicy (readEntry u r p e,(d,S)) =
(case d p of ⌊x⌋ ⇒ (if e ∈ dom x
then ⌊allow ()⌋
else ⌊deny ()⌋)
| _ ⇒ ⌊deny ()⌋)"
|"readEntryFunPolicy x = ⊥"
fun appendEntryFunPolicy :: FunPolicy where
"appendEntryFunPolicy (appendEntry u r p e ed,(d,S)) =
(case d p of ⌊x⌋ ⇒ (if e ∈ dom x
then ⌊deny ()⌋
else ⌊allow ()⌋)
| _ ⇒ ⌊deny ()⌋)"
|"appendEntryFunPolicy x = ⊥"
fun editEntryFunPolicy :: FunPolicy where
"editEntryFunPolicy (editEntry u r p ei e,(d,S)) =
(case d p of ⌊x⌋ ⇒ (if ei ∈ dom x
then ⌊allow ()⌋
else ⌊deny ()⌋)
| _ ⇒ ⌊deny ()⌋)"
|"editEntryFunPolicy x = ⊥"
definition FunPolicy where
"FunPolicy = editEntryFunPolicy ⨁ appendEntryFunPolicy ⨁
readEntryFunPolicy ⨁ deleteEntryFunPolicy ⨁
changeStatusFunPolicy ⨁ deleteSCRFunPolicy ⨁
removeLRFunPolicy ⨁ readSCRFunPolicy ⨁
addLRFunPolicy ⨁ createFunPolicy ⨁ A⇩U"
subsubsection‹Modelling Core RBAC›
type_synonym RBACPolicy = "Operation × υ ↦ unit"
definition RBAC :: "(role × Operation) set" where
"RBAC = {(r,f). r = Nurse ∧ is_readEntry f} ∪
{(r,f). r = Nurse ∧ is_readSCR f} ∪
{(r,f). r = ClinicalPractitioner ∧ is_appendEntry f} ∪
{(r,f). r = ClinicalPractitioner ∧ is_deleteEntry f} ∪
{(r,f). r = ClinicalPractitioner ∧ is_readEntry f} ∪
{(r,f). r = ClinicalPractitioner ∧ is_readSCR f} ∪
{(r,f). r = ClinicalPractitioner ∧ is_changeStatus f} ∪
{(r,f). r = ClinicalPractitioner ∧ is_editEntry f} ∪
{(r,f). r = Clerical ∧ is_createSCR f} ∪
{(r,f). r = Clerical ∧ is_deleteSCR f} ∪
{(r,f). r = Clerical ∧ is_addLR f} ∪
{(r,f). r = Clerical ∧ is_removeLR f}"
definition RBACPolicy :: RBACPolicy where
"RBACPolicy = (λ (f,uc).
if ((roleOfOp f,f) ∈ RBAC ∧ ⌊roleOfOp f⌋ = uc (userOfOp f))
then ⌊allow ()⌋
else ⌊deny ()⌋)"
subsection ‹The State Transitions and Output Function›
subsubsection‹State Transition›
fun OpSuccessDB :: "(Operation × DB) ⇀ DB" where
"OpSuccessDB (createSCR u r p,S) = (case S p of ⊥ ⇒ ⌊S(p↦∅)⌋
| ⌊x⌋ ⇒ ⌊S⌋)"
|"OpSuccessDB ((appendEntry u r p ei e),S) =
(case S p of ⊥ ⇒ ⌊S⌋
| ⌊x⌋ ⇒ ((if ei ∈ (dom x)
then ⌊S⌋
else ⌊S(p ↦ x(ei↦e))⌋)))"
|"OpSuccessDB ((deleteSCR u r p),S) = (Some (S(p:=⊥)))"
|"OpSuccessDB ((deleteEntry u r p ei),S) =
(case S p of ⊥ ⇒ ⌊S⌋
| ⌊x⌋ ⇒ Some (S(p↦(x(ei:=⊥)))))"
|"OpSuccessDB ((changeStatus u r p ei s),S) =
(case S p of ⊥ ⇒ ⌊S⌋
| ⌊x⌋ ⇒ (case x ei of
⌊e⌋ ⇒ ⌊S(p ↦ x(ei↦(s,snd e)))⌋
| ⊥ ⇒ ⌊S⌋))"
|"OpSuccessDB ((editEntry u r p ei e),S) =
(case S p of ⊥ ⇒⌊S⌋
| ⌊x⌋ ⇒ (case x ei of
⌊e⌋ ⇒ ⌊S(p↦(x(ei↦(e))))⌋
| ⊥ ⇒ ⌊S⌋))"
|"OpSuccessDB (x,S) = ⌊S⌋"
fun OpSuccessSigma :: "(Operation × Σ) ⇀ Σ" where
"OpSuccessSigma (addLR u r p lr_id us,S) =
(case S p of ⌊lrs⌋ ⇒ (case (lrs lr_id) of
⊥ ⇒ ⌊S(p↦(lrs(lr_id↦us)))⌋
| ⌊x⌋ ⇒ ⌊S⌋)
| ⊥ ⇒ ⌊S(p↦(Map.empty(lr_id↦us)))⌋)"
|"OpSuccessSigma (removeLR u r p lr_id,S) =
(case S p of Some lrs ⇒ ⌊S(p↦(lrs(lr_id:=⊥)))⌋
| ⊥ ⇒ ⌊S⌋)"
|"OpSuccessSigma (x,S) = ⌊S⌋"
fun OpSuccessUC :: "(Operation × υ) ⇀ υ" where
"OpSuccessUC (f,u) = ⌊u⌋"
subsubsection ‹Output›
type_synonym Output = unit
fun OpSuccessOutput :: "(Operation) ⇀ Output" where
"OpSuccessOutput x = ⌊()⌋"
fun OpFailOutput :: "Operation ⇀ Output" where
"OpFailOutput x = ⌊()⌋"
subsection ‹Combine All Parts›
definition SE_LR_Policy :: "(Operation × DB × Σ, unit) policy" where
"SE_LR_Policy = (λ(x,x). x) o⇩f (SEPolicy ⨂⇩∨⇩D LR_Policy) o (λ(a,b,c). ((a,b),a,c))"
definition SE_LR_FUN_Policy :: "(Operation × DB × Σ, unit) policy" where
"SE_LR_FUN_Policy = ((λ(x,x). x) o⇩f (FunPolicy ⨂⇩∨⇩D SE_LR_Policy) o (λa. (a,a)))"
definition SE_LR_RBAC_Policy :: "(Operation × DB × Σ × υ, unit) policy" where
"SE_LR_RBAC_Policy = (λ(x,x). x)
o⇩f (RBACPolicy ⨂⇩∨⇩D SE_LR_FUN_Policy)
o (λ(a,b,c,d). ((a,d),(a,b,c)))"
definition ST_Allow :: "Operation × DB × Σ × υ ⇀ Output × DB × Σ × υ"
where "ST_Allow = ((OpSuccessOutput ⨂⇩M (OpSuccessDB ⨂⇩S OpSuccessSigma ⨂⇩S OpSuccessUC))
o ( (λ(a,b,c). ((a),(a,b,c)))))"
definition ST_Deny :: "Operation × DB × Σ × υ ⇀ Output × DB × Σ × υ"
where "ST_Deny = (λ (ope,sp,si,uc). Some ((), sp,si,uc))"
definition SE_LR_RBAC_ST_Policy :: "Operation × DB × Σ × υ ↦ Output × DB × Σ × υ"
where "SE_LR_RBAC_ST_Policy = ((λ (x,y).y)
o⇩f ((ST_Allow,ST_Deny) ⨂⇩∇ SE_LR_RBAC_Policy)
o (λx.(x,x)))"
definition PolMon :: "Operation ⇒ (Output decision,DB × Σ × υ) MON⇩S⇩E"
where "PolMon = (policy2MON SE_LR_RBAC_ST_Policy)"
end
Theory ServiceExample
section ‹Instantiating Our Secure Service Example›
theory
ServiceExample
imports
Service
begin
text ‹
In the following, we briefly present an instantiations of our secure service example
from the last section. We assume three different members of the health care staff and
two patients:
›
subsection ‹Access Control Configuration›
definition alice :: user where "alice = 1"
definition bob :: user where "bob = 2"
definition charlie :: user where "charlie = 3"
definition patient1 :: patient where "patient1 = 5"
definition patient2 :: patient where "patient2 = 6"
definition UC0 :: υ where
"UC0 = Map.empty(alice↦Nurse)(bob↦ClinicalPractitioner)(charlie↦Clerical)"
definition entry1 :: entry where
"entry1 = (Open,alice, dummyContent)"
definition entry2 :: entry where
"entry2 = (Closed,bob, dummyContent)"
definition entry3 :: entry where
"entry3 = (Closed,alice, dummyContent)"
definition SCR1 :: SCR where
"SCR1 = (Map.empty(1↦entry1))"
definition SCR2 :: SCR where
"SCR2 = (Map.empty)"
definition Spine0 :: DB where
"Spine0 = Map.empty(patient1↦SCR1)(patient2↦SCR2)"
definition LR1 :: LR where
"LR1 =(Map.empty(1↦{alice}))"
definition Σ0 :: Σ where
"Σ0 = (Map.empty(patient1↦LR1))"
subsection ‹The Initial System State›
definition σ0 :: "DB × Σ×υ" where
"σ0 = (Spine0,Σ0,UC0)"
subsection‹Basic Properties›
lemma [simp]: "(case a of allow d ⇒ ⌊X⌋ | deny d2 ⇒ ⌊Y⌋) = ⊥ ⟹ False"
by (case_tac a,simp_all)
lemma [cong,simp]:
"((if hasLR urp1_alice 1 Σ0 then ⌊allow ()⌋ else ⌊deny ()⌋) = ⊥) = False"
by (simp)
lemmas MonSimps = valid_SE_def unit_SE_def bind_SE_def
lemmas Psplits = option.splits unit.splits prod.splits decision.splits
lemmas PolSimps = valid_SE_def unit_SE_def bind_SE_def if_splits policy2MON_def
SE_LR_RBAC_ST_Policy_def map_add_def id_def LRsimps prod_2_def RBACPolicy_def
SE_LR_Policy_def SEPolicy_def RBAC_def deleteEntrySE_def editEntrySE_def
readEntrySE_def σ0_def Σ0_def UC0_def patient1_def patient2_def LR1_def
alice_def bob_def charlie_def get_entry_def SE_LR_RBAC_Policy_def Allow_def
Deny_def dom_restrict_def policy_range_comp_def prod_orA_def prod_orD_def
ST_Allow_def ST_Deny_def Spine0_def SCR1_def SCR2_def entry1_def entry2_def
entry3_def FunPolicy_def SE_LR_FUN_Policy_def o_def image_def UPFDefs
lemma "SE_LR_RBAC_Policy ((createSCR alice Clerical patient1),σ0)= Some (deny ())"
by (simp add: PolSimps)
lemma exBool[simp]: "∃a::bool. a"
by auto
lemma deny_allow[simp]: " ⌊deny ()⌋ ∉ Some ` range allow"
by auto
lemma allow_deny[simp]: " ⌊allow ()⌋ ∉ Some ` range deny"
by auto
text‹Policy as monad. Alice using her first urp can read the SCR of patient1.›
lemma
"(σ0 ⊨ (os ← mbind [(createSCR alice Clerical patient1)] (PolMon);
(return (os = [(deny (Out) )]))))"
by (simp add: PolMon_def MonSimps PolSimps)
text‹Presenting her other urp, she is not allowed to read it.›
lemma "SE_LR_RBAC_Policy ((appendEntry alice Clerical patient1 ei d),σ0)= ⌊deny ()⌋"
by (simp add: PolSimps)
end