Theory TopoS_Interface

theory TopoS_Interface
imports Main "Lib/FiniteGraph" TopoS_Vertices "Lib/TopoS_Util"
begin



section ‹Security Invariants›
  text‹
    A good documentation of this formalization is available in \<^cite>‹"diekmann2014forte"›. 
›

  text‹
    We define security invariants over a graph.
    The graph corresponds to the network's access control structure.
›

  (*TODO: make datatype!*)
  ― ‹@{typ "'v"} is the type of the nodes in the graph (hosts in the network). 
     @{typ "'a"} is the type of the host attributes.›
  record ('v::vertex, 'a) TopoS_Params =
    node_properties :: "'v::vertex ⇒ 'a option"

text‹
A Security Invariant is defined as locale.

We successively define more and more locales with more and more assumptions.
This clearly depicts which assumptions are necessary to use certain features of a Security Invariant.
In addition, it makes instance proofs of Security Invariants easier, since the lemmas obtained by an (easy, few assumptions) instance proof 
can be used for the complicated (more assumptions) instance proofs.

A security Invariant consists of one function: ‹sinvar›.
Essentially, it is a predicate over the policy (depicted as graph ‹G› and a host attribute mapping (‹nP›)).
›

text ‹A Security Invariant where the offending flows (flows that invalidate the policy) can be defined and calculated.
No assumptions are necessary for this step.
›  
  locale SecurityInvariant_withOffendingFlows = 
    fixes sinvar::"('v::vertex) graph ⇒ ('v::vertex ⇒ 'a) ⇒ bool" ― ‹policy @{text "⇒"} host attribute mapping @{text "⇒"} bool›
   begin
    ― ‹Offending Flows definitions:›
    definition is_offending_flows::"('v × 'v) set ⇒ 'v graph ⇒ ('v ⇒ 'a) ⇒ bool" where
      "is_offending_flows f G nP ≡ ¬ sinvar G nP ∧ sinvar (delete_edges G f) nP"
    
    ― ‹Above definition is not minimal:›
    definition is_offending_flows_min_set::"('v × 'v) set ⇒ 'v graph ⇒ ('v ⇒ 'a) ⇒ bool" where
      "is_offending_flows_min_set f G nP ≡ is_offending_flows f G nP ∧ 
        (∀ (e1, e2) ∈ f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP)"

    ― ‹The set of all offending flows.›
    definition set_offending_flows::"'v graph ⇒ ('v ⇒ 'a) ⇒ ('v × 'v) set set" where
      "set_offending_flows G  nP = {F. F ⊆ (edges G) ∧ is_offending_flows_min_set F G nP}"
  

    text ‹Some of the @{const set_offending_flows} definition›
    lemma offending_not_empty: "⟦ F ∈ set_offending_flows G nP ⟧ ⟹ F ≠ {}"
     by(auto simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    lemma empty_offending_contra:
       "⟦ F ∈ set_offending_flows G nP; F = {}⟧ ⟹ False"
     by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    lemma offending_notevalD: "F ∈ set_offending_flows G nP ⟹ ¬ sinvar G nP"
     by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    lemma sinvar_no_offending: "sinvar G nP ⟹ set_offending_flows G nP = {}"
      by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    theorem removing_offending_flows_makes_invariant_hold:
      "∀F ∈ set_offending_flows G nP. sinvar (delete_edges G F) nP"
      proof(cases "sinvar G nP")
       case True
        hence no_offending: "set_offending_flows G nP = {}" using sinvar_no_offending by simp
        thus "∀F∈set_offending_flows G nP. sinvar (delete_edges G F) nP" using empty_iff by simp
       next
       case False thus "∀F∈set_offending_flows G nP. sinvar (delete_edges G F) nP"
        by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def graph_ops)
      qed
  corollary valid_without_offending_flows:
  "⟦ F ∈ set_offending_flows G nP ⟧ ⟹ sinvar (delete_edges G F) nP"
    by(simp add: removing_offending_flows_makes_invariant_hold)

  lemma set_offending_flows_simp: 
    "⟦ wf_graph G ⟧ ⟹
      set_offending_flows G nP = {F. F ⊆ edges G ∧
        (¬ sinvar G nP ∧ sinvar ⦇nodes = nodes G, edges = edges G - F⦈ nP) ∧
        (∀(e1, e2)∈F. ¬ sinvar ⦇nodes = nodes G, edges = {(e1, e2)} ∪ (edges G - F)⦈ nP)}"
    apply(simp only: set_offending_flows_def is_offending_flows_min_set_def 
      is_offending_flows_def delete_edges_simp2 add_edge_def graph.select_convs)
    apply(subgoal_tac "⋀F e1 e2. F ⊆ edges G ⟹ (e1, e2) ∈ F ⟹ nodes G ∪ {e1, e2} = nodes G")
     apply fastforce
    apply(simp add: wf_graph_def)
    by (metis fst_conv imageI in_mono insert_absorb snd_conv)

   end



