Theory SINVAR_Examples

theory SINVAR_Examples
imports
  TopoS_Interface
  TopoS_Interface_impl
  TopoS_Library
  TopoS_Composition_Theory
  TopoS_Stateful_Policy
  TopoS_Composition_Theory_impl
  TopoS_Stateful_Policy_Algorithm
  TopoS_Stateful_Policy_impl
  TopoS_Impl
begin


(*Instead of opening a lot of pdfs now, ask whether to open them first.
  If not clicked yes/no, it will wait 3 seconds until it continues.
  Don't change other settings!
  DoNothing must remain DoNothing for batch build.
  Changing this reference will change the behavior of all other theories! Careful with this one ;-)*)
ML‹
case !Graphviz.open_viewer of
    OpenImmediately => Graphviz.open_viewer := AskTimeouted 3.0
  | AskTimeouted _ => ()
  | DoNothing => ()
›

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



context begin
  private definition "SINK_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_Sink ⦇ 
          node_properties = [''Bot1'' ↦ Sink,
                             ''Bot2'' ↦ Sink,
                             ''MissionControl1'' ↦ SinkPool,
                             ''MissionControl2'' ↦ SinkPool
                             ]
          ⦈ ''bots and control are infromation sink''"
  value[code] "make_policy [SINK_m] [''INET'', ''Supervisor'', ''Bot1'', ''Bot2'', ''MissionControl1'', ''MissionControl2'']"
  ML_val‹
  visualize_graph_header @{context} @{term "[SINK_m]"}
    @{term "make_policy [SINK_m] [''INET'', ''Supervisor'', ''Bot1'', ''Bot2'', ''MissionControl1'', ''MissionControl2'']"}
    @{term "[''Bot1'' ↦ Sink,
             ''Bot2'' ↦ Sink,
             ''MissionControl1'' ↦ SinkPool,
             ''MissionControl2'' ↦ SinkPool
             ]"};
›
end






context begin
  private definition "ACL_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''db1'' ↦ Master [''h1'', ''h2''],
                             ''db2'' ↦ Master [''db1''],
                             ''h1'' ↦ Care,
                             ''h2'' ↦ Care
                             ]
          ⦈ ''ACL for databases''" 
  value[code] "make_policy [ACL_m] [''db1'', ''db2'', ''h1'', ''h2'', ''h3'']"
  ML_val‹
  visualize_graph_header @{context} @{term "[ACL_m]"}
    @{term "make_policy [ACL_m] [''db1'', ''db2'', ''h1'', ''h2'', ''h3'']"}
    @{term "[''db1'' ↦ Master [''h1'', ''h2''],
             ''db2'' ↦ Master [''db1''],
             ''h1'' ↦ Care,
             ''h2'' ↦ Care
             ]"};
›
end




definition CommWith_m::"(nat SecurityInvariant)" where
    "CommWith_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_ACLcommunicateWith ⦇ 
          node_properties = [
                  1 ↦ [2,3],
                  2 ↦ [3]]
          ⦈ ''One can only talk to 2,3''"


text‹Experimental: the config (only one) can be added to the end.›
ML_val‹
visualize_graph_header @{context} @{term "[CommWith_m]"}
       @{term "⦇ nodesL = [1::nat, 2, 3],
                edgesL = [(1,2), (2,3)]⦈"} @{term "[
                  (1::nat) ↦ [2::nat,3],
                  2 ↦ [3]]"};
›


value[code] "make_policy [CommWith_m] [1,2,3]"
value[code] "implc_offending_flows CommWith_m ⦇nodesL = [1,2,3,4], edgesL = List.product [1,2,3,4] [1,2,3,4] ⦈"
value[code] "make_policy [CommWith_m] [1,2,3,4]"


ML_val‹
visualize_graph @{context} @{term "[ new_configured_list_SecurityInvariant SINVAR_LIB_ACLcommunicateWith ⦇ 
          node_properties = [
                  1::nat ↦ [1,2,3],
                  2 ↦ [1,2,3,4],
                  3 ↦ [1,2,3,4],
                  4 ↦ [1,2,3,4]]
          ⦈ ''usefull description here'']"} @{term "⦇nodesL = [1::nat,2,3,4], edgesL = [(1,2), (1,3), (2,3), (3, 4)] ⦈"};
›


lemma "implc_offending_flows (new_configured_list_SecurityInvariant SINVAR_LIB_ACLcommunicateWith ⦇ 
          node_properties = [
                  1::nat ↦ [1,2,3],
                  2 ↦ [1,2,3,4],
                  3 ↦ [1,2,3,4],
                  4 ↦ [1,2,3,4]]
          ⦈ ''usefull description here'') ⦇nodesL = [1::nat,2,3,4], edgesL = [(1,2), (1,3), (2,3), (3, 4)] ⦈ =
        [[(1, 2), (1, 3)], [(1, 3), (2, 3)], [(3, 4)]]" by eval



