2024-moon-pryde
findings extracted from this paper
-
Stateful firewalls used as censorship middleboxes exhibit counter-intuitive implementation behaviors: FW-3 forwards ACK packets before a TCP handshake is initiated, and FW-1 actively spoofs RST packets in response to unsolicited traffic to thwart evasion attempts. These vendor-specific quirks create or close evasion opportunities that are invisible to rule-verification tools and not predictable from policy documentation alone.
-
Evasion attacks generated against one firewall-deployment combination do not transfer well to other settings: a deployment-agnostic approach (used by censorship circumvention tools) fails to generate effective attacks across diverse victim stacks and attacker capabilities. Pryde's deployment-aware, modular workflow finds successful attacks across configurations with and without insider threats, and against multiple attacker success criteria (data delivery vs. victim ACK vs. attacker receipt of ACK).
-
TCP-compliant packet alphabets are insufficient for modeling stateful firewall evasion. Including non-TCP-compliant traffic — specifically flipped-direction SYNs, out-of-window seq/ack numbers, and packets that form a parallel TCP connection in the reverse direction — is what unlocks discovery of deep attack paths. Prior model-inference work (Alembic) that restricted itself to compliant sequences produced models incapable of generating any of the 6,000+ attacks Pryde found.
-
Pryde generates more than 6,000 successful and unique evasion attacks against 4 popular stateful firewalls, which is 2–3 orders of magnitude higher than censorship circumvention algorithms (e.g., Geneva) and black-box fuzzing. The gap arises because circumvention tools only uncover shallow evasion sequences and cannot systematically explore the full attack-state space.