A Formal Analysis of SCTP: Attack Synthesis and Patch Verification

TL;DR

This work presents a formal security analysis of SCTP by constructing a faithful Promela model, specifying ten $LTL$ correctness properties, and verifying them with the $SPIN$ model checker. It extends the attack-synthesis tool $Korg$ to SCTP and explores four attacker models—Off-Path, Evil-Server, Replay, and On-Path—finding a CVE-2021-3772-inspired attack in the Off-Path case and multiple attacks in other models. The authors demonstrate that the RFC 9260 patch resolves the CVE attack without introducing new flaws under the stated properties, and they identify an RFC ambiguity that can lead to an insecure interpretation, proposing an erratum. They also reveal practical considerations for patch synthesis and emphasize the importance of handling unexpected yet valid packets and timer configurations. The work contributes open-source tooling and a rigorous FM-based perspective on SCTP’s security, with implications for protocol design, implementation, and standardization.

Abstract

SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance tests using the PacketDrill tool. Conformance testing is not exhaustive and a recent vulnerability (CVE-2021-3772) showed SCTP is not immune to attacks. Changes addressing the vulnerability were implemented, but the question remains whether other flaws might persist in the protocol design. We study the security of the SCTP design, taking a rigorous approach rooted in formal methods. We create a formal Promela model of SCTP, and define 10 properties capturing the essential protocol functionality based on its RFC specification and consultation with the lead RFC author. Then we show using the Spin model checker that our model satisfies these properties. We define 4 attacker models - Off-Path, where the attacker is an outsider that can spoof the port and IP of a peer; Evil-Server, where the attacker is a malicious peer; Replay, where an attacker can capture and replay, but not modify, packets; and On-Path, where the attacker controls the channel between peers. We modify an attack synthesis tool designed for transport protocols, Korg, to support our SCTP model and four attacker models. We synthesize 14 unique attacks using the attacker models - including the CVE vulnerability in the Off-Path attacker model, 4 attacks in the Evil-Server attacker model, an opportunistic ABORT attack in the Replay attacker model, and eight connection manipulation attacks in the On-Path attacker model. We show that the proposed patch eliminates the vulnerability and does not introduce new ones according to our model and protocol properties. Finally, we identify and analyze an ambiguity in the RFC, which we show can be interpreted insecurely. We propose an erratum and show that it eliminates the ambiguity.

Figures (15)

• Figure 1: Message sequence chart illustrating SCTP active/passive association establishment routine. Arrows indicate communication direction and time flows from the top down.
• Figure 2: SCTP active/passive association teardown.
• Figure 3: Attack disclosed in CVE-2021-3772. Peers A and B begin having established an association with vtags $i_1, i_2$ (resp.). The Attacker transmits an invalid INIT chunk to A, spoofing the port and IP of B. Peer A responds by sending a valid ABORT to B, which closes the association. By sending a single invalid INIT the Attacker performs a DoS.
• Figure 4: The system $\textsc{UserA} \parallel \textsc{PeerA} \parallel \textsc{Channel} \parallel \textsc{PeerB} \parallel \textsc{UserB}$. Channel contains a size-1 FIFO buffer in each direction (AtoB and BtoA, respectively). Arrows indicate communication direction. Composition between Channel and peers is rendezvous (the buffers are inside Channel).
• Figure 5: SCTP Finite State Machine. $x,v,i?$ (or $x,v,i!$) denotes receive (or send) chunk $x$ with vtag $v$ and itag $i$. Events in multi-event transitions occur in the order they are listed. Logic for OOTB packets, ABORT messages or User_Abort commands, unexpected user commands, and data exchange are ommitted but faithfully implemented in the model and described in this paper.