Theory Example_Forte14

theory Example_Forte14
imports "../TopoS_Impl"
begin



definition policy :: "string list_graph" where
    "policy ≡ ⦇ nodesL = [''CC'', ''C1'', ''C2'', ''IFEsrv'', ''IFE1'', ''IFE2'', ''SAT'', ''Wifi'', ''P1'', ''P2'' ],
                edgesL = [(''CC'', ''C1''), (''CC'', ''C2''), (''CC'', ''IFEsrv''), (''C1'', ''CC''), 
                          (''C1'', ''C2''), (''C2'', ''CC''), (''C2'', ''C1''), 
                          (''IFEsrv'', ''IFE1''), (''IFEsrv'', ''IFE2''), (''IFEsrv'', ''SAT''), (''IFEsrv'', ''Wifi''),
                          (''IFE1'', ''IFEsrv''), (''IFE2'', ''IFEsrv''), 
                          (''Wifi'', ''IFEsrv''), (''Wifi'', ''SAT''), (''Wifi'', ''P1''),
                          (''Wifi'', ''P2''), (''P1'', ''Wifi''), (''P1'', ''P2''), (''P2'', ''Wifi''), (''P2'', ''P1'')
                          ] ⦈"

lemma "wf_list_graph policy" by eval

(*21 rules*)
lemma "length (edgesL policy) = 21" by eval


definition DomainHierarchy_m::"(string SecurityInvariant)" where
      "DomainHierarchy_m ≡ new_configured_list_SecurityInvariant SINVAR_DomainHierarchyNG_impl.SINVAR_LIB_DomainHierarchyNG ⦇ 
          node_properties = [
            ''CC'' ↦ DN (''aircraft''--''crew''--Leaf, 1),
            ''C1'' ↦ DN (''aircraft''--''crew''--Leaf, 0),
            ''C2'' ↦ DN (''aircraft''--''crew''--Leaf, 0),
            ''IFEsrv'' ↦ DN (''aircraft''--''entertain''--Leaf, 0),
            ''IFE1'' ↦ DN (''aircraft''--''entertain''--Leaf, 0),
            ''IFE2'' ↦ DN (''aircraft''--''entertain''--Leaf, 0),
            ''SAT'' ↦ DN (''aircraft''--''entertain''--''INET''--Leaf, 0),
            ''Wifi'' ↦ DN (''aircraft''--''entertain''--''POD''--Leaf, 1),
            ''P1'' ↦ DN (''aircraft''--''entertain''--''POD''--Leaf, 0),
            ''P2'' ↦ DN (''aircraft''--''entertain''--''POD''--Leaf, 0)
          ]
          ⦈ ''Device Hierarchy''"
  text‹sanity check that the host attributes correspond to the desired hierarchy›
  lemma "DomainHierarchyNG_sanity_check_config
    (map snd [
            (''CC'', DN (''aircraft''--''crew''--Leaf, 1)),
            (''C1'', DN (''aircraft''--''crew''--Leaf, 0)),
            (''C2'', DN (''aircraft''--''crew''--Leaf, 0)),
            (''IFEsrv'', DN (''aircraft''--''entertain''--Leaf, 0)),
            (''IFE1'', DN (''aircraft''--''entertain''--Leaf, 0)),
            (''IFE2'', DN (''aircraft''--''entertain''--Leaf, 0)),
            (''SAT'', DN (''aircraft''--''entertain''--''INET''--Leaf, 0)),
            (''Wifi'', DN (''aircraft''--''entertain''--''POD''--Leaf, 1)),
            (''P1'', DN (''aircraft''--''entertain''--''POD''--Leaf, 0)),
            (''P2'', DN (''aircraft''--''entertain''--''POD''--Leaf, 0))
                            ])
            (
            Department ''aircraft'' [
              Department ''entertain'' [
                Department ''POD'' [], Department ''INET'' []
              ],
              Department ''crew'' []
            ])" by eval

definition PolEnforcePoint_m::"(string SecurityInvariant)" where
  "PolEnforcePoint_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_PolEnforcePointExtended ⦇ 
          node_properties = [''IFEsrv'' ↦ SINVAR_SecGwExt.PolEnforcePointIN,
                             ''IFE1'' ↦ SINVAR_SecGwExt.DomainMember,
                             ''IFE2'' ↦ SINVAR_SecGwExt.DomainMember]
          ⦈ ''IFEsrc mediates access of its thin clients''"


(*
0 - unclassified
1 - confidential
2 - secret
3 - topsecret
*)
definition BLP_m::"(string SecurityInvariant)" where
    "BLP_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_BLPtrusted ⦇ 
          node_properties = [''CC'' ↦ ⦇ security_level = 2, trusted = False ⦈,
                             ''C1'' ↦ ⦇ security_level = 2, trusted = False ⦈,
                             ''C2'' ↦ ⦇ security_level = 2, trusted = False ⦈,
                             ''IFE1'' ↦ ⦇ security_level = 1, trusted = False ⦈,
                             ''IFE2'' ↦ ⦇ security_level = 1, trusted = False ⦈,
                             ''IFEsrv'' ↦ ⦇ security_level = 0, trusted = True ⦈]
          ⦈ ''Confidential data''"

definition "security_invariants = [ DomainHierarchy_m, PolEnforcePoint_m, BLP_m]"

lemma "all_security_requirements_fulfilled security_invariants policy" by eval

lemma "implc_get_offending_flows security_invariants policy = []" by eval


text‹
Visualization with a violation.
›
ML‹
visualize_graph @{context} @{term "security_invariants"} @{term "policy⦇edgesL := (''P1'', ''CC'')#edgesL policy⦈"};
›






definition "max_policy = generate_valid_topology security_invariants ⦇nodesL = nodesL policy, edgesL = List.product (nodesL policy) (nodesL policy) ⦈"


text‹calculating the maximum policy›
value "max_policy"


text‹
The diff to the maximum policy. It adds reflexive flows and the IFEsrv may send to the PODs.
›
ML_val‹
visualize_edges @{context} @{term "edgesL policy"} 
    [("edge [dir=\"arrow\", style=dashed, color=\"#FF8822\", constraint=false]", @{term "[e ← edgesL max_policy. e ∉ set (edgesL policy)]"})] ""; 
›


text‹
Visualizing the maximum policy.
›
ML‹
visualize_graph @{context} @{term "security_invariants"} @{term "max_policy"};
›

lemma "all_security_requirements_fulfilled security_invariants policy" by eval
lemma "all_security_requirements_fulfilled security_invariants max_policy" by eval


subsection‹A stateful implementation›
definition "stateful_policy = generate_valid_stateful_policy_IFSACS policy security_invariants"
value "stateful_policy"

ML_val‹
visualize_edges @{context} @{term "flows_fixL stateful_policy"} 
    [("edge [dir=\"arrow\", style=dashed, color=\"#FF8822\", constraint=false]", @{term "flows_stateL stateful_policy"})] ""; 
›


end