Abstract
Continuous verification of network security compliance is an accepted
need. Especially, the analysis of stateful packet filters plays a
central role for network security in practice. But the few existing
tools which support the analysis of stateful packet filters are based on
general applicable formal methods like Satifiability Modulo Theories
(SMT) or theorem prover and show runtimes in the order of minutes to
hours making them unsuitable for continuous compliance verification.
In this work, we address these challenges and present the concept of
state shell interweaving to transform a stateful firewall rule set into
a stateless rule set. This allows us to reuse any fast domain specific
engine from the field of data plane verification tools leveraging smart,
very fast, and domain specialized data structures and algorithms
including Header Space Analysis (HSA). First, we introduce the formal
language FPL that enables a high-level human-understandable
specification of the desired state of network security. Second, we
demonstrate the instantiation of a compliance process using a
verification framework that analyzes the configuration of complex
networks and devices - including stateful firewalls - for compliance
with FPL policies. Our evaluation results show the scalability of the
presented approach for the well known Internet2 and Stanford benchmarks
as well as for large firewall rule sets where it outscales
state-of-the-art tools by a factor of over 41.