Theory UPFCore

(*****************************************************************************
 * HOL-TestGen --- theorem-prover based test case generation
 *                 http://www.brucker.ch/projects/hol-testgen/
 *                                                                            
 * UPF
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2005-2012 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2017 Université Paris-Sud, France
 *               2015-2017 The University of Sheffield, UK  
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

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"                             (‹∅›)

syntax_consts
  "_policylet1" ⇌ allow and
  "_policylet2" ⇌ deny and
  "_Maplets" "_MapUpd" ⇌ fun_upd and
  "_emptypolicy" ⇌ Map.empty
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)
syntax_consts
  "_policyoverride" ⇌ map_add
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)
syntax_consts
  "_policyoverride_A" ⇌ override_A
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)
syntax_consts
  "_policyoverride_D" ⇌ override_D
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 ‹of› 55)
syntax_consts
  "_policy_range_comp" ⇌ policy_range_comp
translations
  "p of q" ⇌ "p o_f q"

lemma policy_range_comp_strict : "f of ∅ = ∅"
  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 of 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,'σ) MONSE)"
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