context begin
  private definition G_dep :: "nat list_graph" where
    "G_dep ≡ ⦇nodesL = [1::nat,2,3,4,5,6,7], edgesL = [(1,2), (2,1), (2,3),
                                                       (4,5), (5,6), (6,7)] ⦈"
  private lemma "wf_list_graph G_dep" by eval

  private definition "DEP_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_Dependability ⦇ 
          node_properties = Some ∘ dependability_fix_nP G_dep (λ_. 0)
          ⦈ ''automatically computed dependability invariant''"
  ML_val‹
  visualize_graph_header @{context} @{term "[DEP_m]"}
    @{term "G_dep"}
    @{term "Some ∘ dependability_fix_nP G_dep (λ_. 0)"};
›

  text‹Connecting @{term "(3,4)"}. This causes only one offedning flow at @{term "(3,4)"}.›
  ML_val‹
  visualize_graph_header @{context} @{term "[DEP_m]"}
    @{term "G_dep⦇edgesL := (3,4)#edgesL G_dep⦈"}
    @{term "Some ∘ dependability_fix_nP G_dep (λ_. 0)"};
›
  text‹We try to increase the dependability level at @{term 3}. Suddenly, offending flows everywhere.›
  ML_val‹
  visualize_graph_header @{context} @{term "[new_configured_list_SecurityInvariant SINVAR_LIB_Dependability ⦇ 
          node_properties = Some ∘ ((dependability_fix_nP G_dep (λ_. 0))(3 := 2))
          ⦈ ''changed deps'']"}
    @{term "G_dep⦇edgesL := (3,4)#edgesL G_dep⦈"}
    @{term "Some ∘ ((dependability_fix_nP G_dep (λ_. 0))(3 := 2))"};
