Theory Impl_List_Playground_ChairNetwork_statefulpolicy_example

theory Impl_List_Playground_ChairNetwork_statefulpolicy_example
imports "../TopoS_Impl"
begin


text‹An example of our chair network [simplified]›

text‹Our access control view on the network›
  definition ChairNetwork_empty :: "string list_graph" where
    "ChairNetwork_empty ≡ ⦇ nodesL = [''WebSrv'', ''FilesSrv'', ''Printer'',
                                ''Students'',
                                ''Employees'',
                                ''Internet''],
                      edgesL = [] ⦈"
  
  lemma "wf_list_graph ChairNetwork_empty" by eval


subsection‹Our security requirements›
  subsubsection‹We have a server with confidential data›
    definition ConfidentialChairData::"(string SecurityInvariant)" where
      "ConfidentialChairData ≡ new_configured_list_SecurityInvariant SINVAR_BLPtrusted_impl.SINVAR_LIB_BLPtrusted ⦇ 
          node_properties = [''FilesSrv'' ↦ ⦇ security_level = 1, trusted = False ⦈,
                             ''Employees'' ↦ ⦇ security_level = 0, trusted = True ⦈]
          ⦈ ''confidential data''"


  subsubsection‹accessibly by employees and students›
    definition "PrintingACL ≡ new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''Printer'' ↦ Master [''Employees'', ''Students''],
                             ''Employees'' ↦ Care,
                             ''Students'' ↦ Care]
          ⦈ ''printing acl''"

  subsubsection‹Printers are information sinks›
    definition "PrintingSink ≡ new_configured_list_SecurityInvariant SINVAR_LIB_Sink ⦇ 
          node_properties = [''Printer'' ↦ Sink]
          ⦈ ''printing sink''"



  subsubsection‹Students and Employees may access each other but are not accessible from the outside›
    definition "InternalSubnet ≡ new_configured_list_SecurityInvariant SINVAR_LIB_SubnetsInGW ⦇ 
          node_properties = [''Students'' ↦ Member, ''Employees'' ↦ Member]
          ⦈ ''internal subnet''"


  subsubsection‹The files server is only accessibly by employees›
    definition "FilesSrvACL ≡ new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''FilesSrv'' ↦ Master [''Employees''],
                             ''Employees'' ↦ Care]
          ⦈ ''file srv acl''"


definition "ChairSecurityRequirements = [ConfidentialChairData, PrintingACL, PrintingSink, InternalSubnet, FilesSrvACL]"

lemma "∀m ∈ set ChairSecurityRequirements. implc_sinvar m ChairNetwork_empty" by eval

value "implc_get_offending_flows ChairSecurityRequirements ChairNetwork_empty"
value "generate_valid_topology ChairSecurityRequirements ChairNetwork_empty"

value "List.product (nodesL ChairNetwork_empty) (nodesL ChairNetwork_empty)"

definition "ChairNetwork = generate_valid_topology ChairSecurityRequirements 
      ⦇nodesL = nodesL ChairNetwork_empty, edgesL = List.product (nodesL ChairNetwork_empty) (nodesL ChairNetwork_empty) ⦈"

value "ChairNetwork"


ML‹
visualize_graph @{context} @{term "ChairSecurityRequirements"} @{term "ChairNetwork"};
›


definition "ChairNetwork_stateful_IFS = ⦇ hostsL = nodesL ChairNetwork, flows_fixL = edgesL ChairNetwork, flows_stateL = filter_IFS_no_violations ChairNetwork ChairSecurityRequirements ⦈"
value "edgesL ChairNetwork"
value "filter_IFS_no_violations ChairNetwork ChairSecurityRequirements"
value "ChairNetwork_stateful_IFS"
lemma "set (flows_stateL ChairNetwork_stateful_IFS) ⊆ (set (flows_fixL ChairNetwork_stateful_IFS))" by eval (*must always hold*)
value "(set (flows_fixL ChairNetwork_stateful_IFS)) - set (flows_stateL ChairNetwork_stateful_IFS)"
(*only problems: printers!!!*)
value "stateful_list_policy_to_list_graph ChairNetwork_stateful_IFS"
lemma "set (filter_IFS_no_violations ChairNetwork [ConfidentialChairData]) = set (edgesL ChairNetwork)" by eval

definition "ChairNetwork_stateful_ACS = ⦇ hostsL = nodesL ChairNetwork, flows_fixL = edgesL ChairNetwork, flows_stateL = filter_compliant_stateful_ACS ChairNetwork ChairSecurityRequirements ⦈"
value "edgesL ChairNetwork"
value "filter_compliant_stateful_ACS ChairNetwork ChairSecurityRequirements"
value "ChairNetwork_stateful_ACS"
lemma "set (flows_stateL ChairNetwork_stateful_ACS) ⊆ (set (flows_fixL ChairNetwork_stateful_ACS))"
  by eval (*must always hold*)
