Formal Correctness of Conflict Detection for Firewalls

Overview

This paper describes the formalization of a correctness proof for a conflict detection algorithm for firewalls in the Coq Proof Assistant. First, it gives formal definitions in Coq of a firewall access rule and of an access request to a firewall. Formally, two rules are in conflict if there exists a request on which one rule would allow access and the other would deny it. The algorithms are expressed in Coq, and prove that it finds all conflicts in a set of rules.