Formal correctness of conflict detection for firewalls

We describe the formalization of a correctness proof for a conflict detection algorithm for firewalls in the Coq Proof Assistant. First, we give 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. We express our algorithm in Coq, and prove that it finds all conflicts in a set of rules. We obtain an OCaml version of the algorithm by direct program extraction. The extracted program has successfully been applied to firewall specifications with over 200,000 rules. Categories and Subject Descriptors F.3.1 [Specifying and Verifying and Reasoning about Programs]: Mechanical verification; C.2.0 [General]: Security and protection General Terms Security, Verification Keywords Coq, Firewall

• Type: Conference
• Year: 2007
• Where: CCS
• Authors: Venanzio Capretta, Bernard Stepien, Amy P. Felty, Stan Matwin
• Keywords: CCS 2007, Conflict Detection Algorithm, Coq Proof Assistant, Firewall Access Rule, Security Privacy