print_locale! SecurityInvariant_withOffendingFlows


text‹
The locale ‹SecurityInvariant_withOffendingFlows› has no assumptions about the security invariant ‹sinvar›.
Undesirable things may happen:
The offending flows can be empty, even for a violated invariant.

We provide an example, the security invariant @{term "(λ_ _. False)"}.
As host attributes, we simply use the identity function @{const id}.
›
lemma "SecurityInvariant_withOffendingFlows.set_offending_flows (λ_ _. False) ⦇ nodes = {''v1''}, edges={} ⦈ id = {}"
by %invisible (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def 
  SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)
lemma "SecurityInvariant_withOffendingFlows.set_offending_flows (λ_ _. False) 
  ⦇ nodes = {''v1'', ''v2''}, edges = {(''v1'', ''v2'')} ⦈ id = {}"
by %invisible (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def 
  SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)

text ‹In general, there exists a @{term sinvar} such that the invariant does not hold and no offending flows exits.›
  lemma "∃sinvar. ¬ sinvar G nP ∧ SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP = {}"
  apply(simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
    SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)
  apply(rule_tac x="(λ_ _. False)" in exI)
  apply(simp)
  done


text‹Thus, we introduce usefulness properties that prohibits such useless invariants.›
text‹We summarize them in an invariant.
It requires the following: 
\begin{enumerate}
  \item The offending flows are always defined.
  \item The invariant is monotonic, i.e. prohibiting more is more secure.
  \item And, the (non-minimal) offending flows are monotonic, i.e. prohibiting more solves more security issues.
\end{enumerate}

Later, we will show that is suffices to show that the invariant is monotonic. The other two properties can be derived.
›

  locale SecurityInvariant_preliminaries = SecurityInvariant_withOffendingFlows sinvar
    for sinvar
    +
    assumes 
      defined_offending:
      "⟦ wf_graph G; ¬ sinvar G nP ⟧ ⟹ set_offending_flows G nP ≠ {}"
    and
      mono_sinvar:
      "⟦ wf_graph ⦇ nodes = N, edges = E ⦈; E' ⊆ E; sinvar ⦇ nodes = N, edges = E ⦈ nP ⟧ ⟹ 
        sinvar ⦇ nodes = N, edges = E' ⦈ nP"
    and mono_offending:
      "⟦ wf_graph G; is_offending_flows ff G nP ⟧ ⟹ is_offending_flows (ff ∪ f') G nP"
  begin

  text ‹
    \begin{small}
    To instantiate a @{const SecurityInvariant_preliminaries}, here are some hints: 
    Have a look at the ‹TopoS_withOffendingFlows.thy› file.
    There is a definition of @{prop sinvar_mono}. It impplies @{prop mono_sinvar} and @{prop mono_offending}
    ‹apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_sinvar_mono[OF sinvar_mono])
    apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])›
  
    In addition, ‹SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono]› gives a nice proof rule for
    @{prop defined_offending}
  
    Basically, ‹sinvar_mono.› implies almost all assumptions here and is equal to @{prop mono_sinvar}.
    \end{small}
›
  end


subsection‹Security Invariants with secure auto-completion of host attribute mappings›

text‹
We will now add a new artifact to the Security Invariant.
It is a secure default host attribute, we will use the symbol ‹⊥›.

The newly introduced Boolean ‹receiver_violation› tells whether a security violation happens at the sender's or the receiver's side.

