Distributed firewall anomaly detection through LTL model checking

An anomaly in a firewall is a relationship between two of its rules that may hint at a possible misconfiguration of its filter. While checking anomalies within a single firewall is well understood, identifying anomalies across multiple firewalls in a network is a much harder problem that has only been studied for restricted cases. In particular, we show that the correct identification of anomalies must take into account the routing function performed in each node of the network. We introduce a formal model of firewalls and routing tables that generalizes past work on the topic; in particular, we show how the detection of anomalies in this model reduces to the model checking of particular instances of Linear Temporal Logic formulæ. An implementation of an anomaly detector that leverages existing model checkers reveals that distributed anomalies can be identified at a reasonable cost.