Can my Firewall System Enforce this Policy?

Firewalls are a fundamental tool for managing and protecting computer networks. They behave according to a configuration that specifies the desired policy, i.e., which packets are allowed to enter a network, possibly with modified addresses. Several tools allow the user to specify policies in various high level languages, and to compile them into different target configuration languages, as well as to automatically migrate a configuration from a system to another. Often, these tools implicitly assume that the target system can enforce any desired policy. Unexpectedly, we find that this is not always the case. In particular, we show that the most common UNIX firewall systems, i.e., iptables, ipfw, pf, are not equally expressive, in that some policies can be implemented in one system but not in another. Here, we formally investigate the expressive power of these firewall systems using techniques from programming language semantics, and set up a formal model to precisely characterize their relationships. Based on this formal model we then present F2F, a prototypical tool that predicts when a policy cannot be expressed in a given system. Our prototype gives detailed information about the unexpressible parts of a policy and provides administrators with hints for fixing the detected problems.