Formal Verification of SYN Flood Attacks Using Dafny

This project formally models and verifies the TCP three-way handshake and SYN flood denial-of-service attack using Dafny, a verification-aware programming language. It demonstrates how a SYN flood attack exhausts a server's backlog queue, preventing legitimate clients from establishing connections.

Project Structure

ECS261-Project/
|-- pyproject.toml                 # uv project configuration
|-- .venv/                         # Python virtual environment (created by uv sync)
|-- syn_flood_simulation.py        # Python simulation (automated + interactive)
|-- 01_Dafny/
|   |-- 3_way_handshake.dfy        # Dafny model: TCP 3-way handshake (packet-level)
|   |-- SYN_Flooding_attack.dfy    # Dafny model: SYN flood (batch processing)
|   |-- crypto_hash.dfy            # Dafny model: SYN Cookie (Dafny only)
|   |-- 3_way_handshake-py/        # Dafny-compiled Python (auto-generated)
|   |-- SYN_Flooding_attack-py/    # Dafny-compiled Python (auto-generated)
|-- 00_toycodes/                   # Early prototypes and experiments

Dafny Models

3_way_handshake.dfy

Models the TCP three-way handshake at the packet level with full formal verification. Key components:

• ConnectionState: CLOSED | LISTEN | SYN_SENT | SYN_RECV | ESTABLISHED
• ConnState: Per-connection state tracking with separate client-side and server-side states, matching the real TCP state machine exactly.
• TCPHandshake class: Manages packets, backlog (half-open connections), and established connections.

Four verified methods model each step of the handshake:

Step	Method	Client State	Server State
1	ClientSendSyn	CLOSED -> SYN_SENT	LISTEN (unchanged)
2	ServerReceiveSyn	SYN_SENT (unchanged)	LISTEN -> SYN_RECV
3	ClientSendAck	SYN_SENT -> ESTABLISHED	SYN_RECV (unchanged)
4	ServerReceiveAck	ESTABLISHED (unchanged)	SYN_RECV -> ESTABLISHED

Each method has Dafny requires (preconditions) and ensures (postconditions) that are statically verified, guaranteeing correctness of the protocol logic.

The file also includes two test methods (TestSingleClientHandshake and TestTwoClientsHandshake) that verify the model handles single and concurrent client connections correctly.

SYN_Flooding_attack.dfy

Models the SYN flood attack at a higher abstraction level using batch client processing. Key features:

• HandleSyn method: Processes a single SYN request and returns ATTACK, CONNECTED, or REJECTED.
• ProcessClients method: Batch processes multiple clients and returns the final backlog state.
• Formally verifies that attackers (who never send ACK) fill the backlog, causing legitimate clients to be rejected.

crypto_hash.dfy — SYN Cookie Defense (Dafny Only)

Models a SYN Cookie defense mechanism using cryptographic hash verification. This is a Dafny-only formal verification model — there is no corresponding Python simulation. The SYN Cookie defense is verified entirely within Dafny, demonstrating how the server can eliminate the backlog by encoding connection state into the SYN-ACK sequence number via a cryptographic hash (Cookie function). The key insight verified by Dafny:

• No backlog required: Unlike the standard 3-way handshake model, TCPHandshakeSYNCookies does not maintain a backlog or capac field.
• Stateless verification: The server recomputes the expected cookie on receiving ACK, verifying the client's legitimacy without storing half-open connection state.

Note: Since SYN Cookies are a defense mechanism (not an attack), they are modeled purely in Dafny for formal verification purposes. The Python simulation focuses on demonstrating the SYN flood attack behavior.

Python Simulation

syn_flood_simulation.py integrates both Dafny models compiled to Python, providing two modes of operation:

Automated Demo (default)

uv run python syn_flood_simulation.py

Runs a three-phase simulation:

1. Phase 1: Two legitimate clients complete the full 3-way handshake.
2. Phase 2: Eight attacker threads send SYN packets concurrently, filling the server backlog.
3. Phase 3: A new legitimate client attempts to connect and is rejected (denial of service confirmed).

Interactive Mode

uv run python syn_flood_simulation.py --interactive

Provides a menu-driven interface to step through the handshake one operation at a time:

Action	Description
[1]	Client sends SYN packet
[2]	Server receives SYN, sends SYN-ACK
[3]	Client receives SYN-ACK, sends ACK
[4]	Server receives ACK, connection ESTABLISHED
[5]	Launch SYN flood attack (8 attackers)
[6]	Show server status with per-connection states
[7]	Run full automated demo

Server status displays per-connection state information read directly from the Dafny model's connStates map, ensuring the Python simulation and the verified Dafny model are always in sync.

  Per-Connection States (from Dafny model):
  +----------+--------------+--------------+------------+
  | ClientID | Client State | Server State |    Type    |
  +----------+--------------+--------------+------------+
  |        1 | ESTABLISHED  | ESTABLISHED  | legitimate |
  |      101 | SYN_SENT     | SYN_RECV     | attacker   |
  |      102 | SYN_SENT     | SYN_RECV     | attacker   |
  ...

Prerequisites

• Dafny (version 4.x or later)
• uv (Python package & environment manager)
• Python 3.10 or later

Environment Setup (uv)

This project uses uv for Python virtual environment management. uv automatically creates and manages a .venv directory — no need for Docker or manual venv setup.

1. Install uv (if not already installed)

curl -LsSf https://astral.sh/uv/install.sh | sh

2. Create the virtual environment and install dependencies

cd ECS261-Project
uv sync

This creates a .venv/ directory with an isolated Python environment. Since this project has no external PyPI dependencies (it uses Dafny-compiled Python modules directly), uv sync simply sets up the environment.

Building and Running

1. Verify the Dafny models

cd 01_Dafny
dafny verify 3_way_handshake.dfy
dafny verify SYN_Flooding_attack.dfy
dafny verify crypto_hash.dfy

All files should report 0 errors.

2. Compile Dafny to Python

cd 01_Dafny
dafny build --target:py 3_way_handshake.dfy
dafny build --target:py SYN_Flooding_attack.dfy

This generates the 3_way_handshake-py/ and SYN_Flooding_attack-py/ directories containing the compiled Python modules.

Note: crypto_hash.dfy does not need to be compiled to Python. It is verified within Dafny only (dafny verify crypto_hash.dfy).

3. Run the Python simulation

From the repository root, use uv run to execute within the virtual environment:

# Automated demo
uv run python syn_flood_simulation.py

# Interactive mode
uv run python syn_flood_simulation.py --interactive

uv run ensures the command runs inside the .venv virtual environment without needing to manually activate it.

4. Run the standalone toy code (optional)

uv run python 00_toycodes/3_way_handshake.py

How the SYN Flood Attack Works

In a normal TCP connection, the client and server exchange three messages (SYN, SYN-ACK, ACK) to establish a connection. The server allocates a backlog entry for each connection in progress (half-open / SYN_RECV state).

In a SYN flood attack:

1. Attackers send SYN packets but never reply with ACK.
2. Each attacker's connection remains in the SYN_RECV state on the server.
3. These half-open connections fill the server's fixed-size backlog.
4. Once the backlog is full, the server cannot accept new SYN packets.
5. Legitimate clients are rejected, resulting in denial of service.

This project formally verifies this behavior: Dafny's static verifier proves that when the backlog is full (|backlog| >= capacity), the precondition requires |backlog| < capac of ServerReceiveSyn is violated, making it impossible for the server to accept new connections.