Firewall anomaly detection with a model checker for visibility logic

An anomaly in a firewall is a relationship between two of its rules that may hint at a possible misconfiguration of its filter. One notable limitation of existing solutions for firewall analysis is that they provide algorithms tailored for the verification of specific anomalies. We introduce a modal logic, called Visibility Logic (VL), which can be used to express arbitrary patterns between rules inside a firewall. A model checker allows one to verify any formula expressed in visibility logic, of which traditional anomalies are merely particular instances, with running times of under one second for 1,500 rules.