A Formal Analysis of SCTP: Attack Synthesis and Patch Verification

Introduction

We use formal methods, namely the Spin model checker, to analyze the security of the Stream Control Transmission Protocol (SCTP). SCTP underpins many telecommunication protocols including SS7, 4G, and 5G, WebRTC, and several internet architecture protocol including IP, SIP, and WiMAX. We report a symphony of new attacks on SCTP across various attacker models, the automated re-discovery of a previously reported denial of service attack (CVE-2021-3772), and two ambiguities in SCTP RFC that, if misinterpreted, enable attacks.

Extra Details

If you're interested in the main results of this work, please read the paper. Otherwise, here are some footnotes and extra details I've accumulated over the year and a half I've worked on this project.

Context around the first ambiguity

In our paper we claim that section 5.2.1 of RFC9260 is textually ambiguous, thus enabling an off-path attack. After completing this paper, a conversation with the SCTP IETF maintainer1 revealed that 5.2.1 is not necessarily ambiguous despite appearing to be. This is because significant external context (which is not necessarily made clear) disambiguates the text. For reference, here's the ambiguous section of 5.2.1 with reference labeling from AllenNLP's coreference resolution model:

I assumed the ambiguous scenario was along the following lines. Suppose two SCTP peers, Peer A and Peer B, intend to establish a connection. Assume an off-channel attacker knows the IP addresses and the ports of the two peers, but not the vtag of the connection. Peer A sends an INIT chunk and moved from CLOSED to COOKIE_WAIT. Peer B receives the INIT chunk and replies with an INIT-ACK chunk. Peer A receives the INIT-ACK chunk, responds with a COOKIE-ECHO chunk, and moves into COOKIE-ECHOED. The attacker then sends an INIT chunk to Peer A. How should peer A respond? Particularly, what parameters should Peer A fill into the INIT-ACK chunk? As you mentioned above Peer A has two choices: (1), use the verification tag that Peer A initially sent to Peer B to initialize the connection, or (2), use the verification tag from the INIT chunk Peer A received from the attacker. The former is the intended interpretation, and the latter interpretation leads to an off-channel attack (which we prove with our model).

At least from what it seems, "it" and "its" in the above text are nonspecific and ambiguous. The subject of the sentence is Peer A (as opposed to peer B), which would grammatically imply "it" and "its" in the sentence refer to Peer A, which is the wrong interpretation.

However, the verification tag is not a parameter of a chunk, but rather a part of the common header, and thus not specified by the text from 5.2.1 I quote above. The peer receiving an INIT chunk can choose to fill in the INIT chunk from the handshake initializing the previous connection (the incorrect interpretation), or fill in the verification tag based on the received INIT chunk (the correct interpretation). This behavior is not explicitly specified and rather implied through 3.3.3. This seems to be in contrast to 5.2.2, which chooses to specifically specify how the verification tag should be filled:


Ideally 5.2.1 should be updated with similar text explicitly specifying how the verification tag should be handled, but the IETF SCTP committee didn't seem so motivated. While the FreeBSD and Linux implementations of SCTP seem to behave correctly here (according to our packetdrill test), it's yet to be seen whether this is the case for the other implementations, including usrsctp. I may eventually file an errata if I find an implementation misinterprets this case.

Short independent writeup for the second ambiguity

For my own documentation purposes, I wrote a short independent writeup on the second ambiguity I found in RFC9260. You can find that writeup here.

Testing multiple LTL properties at once

Spin, by default, does not allow for testing multiple LTL properties at once. Although this limitation makes sense, as Spin works by translating both the model and the property into Buchi automata and intersecting them, it is annoying for development purposes. So, I wrote this nice shellscript that tests all the properties in a folder against a model, builds a nice report, and saves all the traces. It's useful on its own, so feel free to use it!

Adding replay, drop, and reorder on-channel attacker-models to Korg

In this work we made some modifications to Korg, our attack synthesis tool. Among other changes, I wrote an extension of Korg to generate an attacker capable of replaying packets. This attacker model is not specific to SCTP and can be applied to any generic Promela model. However, since this paper was published, I've made many additional changes and improvements to this Korg extension. Among other changes, I've added support for the synthesis of an attacker that can drop or reorder messages on an arbitrary Promela channel, as well as some additional search space optimizations. This is unpublished, and will likely appear in a future paper! If you're interested in using Korg with my private (for now) extensions, do reach out and we can chat :-)

LKSCTP Experimental Setup

In addition to the packetdrill analysis, having deeply studied the Linux Kernel SCTP implementation I created for myself an experimental packet injection setup, which I detailed in this github gist.

On automatically repairing attacks synthesized by Korg

In the conclusion of the paper, we briefly mention our failed attempt to create a pipeline to automatically repair programs whom had attacks successfully generated with Korg. I spent a good amount of effort on this and wrote a brief preliminary report on the theory and methodology (warning: this work is preliminary and likely contains mistakes).

There are two major problems preventing us from directly applying this approach to Korg. First, our repair algorithm is very expensive and requires very strong heuristics to be usable. Second, our approach is automata-theoretic, and thus would require deriving an automata from a Promela model, repairing the automata, and re-propagating the repaired automata into a new Promela model. While deriving an automata from a Promela model and repairing it is doable via the spot toolset, re-propagating an automata to a Promela model is generally infeasible.

Further Reading

If you thought this paper was interesting, here are some other great reads.

1. Automated Attacker Synthesis for Distributed Protocols
2. LTSMIN, essentially the modern version of Spin
3. The Spot toolset has proven to be fantastic for manipulating and debugging ω-automata and LTL properties
4. "Exposing The Flaw In Our Phone System" - A Youtube video by Veritasium on exploiting the SS7 protocol, which relies on SCTP

Footnotes

Bibtex Citation

@inproceedings {GinesinSCTP2024,
  author = {Jacob Ginesin and Max von Hippel and Evan Defloor and Cristina Nita-Rotaru and Michael T{\"u}xen},
  title = {A Formal Analysis of {SCTP}: Attack Synthesis and Patch Verification},
  booktitle = {33rd USENIX Security Symposium (USENIX Security 24)},
  year = {2024},
  isbn = {978-1-939133-44-1},
  address = {Philadelphia, PA},
  pages = {3099--3116},
  url = {https://www.usenix.org/conference/usenixsecurity24/presentation/ginesin},
  publisher = {USENIX Association},
  month = aug
}

Plaintext Citation

Jacob Ginesin, Max von Hippel, Evan Defloor, Cristina Nita-Rotaru, and Michael Tüxen. "A Formal Analysis of SCTP: Attack Synthesis and Patch Verification." In 33rd USENIX Security Symposium (USENIX Security 24), Philadelphia, PA, 2024, pp. 3099-3116. USENIX Association. August 2024.