value "(set (flows_fixL ChairNetwork_stateful_ACS)) - set (flows_stateL ChairNetwork_stateful_ACS)"

(*flows that are already allowed in both directions are not marked as stateful*)
value "((set (flows_fixL ChairNetwork_stateful_ACS)) - set (flows_stateL ChairNetwork_stateful_ACS)) - set (backlinks (flows_fixL ChairNetwork_stateful_ACS))"

(*the new backflows*)
value "set (edgesL (stateful_list_policy_to_list_graph ChairNetwork_stateful_ACS)) - (set (edgesL ChairNetwork))"

(*the resulting ACS graph*)
value "stateful_list_policy_to_list_graph ChairNetwork_stateful_ACS"


value "generate_valid_stateful_policy_IFSACS ChairNetwork ChairSecurityRequirements"
value "generate_valid_stateful_policy_IFSACS_2 ChairNetwork ChairSecurityRequirements"
lemma "set (flows_fixL (generate_valid_stateful_policy_IFSACS ChairNetwork ChairSecurityRequirements)) =
       set (flows_fixL (generate_valid_stateful_policy_IFSACS_2 ChairNetwork ChairSecurityRequirements))" by eval
lemma "set (flows_stateL (generate_valid_stateful_policy_IFSACS ChairNetwork ChairSecurityRequirements)) =
       set (flows_stateL (generate_valid_stateful_policy_IFSACS_2 ChairNetwork ChairSecurityRequirements))" by eval


definition "ChairNetwork_stateful = generate_valid_stateful_policy_IFSACS ChairNetwork ChairSecurityRequirements"


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

(*these requirements impose no restrictoins on the stateful flows*)
definition "ChairNetwork_stateful_v2 = generate_valid_stateful_policy_IFSACS ChairNetwork
    [ConfidentialChairData, PrintingACL,  InternalSubnet, FilesSrvACL]"
ML_val‹
visualize_edges @{context} @{term "flows_fixL ChairNetwork_stateful_v2"} 
    [("edge [dir=\"arrow\", style=dashed, color=\"#FF8822\", constraint=false]",
     @{term "flows_stateL ChairNetwork_stateful_v2"})] ""; 
›

(*The sink requirements imposes the restriction that the printer cannot answer*)
definition "ChairNetwork_stateful_v3 = generate_valid_stateful_policy_IFSACS ChairNetwork [PrintingSink]"
ML_val‹
visualize_edges @{context} @{term "flows_fixL ChairNetwork_stateful_v3"}
    [("edge [dir=\"arrow\", style=dashed, color=\"#FF8822\", constraint=false]", @{term "flows_stateL ChairNetwork_stateful_v3"})] ""; 
›

subsection‹An example of bad side-effects in access control policies›

  definition ACL_not_with::"(string SecurityInvariant)" where
    "ACL_not_with ≡ new_configured_list_SecurityInvariant SINVAR_ACLnotCommunicateWith_impl.SINVAR_LIB_ACLnotCommunicateWith ⦇ 
        node_properties = [''A'' ↦ {''C''},
                           ''B'' ↦ {},
                           ''C'' ↦ {}]
        ⦈ ''example: a must not reach C''"

  definition simple_network :: "string list_graph" where
    "simple_network ≡ ⦇ nodesL = [''A'', ''B'', ''C''],
                      edgesL = [(''B'', ''A''), (''B'', ''C'')] ⦈"
  
  lemma "wf_list_graph ChairNetwork_empty" by eval
  lemma "∀m ∈ set [ACL_not_with]. implc_sinvar m simple_network" by eval


  lemma "implc_get_offending_flows [ACL_not_with] simple_network = []" by eval
  lemma "implc_get_offending_flows [ACL_not_with] 
    ⦇ nodesL = [''A'', ''B'', ''C''], edgesL = [(''B'', ''A''), (''B'', ''C''), (''A'', ''B'')] ⦈ =
      [[(''B'', ''C'')], [(''A'', ''B'')]]" by eval
  lemma "implc_get_offending_flows [ACL_not_with] 
    ⦇ nodesL = [''A'', ''B'', ''C''], edgesL = [(''B'', ''A''), (''B'', ''C''), (''C'', ''B'')] ⦈ =
      []" by eval

value "generate_valid_stateful_policy_IFSACS simple_network [ACL_not_with]"
value "generate_valid_stateful_policy_IFSACS_2 simple_network [ACL_not_with]"








subsection‹performance test›
(*6 minutes , about 1.8k edges in graph, most of the times, no requirements apply,
  simply added some nodes, edges to the chair network. topology is valid*)
(*value "generate_valid_stateful_policy_IFSACS biggraph ChairSecurityRequirements"*)

end