The details can be looked up in \<^cite>‹"diekmann2014forte"›. 
›

  ― ‹Some notes about the notation:
          @{term "fst ` F"} means to apply the function @{const "fst"} to the set @{term "F"} element-wise.
          Example: If @{term "F"} is a set of directed edges, 
          @{term "F ⊆ edges G"}, then @{term "fst ` F"}
          is the set of senders and @{term "snd ` f"} the set of receivers.›

  locale SecurityInvariant = SecurityInvariant_preliminaries sinvar
    for sinvar::"('v::vertex) graph ⇒ ('v::vertex ⇒ 'a) ⇒ bool"
    +
    fixes default_node_properties :: "'a" ("⊥") 
    and receiver_violation :: "bool"
    assumes 
      ― ‹default value can never fix a security violation.›
      ― ‹Idea: Assume there is a violation, then there is some offending flow. 
        @{text receiver_violation} defines whether the violation happens at the sender's or the receiver's side. 
        We call the place of the violation the \emph{offending host}. 
        We replace the host attribute of the offending host with the default attribute. 
        Giving an offending host, a \emph{secure} default attribute does not change whether the invariant holds.
        I.e.\ this reconfiguration does not remove information, thus preserves all security critical information.
        Thought experiment preliminaries: Can a default configuration ever solve an existing security violation? NO!
        Thought experiment 1: admin forgot to configure host, hence it is handled by default configuration value ...
        Thought experiment 2: new node (attacker) is added to the network. What is its default configuration value ...›
      default_secure:
      "⟦ wf_graph G; ¬ sinvar G nP; F ∈ set_offending_flows G nP ⟧ ⟹
        (¬ receiver_violation ⟶ i ∈ fst ` F ⟶ ¬ sinvar G (nP(i := ⊥))) ∧
        (receiver_violation ⟶ i ∈ snd ` F ⟶ ¬ sinvar G (nP(i := ⊥)))"
      and
      default_unique:
      "otherbot ≠ ⊥ ⟹ 
        ∃ (G::('v::vertex) graph) nP i F. wf_graph G ∧ ¬ sinvar G nP ∧ F ∈ set_offending_flows G nP ∧ 
         sinvar (delete_edges G F) nP ∧
         (¬ receiver_violation ⟶ i ∈ fst ` F ∧ sinvar G (nP(i := otherbot))) ∧
         (receiver_violation ⟶ i ∈ snd ` F ∧ sinvar G (nP(i := otherbot))) "
   begin
    ― ‹Removes option type, replaces with default host attribute›
    fun node_props :: "('v, 'a) TopoS_Params ⇒ ('v ⇒ 'a)" where
    "node_props P = (λ i. (case (node_properties P) i of Some property ⇒ property | None ⇒ ⊥))"

    definition node_props_formaldef :: "('v, 'a) TopoS_Params ⇒ ('v ⇒ 'a)" where
    "node_props_formaldef P ≡
    (λ i. (if i ∈ dom (node_properties P) then the (node_properties P i) else ⊥))"

    lemma node_props_eq_node_props_formaldef: "node_props_formaldef = node_props"
     by(simp add: fun_eq_iff node_props_formaldef_def option.case_eq_if domIff)

    text‹
      Checking whether a security invariant holds.
      \begin{enumerate}
        \item check that the policy @{term G} is syntactically valid
        \item check the security invariant @{term sinvar}
      \end{enumerate}
›
    definition eval::"'v graph ⇒ ('v, 'a) TopoS_Params ⇒ bool" where
    "eval G P ≡ wf_graph G ∧ sinvar G (node_props P)"


    lemma unique_common_math_notation:
    assumes "∀G nP i F. wf_graph (G::('v::vertex) graph) ∧ ¬ sinvar G nP ∧ F ∈ set_offending_flows G nP ∧ 
         sinvar (delete_edges G F) nP ∧ 
         (¬ receiver_violation ⟶ i ∈ fst ` F ⟶ ¬ sinvar G (nP(i := otherbot))) ∧
         (receiver_violation ⟶ i ∈ snd ` F ⟶ ¬ sinvar G (nP(i := otherbot)))"
    shows "otherbot = ⊥"
    apply(rule ccontr)
    apply(drule default_unique)
    using assms by blast
   end

print_locale! SecurityInvariant



subsection‹Information Flow Security and Access Control›
text‹

@{term receiver_violation} defines the offending host. Thus, it defines when the violation happens. 

We found that this coincides with the invariant's security strategy. 

\begin{description}
\item[ACS] If the violation happens at the sender, we have an access control strategy (\emph{ACS}). 
I.e.\ the sender does not have the appropriate rights to initiate the connection.

\item[IFS] If the violation happens at the receiver, we have an information flow security strategy (\emph{IFS})
I.e.\ the receiver lacks the appropriate security level to retrieve the (confidential) information. 
The violations happens only when the receiver reads the data.
\end{description}

We refine our @{term SecurityInvariant} locale.
›

subsection ‹Information Flow Security Strategy (IFS)›
  locale SecurityInvariant_IFS = SecurityInvariant_preliminaries sinvar
      for sinvar::"('v::vertex) graph ⇒ ('v::vertex ⇒ 'a) ⇒ bool"
      +
      fixes default_node_properties :: "'a" ("⊥") 
      assumes  default_secure_IFS:
        "⟦ wf_graph G; f ∈ set_offending_flows G nP ⟧ ⟹
          ∀i ∈ snd` f. ¬ sinvar G (nP(i := ⊥))"
      and
      ― ‹If some otherbot fulfills @{text default_secure}, it must be @{term "⊥"} 
             Hence, @{term "⊥"} is uniquely defined›
      default_unique_IFS:
      "(∀G f nP i. wf_graph G ∧ f ∈ set_offending_flows G nP ∧ i ∈ snd` f 
                ⟶ ¬ sinvar G (nP(i := otherbot))) ⟹ otherbot = ⊥"
      begin
        lemma default_unique_EX_notation: "otherbot ≠ ⊥ ⟹ 
          ∃ G nP i f. wf_graph G ∧ ¬ sinvar G nP ∧ f ∈ set_offending_flows G nP ∧ 
           sinvar (delete_edges G f) nP ∧
           (i ∈ snd` f ∧ sinvar G (nP(i := otherbot)))"
          apply(erule contrapos_pp)
          apply(simp)
          using default_unique_IFS SecurityInvariant_withOffendingFlows.valid_without_offending_flows offending_notevalD
          by metis
      end
  
  sublocale SecurityInvariant_IFS ⊆ SecurityInvariant where receiver_violation=True
  apply(unfold_locales)
   apply(simp add: default_secure_IFS)
  apply(simp only: HOL.simp_thms)
  apply(drule default_unique_EX_notation)
  apply(assumption)
  done

  (*other direction*)
  locale SecurityInvariant_IFS_otherDirectrion = SecurityInvariant where receiver_violation=True
  sublocale SecurityInvariant_IFS_otherDirectrion ⊆ SecurityInvariant_IFS
  apply(unfold_locales)
   apply (metis default_secure offending_notevalD)
  apply(erule contrapos_pp)
  apply(simp)
  apply(drule default_unique)
  apply(simp)
  apply(blast)
  done
  

lemma default_uniqueness_by_counterexample_IFS:
  assumes "(∀G F nP i. wf_graph G ∧ F ∈ SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP ∧ i ∈ snd` F 
                ⟶ ¬ sinvar G (nP(i := otherbot)))"
  and "otherbot ≠ default_value ⟹
    ∃G nP i F. wf_graph G ∧ ¬ sinvar G nP ∧ F ∈ (SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP) ∧
       sinvar (delete_edges G F) nP ∧
        i ∈ snd ` F ∧ sinvar G (nP(i := otherbot)) "
   shows "otherbot = default_value"
   using assms by blast


subsection ‹Access Control Strategy (ACS)›
  locale SecurityInvariant_ACS = SecurityInvariant_preliminaries sinvar
      for sinvar::"('v::vertex) graph ⇒ ('v::vertex ⇒ 'a) ⇒ bool"
      +
      fixes default_node_properties :: "'a" ("⊥") 
      assumes  default_secure_ACS:
        "⟦ wf_graph G; f ∈ set_offending_flows G nP ⟧ ⟹
          ∀i ∈ fst` f. ¬ sinvar G (nP(i := ⊥))"
      and
      default_unique_ACS:
      "(∀G f nP i. wf_graph G ∧ f ∈ set_offending_flows G nP ∧ i ∈ fst` f 
                ⟶ ¬ sinvar G (nP(i := otherbot))) ⟹ otherbot = ⊥"
      begin
        lemma default_unique_EX_notation: "otherbot ≠ ⊥ ⟹ 
          ∃ G nP i f. wf_graph G ∧ ¬ sinvar G nP ∧ f ∈ set_offending_flows G nP ∧ 
           sinvar (delete_edges G f) nP ∧
           (i ∈ fst` f ∧ sinvar G (nP(i := otherbot)))"
          apply(erule contrapos_pp)
          apply(simp)
          using default_unique_ACS SecurityInvariant_withOffendingFlows.valid_without_offending_flows offending_notevalD
          by metis
      end
  
  sublocale SecurityInvariant_ACS ⊆ SecurityInvariant where receiver_violation=False
  apply(unfold_locales)
   apply(simp add: default_secure_ACS)
  apply(simp only: HOL.simp_thms)
  apply(drule default_unique_EX_notation)
  apply(assumption)
  done


  (*other direction*)
  locale SecurityInvariant_ACS_otherDirectrion = SecurityInvariant where receiver_violation=False
  sublocale SecurityInvariant_ACS_otherDirectrion ⊆ SecurityInvariant_ACS
  apply(unfold_locales)
   apply (metis default_secure offending_notevalD)
  apply(erule contrapos_pp)
  apply(simp)
  apply(drule default_unique)
  apply(simp)
  apply(blast)
  done


lemma default_uniqueness_by_counterexample_ACS:
  assumes "(∀G F nP i. wf_graph G ∧ F ∈ SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP ∧ i ∈ fst ` F 
                ⟶ ¬ sinvar G (nP(i := otherbot)))"
  and "otherbot ≠ default_value ⟹
    ∃G nP i F. wf_graph G ∧ ¬ sinvar G nP ∧ F ∈ (SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP) ∧
       sinvar (delete_edges G F) nP ∧
        i ∈ fst ` F ∧ sinvar G (nP(i := otherbot))"
  shows "otherbot = default_value"
  using assms by blast


text‹The sublocale relationships tell that the simplified @{const SecurityInvariant_ACS} and @{const SecurityInvariant_IFS} 
  assumptions suffice to do tho generic SecurityInvariant assumptions.›

end