A Formal Analysis of SCTP: Attack Synthesis and Patch Verification

• URL: http://arxiv.org/abs/2403.05663v1
• Date: Fri, 8 Mar 2024 20:38:56 GMT
• Title: A Formal Analysis of SCTP: Attack Synthesis and Patch Verification
• Abstract summary: We study the security of the SCTP design, taking a rigorous approach rooted in formal methods. 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.
• Score: 7.331862211069559
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Recognition Without Enforcement: Configuration-Dependent Failures in LLM Agent Instruction Arbitration and External Control [0.0]
  LLM agents arbitrate among instructions from system prompts, users, memory, and tools, but this arbitration cannot be assumed to enforce trust boundaries.<n>We identify a recognition-enforcement gap: source-format features are linearly decodable from model activations, and models can explicitly identify forged authority when prompted.<n>We treat model self-arbitration as a capability rather than a security boundary and implement an external reference monitor combining authenticated source routing with capability-gated tool execution.
  arXiv  Detail & Related papers  (2026-08-28T16:34:05Z)
• Repurposing Backdoors for Good: Ephemeral Intrinsic Proofs for Verifiable Aggregation in Cross-silo Federated Learning [30.440611659881494]
  We propose a lightweight architecture that shifts from cryptographic proofs to textitIntrinsic Proofs<n>We harness Catastrophic Forgetting to embed verification signals directly into model parameters.<n>Our approach achieves over $1000times$ speedup on ResNet-18 compared to cryptographic baselines, effectively scaling to large models.
  arXiv  Detail & Related papers  (2026-03-11T12:04:18Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  We study adaptive attacks by an untrusted model that knows the protocol and the monitor model.<n>We instantiate a simple adaptive attack vector by which the attacker embeds publicly known or zero-shot prompt injections in the model outputs.
  arXiv  Detail & Related papers  (2025-10-10T15:12:44Z)
• Cuckoo Attack: Stealthy and Persistent Attacks Against AI-IDE [64.47951172662745]
  Cuckoo Attack is a novel attack that achieves stealthy and persistent command execution by embedding malicious payloads into configuration files.<n>We formalize our attack paradigm into two stages, including initial infection and persistence.<n>We contribute seven actionable checkpoints for vendors to evaluate their product security.
  arXiv  Detail & Related papers  (2025-09-19T04:10:52Z)
• Zero-Trust Artificial Intelligence Model Security Based on Moving Target Defense and Content Disarm and Reconstruction [4.0208298639821525]
  This paper examines the challenges in distributing AI models through model zoos and file transfer mechanisms. The physical security of model files is critical, requiring stringent access controls and attack prevention solutions. It demonstrates a 100% disarm rate while validated against known AI model repositories and actual malware attacks from the HuggingFace model zoo.
  arXiv  Detail & Related papers  (2025-03-03T17:32:19Z)
• Cross-Model Transferability of Adversarial Patches in Real-time Segmentation for Autonomous Driving [0.2120527246868857]
  Adrial attacks pose a significant threat to deep learning models, particularly in safety-critical applications like healthcare and autonomous driving. Recently, patch based attacks have demonstrated effectiveness in real-time inference scenarios owing to their 'drag and drop' nature. Here we propose a novel Expectation Over Transformation (EOT) based adversarial patch attack that is more realistic for autonomous vehicles.
  arXiv  Detail & Related papers  (2025-02-22T00:03:53Z)
• Jailbreaking? One Step Is Enough! [6.142918017301964]
  Large language models (LLMs) excel in various tasks but remain vulnerable to jailbreak attacks, where adversaries manipulate prompts to generate harmful outputs. We propose a Reverse Embedded Defense Attack (REDA) mechanism that disguises the attack intention as the "defense" intention. To enhance the model's confidence and guidance in "defensive" intentions, we adopt in-context learning (ICL) with a small number of attack examples.
  arXiv  Detail & Related papers  (2024-12-17T07:33:41Z)
• Exploiting the Vulnerability of Large Language Models via Defense-Aware Architectural Backdoor [0.24335447922683692]
  We introduce a new type of backdoor attack that conceals itself within the underlying model architecture. The add-on modules of model architecture layers can detect the presence of input trigger tokens and modify layer weights. We conduct extensive experiments to evaluate our attack methods using two model architecture settings on five different large language datasets.
  arXiv  Detail & Related papers  (2024-09-03T14:54:16Z)
• EmInspector: Combating Backdoor Attacks in Federated Self-Supervised Learning Through Embedding Inspection [53.25863925815954]
  Federated self-supervised learning (FSSL) has emerged as a promising paradigm that enables the exploitation of clients' vast amounts of unlabeled data. While FSSL offers advantages, its susceptibility to backdoor attacks has not been investigated. We propose the Embedding Inspector (EmInspector) that detects malicious clients by inspecting the embedding space of local models.
  arXiv  Detail & Related papers  (2024-05-21T06:14:49Z)
• Query-Based Adversarial Prompt Generation [67.238873588125]
  We build adversarial examples that cause an aligned language model to emit harmful strings. We validate our attack on GPT-3.5 and OpenAI's safety classifier.
  arXiv  Detail & Related papers  (2024-02-19T18:01:36Z)
• Model Supply Chain Poisoning: Backdooring Pre-trained Models via Embedding Indistinguishability [61.549465258257115]
  We propose a novel and severer backdoor attack, TransTroj, which enables the backdoors embedded in PTMs to efficiently transfer in the model supply chain. Experimental results show that our method significantly outperforms SOTA task-agnostic backdoor attacks.
  arXiv  Detail & Related papers  (2024-01-29T04:35:48Z)
• Mitigating Adversarial Attacks in Federated Learning with Trusted Execution Environments [1.8240624028534085]
  In image-based applications, adversarial examples consist of images slightly perturbed to the human eye getting misclassified by the local model. Pelta is a novel shielding mechanism leveraging Trusted Execution Environments (TEEs) that reduce the ability of attackers to craft adversarial samples. We show the effectiveness of Pelta in mitigating six white-box state-of-the-art adversarial attacks.
  arXiv  Detail & Related papers  (2023-09-13T14:19:29Z)
• One-bit Flip is All You Need: When Bit-flip Attack Meets Model Training [54.622474306336635]
  A new weight modification attack called bit flip attack (BFA) was proposed, which exploits memory fault inject techniques. We propose a training-assisted bit flip attack, in which the adversary is involved in the training stage to build a high-risk model to release.
  arXiv  Detail & Related papers  (2023-08-12T09:34:43Z)
• Your Attack Is Too DUMB: Formalizing Attacker Scenarios for Adversarial Transferability [17.899587145780817]
  Evasion attacks are a threat to machine learning models, where adversaries attempt to affect classifiers by injecting malicious samples. We propose the DUMB attacker model, which allows analyzing if evasion attacks fail to transfer when the training conditions of surrogate and victim models differ. Our analysis, which generated 13K tests over 14 distinct attacks, led to numerous novel findings in the scope of transferable attacks with surrogate models.
  arXiv  Detail & Related papers  (2023-06-27T10:21:27Z)
• DRSM: De-Randomized Smoothing on Malware Classifier Providing Certified Robustness [58.23214712926585]
  We develop a certified defense, DRSM (De-Randomized Smoothed MalConv), by redesigning the de-randomized smoothing technique for the domain of malware detection. Specifically, we propose a window ablation scheme to provably limit the impact of adversarial bytes while maximally preserving local structures of the executables. We are the first to offer certified robustness in the realm of static detection of malware executables.
  arXiv  Detail & Related papers  (2023-03-20T17:25:22Z)
• Omni: Automated Ensemble with Unexpected Models against Adversarial Evasion Attack [35.0689225703137]
  A machine learning-based security detection model is susceptible to adversarial evasion attacks. We propose an approach called Omni to explore methods that create an ensemble of "unexpected models" In studies with five types of adversarial evasion attacks, we show Omni is a promising approach as a defense strategy.
  arXiv  Detail & Related papers  (2020-11-23T20:02:40Z)
• Dispelling Myths on Superposition Attacks: Formal Security Model and Attack Analyses [0.0]
  We propose the first computational security model considering superposition attacks for multiparty protocols. We show that our new security model is satisfiable by proving the security of the well-known One-Time-Pad protocol. We use this newly imparted knowledge to construct the first concrete protocol for Secure Two-Party Computation that is resistant to superposition attacks.
  arXiv  Detail & Related papers  (2020-07-01T18:00:54Z)
• A Self-supervised Approach for Adversarial Robustness [105.88250594033053]
  Adversarial examples can cause catastrophic mistakes in Deep Neural Network (DNNs) based vision systems. This paper proposes a self-supervised adversarial training mechanism in the input space. It provides significant robustness against the textbfunseen adversarial attacks.
  arXiv  Detail & Related papers  (2020-06-08T20:42:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.