Automatic Discovery of Evasion Attacks Against Stateful Firewalls (CMU-CyLab-21-001)

Stateful firewalls (FW) play a critical role in securing our current network infrastructure in various deployments. In this work, we focus on discovering evasion attacks that arise due to semantic implementation vulnerabilities of the intended stateful behaviors. Such attacks enable firewall evasion even if the rules are configured correctly. This is in contrast to prior work that focused on software bugs for privilege escalation and/or policy misconfigurations. Given the black-box and proprietary nature of firewall implementations, we design and implement a model-guided approach for uncovering such evasion vulnerabilities. Specifically, we infer a behavioral model of a specific FW implementation and then use the inferred model to synthesize attack strategies for a given deployment and threat model. In designing Pryde, we address key technical challenges in ensuring that our model inference is tractable and our attack synthesis can cover multiple semantic vulnerability opportunities. We evaluate Pryde on four production-quality firewalls. We discover thousands of distinct attack sequences for 4 popular firewalls (FW).