Theory StatefulCore
subsection ‹Stateful Protocols: Foundations›
theory
StatefulCore
imports
"../PacketFilter/PacketFilter"
LTL_alike
begin
text‹
The simple system of a stateless packet filter is not enough to model all common real-world
scenarios. Some protocols need further actions in order to be secured. A prominent example is
the File Transfer Protocol (FTP), which is a popular means to move files across the Internet.
It behaves quite differently from most other application layer protocols as it uses a two-way
connection establishment which opens a dynamic port. A stateless packet filter would only have
the possibility to either always open all the possible dynamic ports or not to allow that
protocol at all. Neither of these options is satisfactory. In the first case, all ports above
1024 would have to be opened which introduces a big security hole in the system, in the second
case users wouldn't be very happy. A firewall which tracks the state of the TCP connections on
a system does not help here either, as the opening and closing of the ports takes place on the
application layer. Therefore, a firewall needs to have some knowledge of the application
protocols being run and track the states of these protocols. We next model this behaviour.
The key point of our model is the idea that a policy remains the same as before: a mapping from
packet to packet out. We still specify for every packet, based on its source and destination
address, the expected action. The only thing that changes now is that this mapping is allowed
to change over time. This indicates that our test data will not consist of single packets but
rather of sequences thereof.
At first we hence need a state. It is a tuple from some memory to be refined later and the
current policy.
›
type_synonym ('α,'β,'γ) FWState = "'α × (('β,'γ) packet ↦ unit)"
text‹Having a state, we need of course some state transitions. Such
a transition can happen every time a new packet arrives. State
transitions can be modelled using a state-exception monad.
›
type_synonym ('α,'β,'γ) FWStateTransitionP =
"('β,'γ) packet ⇒ ((('β,'γ) packet ↦ unit) decision, ('α,'β,'γ) FWState) MON⇩S⇩E"
type_synonym ('α,'β,'γ) FWStateTransition =
"(('β,'γ) packet × ('α,'β,'γ) FWState) ⇀ ('α,'β,'γ) FWState"
text‹The memory could be modelled as a list of accepted packets.›
type_synonym ('β,'γ) history = "('β,'γ) packet list"
fun packet_with_id where
"packet_with_id [] i = []"
|"packet_with_id (x#xs) i = (if id x = i then (x#(packet_with_id xs i)) else (packet_with_id xs i))"
fun ids1 where
"ids1 i (x#xs) = (id x = i ∧ ids1 i xs)"
|"ids1 i [] = True"
fun ids where
"ids a (x#xs) = (NetworkCore.id x ∈ a ∧ ids a xs)"
|"ids a [] = True"
definition applyPolicy:: "('i × ('i ↦ 'o)) ↦ 'o"
where "applyPolicy = (λ (x,z). z x)"
end