Verification and Attack Synthesis for Network Protocols

TL;DR

This dissertation presents a comprehensive, formal treatment of network protocol correctness, performance, and security using a trio of formal methods: theorem proving (Ivy, ACL2s/ACL2(r)), model checking (SPIN), and automated program/attack synthesis (Korg). It introduces formal models for key RTT/RTO components (Karn's Algorithm and RFC 6298), Go-Back-N with a realistic token-bucket network, and correctness proofs for TCP, DCCP, and SCTP handshakes, including attacker synthesis that automatically uncovers vulnerabilities and patches (e.g., SCTP CVE-2021-3772 and related RFC ambiguities). The work demonstrates both the feasibility and utility of combining multiple FM techniques to verify core internet protocols under normal and adversarial conditions, providing open-source artifacts to reproduce results and guiding RFC refinement. Collectively, the results yield precise guarantees about protocol behavior, inform practical patching and hardening efforts, and illustrate a replicable methodology for formal analysis of protocol designs and security properties with real-world impact.

Abstract

Network protocols are programs with inputs and outputs that follow predefined communication patterns to synchronize and exchange information. There are many protocols and each serves a different purpose, e.g., routing, transport, secure communication, etc. The functional and performance requirements for a protocol can be expressed using a formal specification, such as, a set of logical predicates over its traces. A protocol could be prevented from achieving its requirements due to a bug in its design or implementation, a component failure (e.g., a crash), or an attack. This dissertation shows that formal methods can feasibly characterize the functionality and performance of network protocols under normal conditions as well as when subjected to attacks.

Figures (25)

• Figure 1: Illustration of an ambiguous Ack, with the sender's local clock shown on the left. Sender's packets are illustrated as packets, while receiver's Acks are shown as envelopes. The first time the sender transmits 2 the packet is lost in-transit. Later, upon receiving a cumulative Ack of 2, the sender determines the receiver had not yet received the 2 packet and thus the packet might be lost in transit. It thus retransmits 2. Ultimately the receiver receives the retransmission and responds with a cumulative Ack of 4. When the sender receives this Ack it cannot determine which 2 packet delivery triggered the ACK transmission and thus, it does not know whether to measure an RTT of 7-3=4 or 7-6=1. Hence, the Ack is ambiguous, so any sampled RTT would be as well.
• Figure 2: The sender, channel, and receiver. The sender sends packets by $\mathit{snd}_s$ actions which are received by $\mathit{rcv}_r$ actions at the receiver's endpoint, and similarly, the receiver sends Acks by $\mathit{snd}_r$ actions which are received by $\mathit{rcv}_s$ actions at the receiver's endpoint.
• Figure 3: Message sequence chart illustrating an example execution. Time progresses from top down. Instructions executed by Alg. \ref{['AlgKarn']} are shown on the left, and the sender's execution is on the right. $\mathit{snd}_s$ events are indicated with arrows from sender to channel, $\mathit{rcv}_r$ events with arrows from channel to receiver, etc. After the final $\mathit{rcv}_s$ event, sender executes Line \ref{['sample']} and outputs the computation $\hbox{\sf S}\xspace = 6 - 2 = 4$.
• Figure 4: On the left are two $67.5/7.5$ steady-state scenarios. On top the samples are drawn from the uniform distribution over the bounds, and timeouts rarely, if ever, occur. In the bottom (pathological) scenario, every 100$^{\text{th}}$ sample equals $c+r = 75$ while the rest equal $c-r = 60$, and at each "spike", a timeout occurs. There are infinitely many spikes, and one is shown on the right ($n=[350,450]$).
• Figure 5: Example message sequence charts for GB$(1)$ and GB$(2)$. In both, the receiver waits to receive $N$ packets (regardless of whether or not these packets are in order) before transmitting an Ack$a$ cumulatively acknowledging all packets $p < a$. The sender in both charts successfully transmits an entire window, but then loses the first transmission of the subsequent window. In GB$(1)$, the entire second window is lost, resulting in a retransmission. On the other hand, in GB$(2)$, the second window consists of two packets, the second of which (carrying sequence number $4$) is successfully received, but not delivered since it is out of order. Since the packet with sequence number $3$ did not make it through, the sender is forced to retransmit.

Theorems & Definitions (23)

• proof
• Theorem 1
• Theorem 2
• Theorem 3
• Definition 1: Serial TBF Composition
• Definition 2: Abstract TBF Composition
• Definition 3: Reachability
• Definition 4: TBF Equivalence
• Theorem 4
• Theorem 5