Boolean Expressions in Firewall Analysis

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 the firewall policy. This shows that past results suggesting a combinatorial explosion when converting from a Boolean expression in CNF to one in DNF does note occur in the context of firewall analysis