A model of stateful firewalls and its properties

We propose the first model of stateful firewalls. In this model, each stateful firewall has a variable set called the state of the firewall, which is used to store some packets that the firewall has accepted previously and needs to remember in the near future. Each stateful firewall consists of two sections: a stateful section and a stateless section. Upon receiving a packet, the firewall processes it in two steps. In the first step, the firewall augments the packet with an additional field called the tag, and uses the stateful section to compute the value of this field according to the current state of the firewall. In the second step, the firewall compares the packet together with its tag value against a sequence of rules in the stateless section to identify the first rule that the packet matches: the decision of this rule determines the fate of the packet. Our model of stateful firewalls has several favorable properties. First, despite its simplicity, it can express a variety of state tracking functionalities. Second, it allows us to inherit the rich results in stateless firewall design and analysis. Third, it provides backward compatibility such that a stateless firewall can also be specified using our model. This paper goes beyond proposing this stateful firewall model itself. A significant portion of this paper is devoted to analyzing the properties of stateful firewalls that are specified using our model. We outline a method for verifying whether a firewall is truly stateful. The method is based on the three properties of firewalls: conforming, grounded, and proper. We show that if a firewall satisfies these three properties, then the firewall is truly stateful.