Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Discovering and Reproducing Network Protocols Vulnerabilities

Christophe Crochet, John Aoga, Axel Legay

TL;DR

The paper addresses the challenge of proactively discovering vulnerabilities in increasingly complex network protocols and cross-protocol interactions. It proposes Network Attack-centric Compositional Testing (NACT), a model-based mutation framework that extends prior Network-centric Compositional Testing (NCT) with formal-spec mutations, composable attacker models, and randomized constraint solving to generate adversarial testing scenarios. Through MiniP and five QUIC implementations, NACT identifies both known and novel vulnerabilities, including version negotiation abuse and memory-exhaustion exploits, while also enabling detection of regressions across versions. The framework supports black-box testing and multiprotocol scenarios in virtual networks, offering a practical approach to harden protocols for microservice architectures; future work includes integrating NSCT to verify time-dependent properties and expanding empirical evaluations within the AMC3 project.

Abstract

The rapid evolution of cyber threats has increased the need for robust methods to discover vulnerabilities in increasingly complex and diverse network protocols. This paper introduces Network Attack-centric Compositional Testing (NACT), a novel methodology designed to discover new vulnerabilities in network protocols and create scenarios to reproduce these vulnerabilities through attacker models. NACT integrates composable attacker specifications, formal specification mutations, and randomized constraint-solving techniques to generate sophisticated attack scenarios and test cases. The methodology enables comprehensive testing of both single-protocol and multi-protocol interactions. Through case studies involving a custom minimalist protocol (MiniP) and five widely used QUIC implementations, NACT is shown to effectively identify, reproduce, and find new real-world vulnerabilities such as version negotiation abuse. Additionally, by comparing the current and older versions of these QUIC implementations, NACT demonstrates its ability to detect both persistent vulnerabilities and regressions. Finally, by supporting cross-protocol testing within a black-box testing framework, NACT provides a versatile approach to improve the security of network protocols.

Formally Discovering and Reproducing Network Protocols Vulnerabilities

TL;DR

The paper addresses the challenge of proactively discovering vulnerabilities in increasingly complex network protocols and cross-protocol interactions. It proposes Network Attack-centric Compositional Testing (NACT), a model-based mutation framework that extends prior Network-centric Compositional Testing (NCT) with formal-spec mutations, composable attacker models, and randomized constraint solving to generate adversarial testing scenarios. Through MiniP and five QUIC implementations, NACT identifies both known and novel vulnerabilities, including version negotiation abuse and memory-exhaustion exploits, while also enabling detection of regressions across versions. The framework supports black-box testing and multiprotocol scenarios in virtual networks, offering a practical approach to harden protocols for microservice architectures; future work includes integrating NSCT to verify time-dependent properties and expanding empirical evaluations within the AMC3 project.

Abstract

The rapid evolution of cyber threats has increased the need for robust methods to discover vulnerabilities in increasingly complex and diverse network protocols. This paper introduces Network Attack-centric Compositional Testing (NACT), a novel methodology designed to discover new vulnerabilities in network protocols and create scenarios to reproduce these vulnerabilities through attacker models. NACT integrates composable attacker specifications, formal specification mutations, and randomized constraint-solving techniques to generate sophisticated attack scenarios and test cases. The methodology enables comprehensive testing of both single-protocol and multi-protocol interactions. Through case studies involving a custom minimalist protocol (MiniP) and five widely used QUIC implementations, NACT is shown to effectively identify, reproduce, and find new real-world vulnerabilities such as version negotiation abuse. Additionally, by comparing the current and older versions of these QUIC implementations, NACT demonstrates its ability to detect both persistent vulnerabilities and regressions. Finally, by supporting cross-protocol testing within a black-box testing framework, NACT provides a versatile approach to improve the security of network protocols.

Paper Structure

This paper contains 31 sections, 4 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Background
  3. (1) Network Attack Vectors and Agents.
  4. (a) Types of Network Attacks.
  5. (b) Attack Vectors.
  6. (2) Network-Centric Testing Approaches.
  7. NCT Principle.
  8. MiniP.
  9. MiniP Network-centric Structure.
  10. Formal specification.
  11. (3) Network-Centric Testing Limitations.
  12. ① Limited to Specification-Conforming Testing.
  13. ② Single Protocol Testing.
  14. ③ Restricted to Point-To-Point communications.
  15. Putting all together.
  16. ...and 16 more sections

Figures (4)

  • Figure 1: MiniP Network-Centric Testing (NCT) structure
  • Figure 2: MiniP Formal Specification Mutation
  • Figure 3: Virtual networks and NACT
  • Figure 4: System Component