  In modern networks, forwarding of packets often depends on the history of
previously transmitted traffic. Such networks contain stateful middleboxes,
whose forwarding behaviour depends on a mutable internal state. Firewalls and
load balancers are typical examples of stateful middleboxes.
  This work addresses the complexity of verifying safety properties, such as
isolation, in networks with finite-state middleboxes. Unfortunately, we show
that even in the absence of forwarding loops, reasoning about such networks is
undecidable due to interactions between middleboxes connected by unbounded
ordered channels. We therefore abstract away channel ordering. This abstraction
is sound for safety, and makes the problem decidable. Specifically, safety
checking becomes EXPSPACE-complete in the number of hosts and middleboxes in
the network. To tackle the high complexity, we identify two useful subclasses
of finite-state middleboxes which admit better complexities. The simplest class
includes, e.g., firewalls and permits polynomial-time verification. The second
class includes, e.g., cache servers and learning switches, and makes the safety
problem coNP-complete.
  Finally, we implement a tool for verifying the correctness of stateful
networks.
