Theory CryptoDB

section‹CryptoDB›
theory CryptoDB
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 = [
                        ''A'', ''A_encrypter'', ''A_channel'',
                        ''B'', ''B_encrypter'', ''B_channel'',
                        ''C'', ''C_encrypter'', ''C_channel_in'', ''C_channel_out'', ''C_decrypter'',
                        ''Adversary'',
                        ''CryptoDB''],
              edgesL = [
              (''A'', ''A_encrypter''), (''A_encrypter'', ''A_channel''), (''A_channel'', ''CryptoDB''),
              (''B'', ''B_encrypter''), (''B_encrypter'', ''B_channel''), (''B_channel'', ''CryptoDB''),
              (''C'', ''C_encrypter''), (''C_encrypter'', ''C_channel_out''), (''C_channel_out'', ''CryptoDB''),
              (''CryptoDB'', ''C_channel_in''), (''C_channel_in'', ''C_decrypter''), (''C_decrypter'', ''C'')
              ] ⦈"

context begin
  private definition "tainiting_host_attributes ≡ [
                           ''A'' ↦ TaintsUntaints {''A''} {},
                           ''A_encrypter'' ↦ TaintsUntaints {} {''A''},
                           ''A_channel'' ↦ TaintsUntaints {} {},
                           ''B'' ↦ TaintsUntaints {''B''} {},
                           ''B_encrypter'' ↦ TaintsUntaints {} {''B''},
                           ''B_channel'' ↦ TaintsUntaints {} {},
                           ''C'' ↦ TaintsUntaints {''C''} {},
                           ''C_encrypter'' ↦ TaintsUntaints {} {''C''},
                           ''C_decrypter'' ↦ TaintsUntaints {''C''} {},
                           ''C_channel_out'' ↦ TaintsUntaints {} {},
                           ''C_channel_in'' ↦ TaintsUntaints {} {},
                           ''Adversary'' ↦ TaintsUntaints {} {}
                           ]"
  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 ⦈ ''user-data''"
end
lemma "wf_list_graph policy" by eval

ML_val‹
visualize_graph @{context} @{term "[]::string SecurityInvariant list"} @{term "policy"};
›


context begin
  private definition "A_host_attributes ≡
                [''A'' ↦ Member,
                 ''A_encrypter'' ↦ Member,
                 ''A_channel'' ↦ Member
                 ]"
  private lemma "dom A_host_attributes ⊆ set (nodesL policy)"
    by(simp add: A_host_attributes_def policy_def)
  definition "SystemA_m ≡ new_configured_list_SecurityInvariant
                                  SINVAR_LIB_SubnetsInGW
                                    ⦇ node_properties = A_host_attributes ⦈ ''sys-A''"
end

context begin
  private definition "B_host_attributes ≡
                [''B'' ↦ Member,
                 ''B_encrypter'' ↦ Member,
                 ''B_channel'' ↦ Member
                 ]"
  private lemma "dom B_host_attributes ⊆ set (nodesL policy)"
    by(simp add: B_host_attributes_def policy_def)
  definition "SystemB_m ≡ new_configured_list_SecurityInvariant
                                  SINVAR_LIB_SubnetsInGW
                                    ⦇ node_properties = B_host_attributes ⦈ ''sys-B''"
end



context begin
  private definition "C_host_attributes ≡
                [(''C_channel_in'', SystemBoundaryInput),
                 (''C_decrypter'', SystemComponent),
                 (''C'', SystemComponent),
                 (''C_encrypter'', SystemComponent),
                 (''C_channel_out'', SystemBoundaryOutput)
                 ]"
  private lemma "dom (map_of C_host_attributes) ⊆ set (nodesL policy)"
    by(simp add: C_host_attributes_def policy_def)
  definition "SystemC_m ≡ new_meta_system_boundary C_host_attributes ''sys-C''"
end

definition "invariants ≡ [Tainting_m, SystemA_m, SystemB_m] @ SystemC_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⦈)"};
›


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)"

text‹visualizing all flows which may not end at the adversary. I.e. things which are prohibited.›
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 policy)) ∧ ((e1,e2) ∉ set (edgesL (make_policy invariants (nodesL policy)))) ∧ (e2 = ''Adversary'') ∧ (e1 ≠ ''Adversary'')]"})] "";
›


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


end