Theory IDEM

section‹IDEM›
theory IDEM
imports "../../TopoS_Impl"
begin

ML‹
case !Graphviz.open_viewer of
    OpenImmediately => Graphviz.open_viewer := AskTimeouted 3.0
  | AskTimeouted _ => ()
  | DoNothing => ()
›

definition policy :: "string list_graph" where
  "policy ≡ ⦇ nodesL = [''Logger'',
                        ''Sensor_Controller'',
                        ''P4S_in'',
                        ''P4S_filter_A'',
                        ''P4S_filter_B'',
                        ''P4S_filter_C'',
                        ''P4S_aggregator_C'',
                        ''P4S_encrypt_A'',
                        ''P4S_encrypt_B'',
                        ''P4S_encrypt_C'',
                        ''P4S_encrypt_C_low'',
                        ''P4S_out'',
                        ''P4S_DB'',

                        ''Adversary''],
              edgesL = [
              (''Logger'', ''Sensor_Controller''),
              (''Sensor_Controller'', ''P4S_in''),
              (''P4S_in'',       ''P4S_filter_A''),
              (''P4S_in'',       ''P4S_filter_B''),
              (''P4S_in'',       ''P4S_filter_C''),

              (''P4S_filter_A''    , ''P4S_encrypt_A''),
              (''P4S_filter_B''    , ''P4S_encrypt_B''),
              (''P4S_filter_C''    , ''P4S_encrypt_C''),
              (''P4S_filter_C''    , ''P4S_aggregator_C''),
              (''P4S_aggregator_C'', ''P4S_encrypt_C_low''),

              (''P4S_encrypt_A''      , ''P4S_out''),
              (''P4S_encrypt_B''      , ''P4S_out''),
              (''P4S_encrypt_C''      , ''P4S_out''),
              (''P4S_encrypt_C_low''  , ''P4S_out''),

              (''P4S_out'', ''P4S_DB'')
              ] ⦈"

lemma "wf_list_graph policy" by eval

context begin
  definition "tainiting_host_attributes ≡ [
                           ''Logger'' ↦ TaintsUntaints {''A'',''B'',''C'',''D''} {},
                           ''Sensor_Controller'' ↦ TaintsUntaints {''A'',''B'',''C'',''D''} {},
                           ''P4S_in'' ↦ TaintsUntaints {''A'',''B'',''C'',''D''} {},
                           ''P4S_filter_A'' ↦ TaintsUntaints {''A''} {''B'',''C'',''D''},
                           ''P4S_filter_B'' ↦ TaintsUntaints {''B''} {''A'',''C'',''D''},
                           ''P4S_filter_C'' ↦ TaintsUntaints {''C''} {''A'',''B'',''D''},
                           ''P4S_aggregator_C'' ↦ TaintsUntaints {''C_low''} {''C''},
                           ''P4S_encrypt_A'' ↦ TaintsUntaints {} {''A''},
                           ''P4S_encrypt_B'' ↦ TaintsUntaints {} {''B''},
                           ''P4S_encrypt_C'' ↦ TaintsUntaints {} {''C''},
                           ''P4S_encrypt_C_low'' ↦ TaintsUntaints {}{''C_low''}
                           ]"
  private lemma "dom (tainiting_host_attributes) ⊆ set (nodesL policy)"
    by(simp add: tainiting_host_attributes_def policy_def)
  definition "Tainting_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_TaintingTrusted ⦇
        node_properties = tainiting_host_attributes ⦈ ''critical energy data'' "
end

context begin
  private definition "system_EMS ≡
                [(''Logger'',  SystemComponent),
                 (''Sensor_Controller'',  SystemBoundaryOutput)
                 ]"
  private lemma "dom(map_of system_EMS) ⊆ set (nodesL policy)"
    by(simp add: system_EMS_def policy_def)
  definition "system_EMS_m ≡ new_meta_system_boundary system_EMS ''EMS''"
end

context begin
  private definition "system_P4S ≡
                [(''P4S_in'',  SystemBoundaryInput),
                 (''P4S_filter_A'',  SystemComponent),
                 (''P4S_filter_B'',  SystemComponent),
                 (''P4S_filter_C'',  SystemComponent),
                 (''P4S_aggregator_C'',  SystemComponent),
                 (''P4S_encrypt_A'',  SystemComponent),
                 (''P4S_encrypt_B'',  SystemComponent),
                 (''P4S_encrypt_C'',  SystemComponent),
                 (''P4S_encrypt_C_low'',  SystemComponent),
                 (''P4S_out'',  SystemBoundaryOutput)
                 ]"
  private lemma "dom(map_of system_P4S) ⊆ set (nodesL policy)"
    by(simp add: system_P4S_def policy_def)
  definition "system_P4S_m ≡ new_meta_system_boundary system_P4S ''P4S''"
end



context begin
  private definition "system_P4Sstorage ≡
                [(''P4S_DB'',  SystemBoundaryInput)
                 ]"
  private lemma "dom(map_of system_P4Sstorage) ⊆ set (nodesL policy)"
    by(simp add: system_P4Sstorage_def policy_def)
  definition "system_P4Sstorage_m ≡ new_meta_system_boundary system_P4Sstorage ''P4S storage''"
end


definition "invariants ≡ [Tainting_m] @ system_EMS_m @ system_P4S_m @system_P4Sstorage_m"

lemma "all_security_requirements_fulfilled invariants policy" by eval
ML‹
visualize_graph @{context} @{term "invariants"} @{term "policy"};
›


value[code] "implc_get_offending_flows invariants (policy⦇ edgesL := edgesL policy⦈)"
(*ML{*
visualize_graph @{context} @{term "invariants"} @{term "(policy⦇ edgesL := edgesL policy⦈)"};
*}*)
ML‹
visualize_graph_header @{context} @{term "invariants"} @{term "policy"} @{term tainiting_host_attributes};
›


definition make_policy :: "('a SecurityInvariant) list ⇒ 'a list ⇒ 'a list_graph" where
  "make_policy sinvars Vs ≡ generate_valid_topology sinvars ⦇nodesL = Vs, edgesL = List.product Vs Vs ⦈"


value[code] "make_policy invariants (nodesL policy)"

ML_val‹
visualize_edges @{context} @{term "edgesL policy"}
    [("edge [dir=\"arrow\", style=dashed, color=\"#FF8822\", constraint=false]",
     @{term "[(e1, e2) ←  List.product  (nodesL policy) (nodesL policy).
     (e1,e2) ∉ set (edgesL (make_policy invariants (nodesL policy))) ∧ (e2 = ''Adversary'') ∧ (e1 ≠ ''Adversary'')]"})] "";
›


end