Jacob Ginesin*, Max von Hippel*, Evan Defloor, Cristina Nita-Rotaru, Michael Tüxen
Northeastern University, FH Munster
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.
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.
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:
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.
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!
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 :-)
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.
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.
@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
}
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.