›
  lemma "implc_offending_flows (new_configured_list_SecurityInvariant SINVAR_LIB_Dependability ⦇ 
                          node_properties = Some ∘ ((dependability_fix_nP G_dep (λ_. 0))(3 := 2))
                          ⦈ ''changed deps'')
             (G_dep⦇edgesL := (3,4)#edgesL G_dep⦈) = 
           [[(3, 4)], [(1, 2), (2, 1), (5, 6)], [(1, 2), (4, 5)], [(2, 1), (4, 5)], [(2, 3), (4, 5)], [(2, 3), (5, 6)]]"
           by eval

  text‹If we recompute the dependability levels for the changed graph, we see that suddenly, 
        The level at @{term 1} and @{term 2} increased, though we only added the edge @{term "(3,4)"}.
        This hints that we connected the graph. If an attacker can now compromise @{term 1}, she 
        may be able to peek much deeper into the network.›
  ML_val‹
  visualize_graph_header @{context} @{term "[new_configured_list_SecurityInvariant SINVAR_LIB_Dependability ⦇ 
          node_properties = Some ∘ dependability_fix_nP (G_dep⦇edgesL := (3,4)#edgesL G_dep⦈) (λ_. 0)
          ⦈ ''changed deps'']"}
    @{term "G_dep⦇edgesL := (3,4)#edgesL G_dep⦈"}
    @{term "Some ∘ dependability_fix_nP (G_dep⦇edgesL := (3,4)#edgesL G_dep⦈) (λ_. 0)"};
›

  text‹Dependability is reflexive, a host can depend on itself.›
  ML_val‹
  visualize_graph_header @{context} @{term "[new_configured_list_SecurityInvariant SINVAR_LIB_Dependability ⦇ 
          node_properties = Some ∘ dependability_fix_nP ⦇nodesL = [1::nat], edgesL = [(1,1)] ⦈ (λ_. 0)
          ⦈ ''changed deps'']"}
    @{term "⦇nodesL = [1::nat], edgesL = [(1,1)] ⦈"}
    @{term "Some ∘ dependability_fix_nP ⦇nodesL = [1::nat], edgesL = [(1,1)] ⦈ (λ_. 0)"};
›
  ML_val‹
  visualize_graph_header @{context} @{term "[new_configured_list_SecurityInvariant SINVAR_LIB_Dependability_norefl ⦇ 
          node_properties = (λ_::nat. Some 0)
          ⦈ ''changed deps'']"}
    @{term "⦇nodesL = [1::nat], edgesL = [(1,1)] ⦈"}
    @{term "(λ_::nat. Some (0::nat))"};
›

end



context begin
  private definition G_noninter :: "nat list_graph" where
    "G_noninter ≡ ⦇nodesL = [1::nat,2,3,4], edgesL = [(1,2), (1,3), (2,3), (3, 4)] ⦈"
  private lemma "wf_list_graph G_noninter" by eval

  private definition "NonI_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_NonInterference ⦇ 
          node_properties = [
                  1::nat ↦ Interfering,
                  2 ↦ Unrelated, 
                  3 ↦ Unrelated, 
                  4 ↦ Interfering]
          ⦈ ''One and Four interfere''"
  ML_val‹
  visualize_graph @{context} @{term "[ NonI_m ]"} @{term "G_noninter"};
›

  (*The same as the CommWith example*)
  lemma "implc_offending_flows NonI_m G_noninter = [[(1, 2), (1, 3)], [(1, 3), (2, 3)], [(3, 4)]]"
           by eval


  ML_val‹
  visualize_graph @{context} @{term "[ NonI_m ]"} @{term "⦇nodesL = [1::nat,2,3,4], edgesL = [(1,2), (1,3), (2,3), (4, 3)] ⦈"};
›

  lemma "implc_offending_flows NonI_m ⦇nodesL = [1::nat,2,3,4], edgesL = [(1,2), (1,3), (2,3), (4, 3)] ⦈ =
    [[(1, 2), (1, 3)], [(1, 3), (2, 3)], [(4, 3)]]"
           by eval

  text‹In comparison, @{const SINVAR_LIB_ACLcommunicateWith} is less strict. 
        Changing the direction of the edge @{term "(3,4)"} removes the access from @{term 1} to @{term 4}
        and the invariant holds.›
  lemma "implc_offending_flows (new_configured_list_SecurityInvariant SINVAR_LIB_ACLcommunicateWith ⦇ 
          node_properties = [
                  1::nat ↦ [1,2,3],
                  2 ↦ [1,2,3,4],
                  3 ↦ [1,2,3,4],
                  4 ↦ [1,2,3,4]]
          ⦈ ''One must not access Four'') ⦇nodesL = [1::nat,2,3,4], edgesL = [(1,2), (1,3), (2,3), (4, 3)] ⦈ = []" by eval
end



context begin
  private definition "subnets_host_attributes ≡ [
                             ''v11'' ↦ Subnet 1,
                             ''v12'' ↦ Subnet 1,
                             ''v13'' ↦ Subnet 1,
                             ''v1b'' ↦ BorderRouter 1,
                             ''v21'' ↦ Subnet 2,
                             ''v22'' ↦ Subnet 2,
                             ''v23'' ↦ Subnet 2,
                             ''v2b'' ↦ BorderRouter 2,
                             ''v3b'' ↦ BorderRouter 3
                             ]"
  private definition "Subnets_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_Subnets ⦇ 
          node_properties = subnets_host_attributes
          ⦈ ''Collaborating hosts''"
  private definition "subnet_hosts ≡ [''v11'', ''v12'', ''v13'', ''v1b'',
                                      ''v21'', ''v22'', ''v23'', ''v2b'',
                                      ''v3b'', ''vo'']"

  private lemma "dom (subnets_host_attributes) ⊆ set (subnet_hosts)"
    by(simp add: subnet_hosts_def subnets_host_attributes_def)
  value[code] "make_policy [Subnets_m] subnet_hosts"
  ML_val‹
  visualize_graph_header @{context} @{term "[Subnets_m]"}
    @{term "make_policy [Subnets_m] subnet_hosts"}
    @{term "subnets_host_attributes"};
