Networking infrastructure, such as routers and firewalls, consist of a policy (i.e., where to forward which packets) and a mechanism that implements it. As the correctness of the policy is critical, it is a natural candidate for formal verification. Indeed, several verification algorithms have been developed, that detect anomalies, conflicts, and redundancies in practical firewalls and flow tables. However, theory suggests that the problem is intractable in general: the decision tree for a policy is of size O((2n)d), where n is the number of rules and d is the number of observed features used in making the decision. (In a typical firewall, n = 1000 and d = 10.) In this paper, we show why the verification of practical firewalls is not as hard as previously thought. Using a new concept, “rules in play,” we find a new, tight bound on the size of the decision tree, and suggest three other factors - narrow fields, singletons, and all-matches - that make the problem tractable in practice. We also present an algorithm to solve an open problem: pruning a policy to the minimum possible number of rules, without changing its meaning.
展开▼
