Theory Semantics_Stateful

theory Semantics_Stateful
imports Semantics
begin

section‹Semantics Stateful›

subsection‹Model 1 -- Curried Stateful Matcher›

text‹Processing a packet with state can be modeled as follows:
  The state is @{term σ}.
  The primitive matcher @{term γ⇩σ} is a curried function where the first argument is the state and
  it returns a stateless primitive matcher, i.e. @{term "γ = (γ⇩σ σ)"}.
  With this stateless primitive matcher @{term γ}, the @{const iptables_bigstep} semantics are executed.
  As entry point, the iptables built-in chains @{term "''INPUT''"}, @{term "''OUTPUT''"}, and @{term "''FORWARD''"} with their
  default-policy (@{const Accept} or @{const Drop} are valid for iptables) are chosen.
  The semantics must yield a @{term "Decision X"}.
  Due to the default-policy, this is always the case if the ruleset is well-formed.
  When a decision is made, the state @{term σ} is updated.›

inductive semantics_stateful ::
  "'a ruleset ⇒
   ('σ ⇒ ('a, 'p) matcher) ⇒ ― ‹matcher, first parameter is the state›
   ('σ ⇒ final_decision ⇒ 'p ⇒ 'σ) ⇒ ― ‹state update function after firewall has decision for a packet›
   'σ ⇒ ― ‹Starting state. constant›
   (string × action) ⇒ ― ‹The chain and default policy the firewall evaluates. For example ''FORWARD'', Drop›
   'p list ⇒ ― ‹packets to be processed›
   ('p × final_decision) list ⇒ ― ‹packets which have been processed and their decision. ordered the same as the firewall processed them. oldest packet first›
   'σ ⇒ ― ‹final state›
   bool" for Γ and γ⇩σ and state_update and σ⇩0 where
  ― ‹A list of packets @{term ps} waiting to be processed. Nothing has happened, start and final state are the same, the list of processed packets is empty.›
  "semantics_stateful Γ γ⇩σ state_update σ⇩0 (built_in_chain, default_policy) ps [] σ⇩0" |

  ― ‹Processing one packet›
  "semantics_stateful Γ γ⇩σ state_update σ⇩0 (built_in_chain, default_policy) (p#ps) ps_processed σ' ⟹
   Γ,(γ⇩σ σ'),p⊢ ⟨[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy],Undecided⟩ ⇒ Decision X ⟹
    semantics_stateful Γ γ⇩σ state_update σ⇩0 (built_in_chain, default_policy) ps (ps_processed@[(p, X)]) (state_update σ' X p)"


lemma semantics_stateful_intro_process_one: "semantics_stateful Γ γ⇩σ state_upate σ⇩0 (built_in_chain, default_policy) (p#ps) ps_processed_old σ_old ⟹
       Γ,γ⇩σ σ_old,p⊢ ⟨[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy], Undecided⟩ ⇒ Decision X ⟹
       σ' = state_upate σ_old X p ⟹
       ps_processed = ps_processed_old@[(p, X)] ⟹
       semantics_stateful Γ γ⇩σ state_upate σ⇩0 (built_in_chain, default_policy) ps ps_processed σ'"
  by(auto intro: semantics_stateful.intros)

lemma semantics_stateful_intro_start: "σ⇩0 = σ' ⟹ ps_processed = [] ⟹
       semantics_stateful Γ γ⇩σ state_upate σ⇩0 (built_in_chain, default_policy) ps ps_processed σ'"
  by(auto intro: semantics_stateful.intros)


text‹Example below›

subsection‹Model 2 -- Packets Tagged with State Information›

text‹In this model, the matcher is completely stateless but packets are previously tagged with
      (static) stateful information.›

inductive semantics_stateful_packet_tagging ::
   "'a ruleset ⇒
    ('a, 'ptagged) matcher ⇒
    ('σ ⇒ 'p ⇒ 'ptagged) ⇒ ― ‹taggs the packet accordig to the current state before processing by firewall›
    ('σ ⇒ final_decision ⇒ 'p ⇒ 'σ) ⇒ ― ‹state updater›
    'σ ⇒ ― ‹Starting state. constant›
    (string × action) ⇒
    'p list ⇒ ― ‹packets to be processed›
    ('p × final_decision) list ⇒ ― ‹packets which have been processed›
    'σ ⇒ ― ‹final state›
    bool" for Γ and γ and packet_tagger and state_update and σ⇩0 where
  "semantics_stateful_packet_tagging Γ γ packet_tagger state_update σ⇩0 (built_in_chain, default_policy) ps [] σ⇩0" |

  "semantics_stateful_packet_tagging Γ γ packet_tagger state_update σ⇩0 (built_in_chain, default_policy) (p#ps) ps_processed σ' ⟹
   Γ,γ,(packet_tagger σ' p)⊢ ⟨[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy],Undecided⟩ ⇒ Decision X ⟹
    semantics_stateful_packet_tagging Γ γ packet_tagger state_update σ⇩0 (built_in_chain, default_policy) ps (ps_processed@[(p, X)]) (state_update σ' X p)"


lemma semantics_stateful_packet_tagging_intro_start: "σ⇩0 = σ' ⟹ ps_processed = [] ⟹
       semantics_stateful_packet_tagging Γ γ packet_tagger state_upate σ⇩0 (built_in_chain, default_policy) ps ps_processed σ'"
  by(auto intro: semantics_stateful_packet_tagging.intros)

lemma semantics_stateful_packet_tagging_intro_process_one:
      "semantics_stateful_packet_tagging Γ γ packet_tagger state_upate σ⇩0 (built_in_chain, default_policy) (p#ps) ps_processed_old σ_old ⟹
       Γ,γ,(packet_tagger σ_old p)⊢ ⟨[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy], Undecided⟩ ⇒ Decision X ⟹
       σ' = state_upate σ_old X p ⟹
       ps_processed = ps_processed_old@[(p, X)] ⟹
       semantics_stateful_packet_tagging Γ γ packet_tagger state_upate σ⇩0 (built_in_chain, default_policy) ps ps_processed σ'"
  by(auto intro: semantics_stateful_packet_tagging.intros)


lemma semantics_bigstep_state_vs_tagged: 
  assumes "∀m::'m. stateful_matcher' σ m p = stateful_matcher_tagged' m (packet_tagger' σ p)" 
  shows "Γ,stateful_matcher' σ,p⊢ ⟨rs, Undecided⟩ ⇒ t ⟷
         Γ,stateful_matcher_tagged',packet_tagger' σ p⊢ ⟨rs, Undecided⟩ ⇒ t"
proof -
  { fix m::"'m match_expr"
   from assms have
    "matches (stateful_matcher' σ) m p ⟷ matches stateful_matcher_tagged' m (packet_tagger' σ p)"
      by(induction m) (simp_all)
  } note matches_stateful_matcher_stateful_matcher_tagged=this

  show ?thesis (is "?lhs ⟷ ?rhs")
  proof
    assume ?lhs
    thus ?rhs
     proof(induction rs Undecided t rule: iptables_bigstep_induct)
     case (Seq _ _ _ t)
       thus ?case
         apply(cases t)
          apply (simp add: seq)
         apply(auto simp add: decision seq dest: decisionD)
         done
     qed(auto intro: iptables_bigstep.intros simp add: matches_stateful_matcher_stateful_matcher_tagged)
  next
    assume ?rhs
    thus ?lhs
     proof(induction rs Undecided t rule: iptables_bigstep_induct)
     case (Seq _ _ _ t)
       thus ?case
         apply(cases t)
          apply (simp add: seq)
         apply(auto  simp add: decision seq dest: decisionD)
         done
     qed(auto intro: iptables_bigstep.intros simp add: matches_stateful_matcher_stateful_matcher_tagged)
  qed
qed
   


text‹Both semantics are equal›
theorem semantics_stateful_vs_tagged:
  assumes "∀m σ p. stateful_matcher' σ m p = stateful_matcher_tagged' m (packet_tagger' σ p)" 
  shows "semantics_stateful rs stateful_matcher' state_update' σ⇩0 start ps ps_processed σ' =
       semantics_stateful_packet_tagging rs stateful_matcher_tagged' packet_tagger' state_update' σ⇩0 start ps ps_processed σ'"
  proof -
   from semantics_bigstep_state_vs_tagged[of stateful_matcher' _ _ stateful_matcher_tagged' packet_tagger'] assms
     have vs_tagged:
     "rs,stateful_matcher' σ',p⊢ ⟨[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy], Undecided⟩ ⇒ t ⟷
      rs,stateful_matcher_tagged',packet_tagger' σ' p⊢ ⟨[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy], Undecided⟩ ⇒ t"
      for t p σ' built_in_chain default_policy by blast
   from assms have stateful_matcher_eq:
    "(λa b. stateful_matcher_tagged' a (packet_tagger' σ' b)) = stateful_matcher' σ'" for σ' by presburger  
  show ?thesis (is "?lhs ⟷ ?rhs")
    proof
      assume ?lhs thus ?rhs
        proof(induction rule: semantics_stateful.induct)
        case 1 thus ?case by(auto intro: semantics_stateful_packet_tagging_intro_start)[1]
        next
        case (2 built_in_chain default_policy p ps  ps_processed σ')
          from 2 have
            "semantics_stateful_packet_tagging rs stateful_matcher_tagged' packet_tagger' state_update' σ⇩0 (built_in_chain, default_policy) (p # ps) ps_processed σ'"
            by blast
          with 2(2,3) show ?case
          apply -
          apply(rule semantics_stateful_packet_tagging_intro_process_one)
             apply(simp_all add: vs_tagged)
          done
       qed
    next
      assume ?rhs thus ?lhs
      proof(induction rule: semantics_stateful_packet_tagging.induct)
        case 1 thus ?case by(auto intro: semantics_stateful_intro_start)
        next
        case (2 built_in_chain default_policy p ps ps_processed σ') thus ?case
           apply -
           apply(rule semantics_stateful_intro_process_one)
              apply(simp_all add: stateful_matcher_eq vs_tagged)
           done
      qed
    qed
  qed


text‹Examples›
context
begin
subsection‹Example: Conntrack with curried matcher›
  text‹We illustrate stateful semantics with a simple example. We allow matching on the states New
  and Established. In addition, we introduce a primitive match to match on outgoing ssh packets (dst port = 22).
  The state is managed in a state table where accepted connections are remembered.›


  text‹SomePacket with source and destination port or something we don't know about›
  private datatype packet = SomePacket "nat × nat" | OtherPacket

  private datatype primitive_matches = New | Established | IsSSH

  text‹In the state, we remember the packets which belong to an established connection.›
  private datatype conntrack_state = State "packet set"

  text‹The stateful primitive matcher: It is given the current state table. 
    If match on @{const Established}, the packet must be known in the state table.
    If match on @{const New}, the packet must not be in the state table.
    If match on @{const IsSSH}, the dst port of the packet must be 22.›
  private fun stateful_matcher :: "conntrack_state ⇒ (primitive_matches, packet) matcher" where
    "stateful_matcher (State state_table) = (λm p. m = Established ∧ p ∈ state_table ∨
                                           m = New ∧ p ∉ state_table ∨
                                           m = IsSSH ∧ (∃dst_port. p = SomePacket (22, dst_port)))"

  text‹Connections are always bi-directional.›
  private fun reverse_direction :: "packet ⇒ packet" where
    "reverse_direction OtherPacket = OtherPacket" |
    "reverse_direction (SomePacket (src, dst)) = SomePacket (dst,src)"

  text‹If a packet is accepted, the state for its bi-directional connection is saved in the state table.›
  private fun state_update' :: "conntrack_state ⇒ final_decision ⇒ packet ⇒ conntrack_state" where
    "state_update' (State state_table) FinalAllow p = State (state_table ∪ {p, reverse_direction p})" |
    "state_update' (State state_table) FinalDeny p = State state_table"

  text‹Allow everything that is established and allow new ssh connections.
    Drop everything else (default policy, see below)›
  private definition "ruleset == [''INPUT'' ↦ [Rule (Match Established) Accept, Rule (MatchAnd (Match IsSSH) (Match New)) Accept]]"

  text‹The @{const ruleset} does not allow @{const OtherPacket}›
  lemma "semantics_stateful ruleset stateful_matcher state_update' (State {}) (''INPUT'', Drop) []
    [(OtherPacket, FinalDeny)] (State {})"
    unfolding ruleset_def
    apply(rule semantics_stateful_intro_process_one)
        apply(simp_all)
       apply(rule semantics_stateful_intro_start)
        apply(simp_all)
     apply(rule seq_cons)
      apply(rule call_result)
        apply(simp_all)
      apply(rule seq_cons)
       apply(auto intro: iptables_bigstep.intros)
    done


  text‹The @{const ruleset} allows ssh packets, i.e. any packets with destination port 22 in the @{const New} rule.
        The state is updated such that everything which belongs to the connection will now be accepted.›
  lemma "semantics_stateful ruleset stateful_matcher state_update' (State {}) (''INPUT'', Drop)
          []
          [(SomePacket (22, 1024), FinalAllow)]
          (State {SomePacket (1024, 22), SomePacket (22, 1024)})"
    unfolding ruleset_def
    apply(rule semantics_stateful_intro_process_one)
        apply(simp_all)
       apply(rule semantics_stateful_intro_start)
        apply(simp_all)
     apply(rule seq_cons)
      apply(rule call_result)
        apply(simp_all)
      apply(rule seq_cons)
       apply(auto intro: iptables_bigstep.intros)
    done

  text‹If we continue with this state, answer packets are now allowed›
  lemma "semantics_stateful ruleset stateful_matcher state_update' (State {}) (''INPUT'', Drop)
          []
          [(SomePacket (22, 1024), FinalAllow), (SomePacket (1024, 22), FinalAllow)]
          (State {SomePacket (1024, 22), SomePacket (22, 1024)})"
    unfolding ruleset_def
    apply(rule semantics_stateful_intro_process_one)
        apply(simp_all)
      apply(rule semantics_stateful_intro_process_one)
         apply(simp_all)
        apply(rule semantics_stateful_intro_start)
         apply(simp_all)
      apply(rule seq_cons, rule call_result, simp_all, rule seq_cons)
        apply(auto intro: iptables_bigstep.intros)
    apply(rule seq_cons, rule call_result, simp_all, rule seq_cons)
      apply(auto intro: iptables_bigstep.intros)
    done

  text‹In contrast, without having previously established a state, answer packets are prohibited›
  text‹If we continue with this state, answer packets are now allowed›
  lemma "semantics_stateful ruleset stateful_matcher state_update' (State {}) (''INPUT'', Drop)
          []
          [(SomePacket (1024, 22), FinalDeny), (SomePacket (22, 1024), FinalAllow), (SomePacket (1024, 22), FinalAllow)]
          (State {SomePacket (1024, 22), SomePacket (22, 1024)})"
    unfolding ruleset_def
    apply(rule semantics_stateful_intro_process_one)
        apply(simp_all)
      apply(rule semantics_stateful_intro_process_one)
         apply(simp_all)
       apply(rule semantics_stateful_intro_process_one)
          apply(simp_all)
        apply(rule semantics_stateful_intro_start)
         apply(simp_all)
       apply(rule seq_cons, rule call_result, simp_all, rule seq_cons, auto intro: iptables_bigstep.intros)+
    done


subsection‹Example: Conntrack with packet tagging›

  datatype packet_tag = TagNew | TagEstablished
  datatype packet_tagged = SomePacket_tagged "nat × nat × packet_tag" | OtherPacket_tagged packet_tag

  fun get_packet_tag :: "packet_tagged ⇒ packet_tag" where
    "get_packet_tag (SomePacket_tagged (_,_, tag)) = tag" |
    "get_packet_tag (OtherPacket_tagged tag) = tag"

  definition stateful_matcher_tagged :: "(primitive_matches, packet_tagged) matcher" where
    "stateful_matcher_tagged ≡ λm p. m = Established ∧ (get_packet_tag p = TagEstablished) ∨
                                           m = New ∧ (get_packet_tag p = TagNew) ∨
                                           m = IsSSH ∧ (∃dst_port tag. p = SomePacket_tagged (22, dst_port, tag))"

  fun calculate_packet_tag :: "conntrack_state ⇒ packet ⇒ packet_tag" where
    "calculate_packet_tag (State state_table) p = (if p ∈ state_table then TagEstablished else TagNew)"

  fun packet_tagger :: "conntrack_state ⇒ packet ⇒ packet_tagged" where
    "packet_tagger σ (SomePacket (s,d)) = (SomePacket_tagged (s,d, calculate_packet_tag σ (SomePacket (s,d))))" |
    "packet_tagger σ OtherPacket = (OtherPacket_tagged (calculate_packet_tag σ OtherPacket))"

  text‹If a packet is accepted, the state for its bi-directional connection is saved in the state table.›
  fun state_update_tagged :: "conntrack_state ⇒ final_decision ⇒ packet ⇒ conntrack_state" where
    "state_update_tagged (State state_table) FinalAllow p = State (state_table ∪ {p, reverse_direction p})" |
    "state_update_tagged (State state_table) FinalDeny p = State state_table"


  
  text‹Both semantics are equal›
  lemma "semantics_stateful rs stateful_matcher state_update' σ⇩0 start ps ps_processed σ' =
    semantics_stateful_packet_tagging rs stateful_matcher_tagged packet_tagger state_update' σ⇩0 start ps ps_processed σ'"
    apply(rule semantics_stateful_vs_tagged)
    apply(intro allI, rename_tac m σ p)
    apply(case_tac σ)
    apply(case_tac p)
     apply(simp_all add: stateful_matcher_tagged_def)
    apply force
    done
end

end