›


  text‹Emulating the same but with accessible members with SubnetsInGW and ACLs›
  private definition "SubnetsInGW_ACL_ms ≡ [new_configured_list_SecurityInvariant SINVAR_LIB_SubnetsInGW ⦇ 
          node_properties = [''v11'' ↦ Member, ''v12'' ↦ Member, ''v13'' ↦ Member, ''v1b'' ↦ InboundGateway]
          ⦈ ''v1 subnet'',
          new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''v1b'' ↦ Master [''v11'', ''v12'', ''v13'', ''v2b'', ''v3b''],
                             ''v11'' ↦ Care,
                             ''v12'' ↦ Care,
                             ''v13'' ↦ Care,
                             ''v2b'' ↦ Care,
                             ''v3b'' ↦ Care
                             ]
          ⦈ ''v1b ACL'',
          new_configured_list_SecurityInvariant SINVAR_LIB_SubnetsInGW ⦇ 
          node_properties = [''v21'' ↦ Member, ''v22'' ↦ Member, ''v23'' ↦ Member, ''v2b'' ↦ InboundGateway]
          ⦈ ''v2 subnet'',
          new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''v2b'' ↦ Master [''v21'', ''v22'', ''v23'', ''v1b'', ''v3b''],
                             ''v21'' ↦ Care,
                             ''v22'' ↦ Care,
                             ''v23'' ↦ Care,
                             ''v1b'' ↦ Care,
                             ''v3b'' ↦ Care
                             ]
          ⦈ ''v2b ACL'',
          ⌦‹new_configured_list_SecurityInvariant SINVAR_LIB_SubnetsInGW ⦇ 
          node_properties = [''v3b'' ↦ InboundGateway]
          ⦈ ''v3b'',›
          new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''v3b'' ↦ Master [''v1b'', ''v2b''],
                             ''v1b'' ↦ Care,
                             ''v2b'' ↦ Care
                             ]
          ⦈ ''v3b ACL'']"
  value[code] "make_policy SubnetsInGW_ACL_ms subnet_hosts"
  lemma "set (edgesL (make_policy [Subnets_m] subnet_hosts)) ⊆ set (edgesL (make_policy SubnetsInGW_ACL_ms subnet_hosts))" by eval
  lemma "[e <- edgesL (make_policy SubnetsInGW_ACL_ms subnet_hosts). e ∉ set (edgesL (make_policy [Subnets_m] subnet_hosts))] =
   [(''v1b'', ''v11''), (''v1b'', ''v12''), (''v1b'', ''v13''), (''v2b'', ''v21''), (''v2b'', ''v22''), (''v2b'', ''v23'')]" by eval
  ML_val‹
  visualize_graph @{context} @{term "SubnetsInGW_ACL_ms"}
    @{term "make_policy SubnetsInGW_ACL_ms subnet_hosts"};
›
end




context begin
  private definition "secgwext_host_attributes ≡ [
                             ''hypervisor'' ↦ PolEnforcePoint,
                             ''securevm1'' ↦ DomainMember,
                             ''securevm2'' ↦ DomainMember,
                             ''publicvm1'' ↦ AccessibleMember,
                             ''publicvm2'' ↦ AccessibleMember
                             ]"
  private definition "SecGwExt_m ≡ new_configured_list_SecurityInvariant SINVAR_LIB_PolEnforcePointExtended ⦇ 
          node_properties = secgwext_host_attributes
          ⦈ ''secure hypervisor mediates accesses between secure VMs''"
  private definition "secgwext_hosts ≡ [''hypervisor'', ''securevm1'', ''securevm2'',
                                      ''publicvm1'', ''publicvm2'',
                                      ''INET'']"

  private lemma "dom (secgwext_host_attributes) ⊆ set (secgwext_hosts)"
    by(simp add: secgwext_hosts_def secgwext_host_attributes_def)
  value[code] "make_policy [SecGwExt_m] secgwext_hosts"
  ML_val‹
  visualize_graph_header @{context} @{term "[SecGwExt_m]"}
    @{term "make_policy [SecGwExt_m] secgwext_hosts"}
    @{term "secgwext_host_attributes"};
›

  ML_val‹
  visualize_graph_header @{context} @{term "[SecGwExt_m, new_configured_list_SecurityInvariant SINVAR_LIB_BLPtrusted ⦇ 
        node_properties = [''hypervisor'' ↦ ⦇ security_level = 0, trusted = True ⦈,
                           ''securevm1'' ↦ ⦇ security_level = 1, trusted = False ⦈,
                           ''securevm2'' ↦ ⦇ security_level = 1, trusted = False ⦈
                           ] ⦈ ''secure vms are confidential'']"}
    @{term "make_policy [SecGwExt_m, new_configured_list_SecurityInvariant SINVAR_LIB_BLPtrusted ⦇ 
        node_properties = [''hypervisor'' ↦ ⦇ security_level = 0, trusted = True ⦈,
                           ''securevm1'' ↦ ⦇ security_level = 1, trusted = False ⦈,
                           ''securevm2'' ↦ ⦇ security_level = 1, trusted = False ⦈
                           ] ⦈ ''secure vms are confidential''] secgwext_hosts"}
    @{term "secgwext_host_attributes"};
›
end


end