Boolean Expressions in Firewall Analysis
Adam Hamilton, Matthew Roughan, and Giang T. Nguyen

TL;DR
This paper models firewall policies as Boolean expressions, providing an efficient translation algorithm into CNF or DNF with polynomial size bounds, facilitating verification with SAT solvers.
Contribution
It introduces a novel algorithm for translating firewall rules into Boolean expressions with polynomial size bounds, addressing complexity issues in firewall analysis.
Findings
Polynomial bounds on Boolean expression size
Efficient translation of firewall rules into CNF/DNF
No exponential explosion in size during conversion
Abstract
Firewall policies are an important line of defence in cybersecurity, specifying which packets are allowed to pass through a network and which are not. These firewall policies are made up of a list of interacting rules. In practice, firewall can consist of hundreds or thousands of rules. This can be very difficult for a human to correctly configure. One proposed solution is to model firewall policies as Boolean expressions and use existing computer programs such as SAT solvers to verify that the firewall satisfies certain conditions. This paper takes an in-depth look at the Boolean expressions that represent firewall policies. We present an algorithm that translates a list of firewall rules into a Boolean expression in conjunctive normal form (CNF) or disjunctive normal form (DNF). We also place an upper bound on the size of the CNF and DNF that is polynomial in the number of rules in…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNetwork Packet Processing and Optimization · Network Security and Intrusion Detection · Internet Traffic Analysis and Secure E-voting
