Theory SINVAR_DomainHierarchyNG_impl

theory SINVAR_DomainHierarchyNG_impl
imports SINVAR_DomainHierarchyNG "../TopoS_Interface_impl"
begin


subsubsection ‹SecurityInvariant DomainHierarchy List Implementation›

code_identifier code_module SINVAR_DomainHierarchyNG_impl => (Scala) SINVAR_DomainHierarchyNG

fun sinvar :: "'v list_graph ⇒ ('v ⇒ domainNameTrust) ⇒ bool" where
  "sinvar G nP = (∀ (s, r) ∈ set (edgesL G). (nP r) ⊑⇩t⇩r⇩u⇩s⇩t (nP s))"


definition DomainHierarchyNG_sanity_check_config :: "domainNameTrust list ⇒ domainTree ⇒ bool" where
  "DomainHierarchyNG_sanity_check_config host_attributes tree = (∀ c ∈ set host_attributes.
    case c of Unassigned ⇒ True
            | DN (level, trust) ⇒ valid_hierarchy_pos tree level
   )"

fun verify_globals :: "'v list_graph ⇒ ('v ⇒ domainNameTrust) ⇒ domainTree ⇒ bool" where
  "verify_globals G nP tree = (∀ v ∈ set (nodesL G). 
    case (nP v) of Unassigned ⇒ True | DN (level, trust) ⇒ valid_hierarchy_pos tree level
   )"

(*TODO: to get rid of verify_globals
  this stronger DomainHierarchyNG_sanity_check_config sanity checker checks the config
  for all graphs!*)
lemma "DomainHierarchyNG_sanity_check_config c tree ⟹
    {x. ∃v. nP v = x} = set c ⟹
    verify_globals G nP tree"
  apply(simp add: DomainHierarchyNG_sanity_check_config_def split: if_split_asm)
  apply(clarify)
  apply(case_tac "nP v")
   apply(simp_all)
  apply(clarify)
  by force


definition DomainHierarchyNG_offending_list:: "'v list_graph ⇒ ('v ⇒ domainNameTrust) ⇒ ('v × 'v) list list" where
  "DomainHierarchyNG_offending_list G nP = (if sinvar G nP then
    []
   else 
    [ [e ← edgesL G. case e of (s,r) ⇒ ¬ (nP r) ⊑⇩t⇩r⇩u⇩s⇩t (nP s) ] ])"



lemma "DomainHierarchyNG.node_props P = 
  (λi. case node_properties P i of None ⇒ SINVAR_DomainHierarchyNG.default_node_properties | Some property ⇒ property)"
by(fact SecurityInvariant.node_props.simps[OF TopoS_DomainHierarchyNG, of "P"])

definition "NetModel_node_props P = (λ i. (case (node_properties P) i of Some property ⇒ property | None ⇒ SINVAR_DomainHierarchyNG.default_node_properties))"
(*lemma[code_unfold]: "SecurityInvariant.node_props SINVAR_DomainHierarchy.default_node_properties P = NetModel_node_props P"
apply(simp add: NetModel_node_props_def)
done*)

(*TODO does this work?*)
lemma[code_unfold]: "DomainHierarchyNG.node_props P = NetModel_node_props P"
by(simp add: NetModel_node_props_def)

definition "DomainHierarchyNG_eval G P = (wf_list_graph G ∧
  sinvar G (SecurityInvariant.node_props SINVAR_DomainHierarchyNG.default_node_properties P))"


interpretation DomainHierarchyNG_impl:TopoS_List_Impl 
  where default_node_properties=SINVAR_DomainHierarchyNG.default_node_properties
  and sinvar_spec=SINVAR_DomainHierarchyNG.sinvar
  and sinvar_impl=sinvar
  and receiver_violation=SINVAR_DomainHierarchyNG.receiver_violation
  and offending_flows_impl=DomainHierarchyNG_offending_list
  and node_props_impl=NetModel_node_props
  and eval_impl=DomainHierarchyNG_eval
 apply(unfold TopoS_List_Impl_def)
 apply(rule conjI)
  apply(simp add: TopoS_DomainHierarchyNG list_graph_to_graph_def; fail)
 apply(rule conjI)
  apply(simp add: list_graph_to_graph_def DomainHierarchyNG_offending_set
        DomainHierarchyNG_offending_set_def DomainHierarchyNG_offending_list_def; fail)
 apply(rule conjI)
  apply(simp only: NetModel_node_props_def)
  apply(metis DomainHierarchyNG.node_props.simps DomainHierarchyNG.node_props_eq_node_props_formaldef)
 apply(simp only: DomainHierarchyNG_eval_def)
 apply(intro allI)
 apply(rule TopoS_eval_impl_proofrule[OF TopoS_DomainHierarchyNG])
 apply(simp add: list_graph_to_graph_def)
done


subsubsection ‹DomainHierarchyNG packing›
  definition SINVAR_LIB_DomainHierarchyNG :: "('v::vertex, domainNameTrust) TopoS_packed" where
    "SINVAR_LIB_DomainHierarchyNG ≡ 
    ⦇ nm_name = ''DomainHierarchyNG'', 
      nm_receiver_violation = SINVAR_DomainHierarchyNG.receiver_violation,
      nm_default = SINVAR_DomainHierarchyNG.default_node_properties, 
      nm_sinvar = sinvar,
      nm_offending_flows = DomainHierarchyNG_offending_list, 
      nm_node_props = NetModel_node_props,
      nm_eval = DomainHierarchyNG_eval
      ⦈"
  interpretation SINVAR_LIB_DomainHierarchyNG_interpretation: TopoS_modelLibrary SINVAR_LIB_DomainHierarchyNG 
      SINVAR_DomainHierarchyNG.sinvar
    apply(unfold TopoS_modelLibrary_def SINVAR_LIB_DomainHierarchyNG_def)
    apply(rule conjI)
     apply(simp)
    apply(simp)
    by(unfold_locales)






text ‹Examples:›
definition example_TUM_net :: "string list_graph" where
  "example_TUM_net ≡ ⦇ nodesL=[''Gateway'', ''LowerSVR'', ''UpperSRV''], 
        edgesL=[
          (''Gateway'',''LowerSVR''), (''Gateway'',''UpperSRV''), 
          (''LowerSVR'', ''Gateway''),
          (''UpperSRV'', ''Gateway'')
        ] ⦈"
value "wf_list_graph example_TUM_net"

definition example_TUM_config :: "string ⇒ domainNameTrust" where
  "example_TUM_config ≡ ((λ e. default_node_properties)
        (''Gateway'':= DN (''ACD''--''AISD''--Leaf, 1),
         ''LowerSVR'':= DN (''ACD''--''AISD''--Leaf, 0),
         ''UpperSRV'':= DN (''ACD''--Leaf, 0)
       ))"

definition example_TUM_hierarchy :: "domainTree" where
"example_TUM_hierarchy ≡ (Department ''ACD'' [
           Department ''AISD'' []
       ])"

value "verify_globals example_TUM_net example_TUM_config example_TUM_hierarchy"
value "sinvar     example_TUM_net example_TUM_config"

definition example_TUM_net_invalid where
"example_TUM_net_invalid ≡ example_TUM_net⦇edgesL :=  
    (''LowerSRV'', ''UpperSRV'')#(edgesL example_TUM_net)⦈"

value "verify_globals example_TUM_net_invalid example_TUM_config example_TUM_hierarchy"
value "sinvar     example_TUM_net_invalid example_TUM_config"
value "DomainHierarchyNG_offending_list example_TUM_net_invalid example_TUM_config"


hide_const (open) NetModel_node_props

hide_const (open) sinvar 

end