Formal and Fuzzing Amplification: Targeting Vulnerability Detection in 5G and Beyond

TL;DR

This paper introduces a hybrid framework combining formal verification and fuzz testing to efficiently identify vulnerabilities in 5G protocols, specifically targeting the RRC connection process, and demonstrates its effectiveness with real-world results.

Contribution

The paper presents a novel hierarchical framework that integrates formal methods and fuzzing to enhance vulnerability detection in 5G systems, addressing scalability challenges.

Findings

Identified 53 vulnerabilities in 5G RRC protocols.

Established 1 attack model for protocol security.

Demonstrated improved detection coverage through combined methods.

Abstract

Softwarization and virtualization in 5G and beyond require rigorous testing against vulnerabilities and unintended emergent behaviors for critical infrastructure and network security assurance. Formal methods operates efficiently in protocol-level abstract specification models, and fuzz testing offers comprehensive experimental evaluation of system implementations. In this paper, we propose a novel framework that leverages the respective advantages and coverage of both formal and fuzzing methods to efficiently detect vulnerabilities from protocol logic to implementation stacks hierarchically. The detected attack traces from the formal verification results in critical protocols guide the case generation of fuzz testing, and the feedbacks from fuzz testing further broaden the scope of the formal verification. We examine the proposed framework with the 5G Non Standard-Alone (NSA) security processes, focusing on the Radio Resource Control (RRC) connection process. We first identify protocol-level vulnerabilities of user credentials via formal methods. Following this, we implement bit-level fuzzing to evaluate potential impacts and risks of integrity-vulnerable identifier variation. Concurrently, we conduct command-level mutation-based fuzzing by fixing the assumption identifier to assess the potential impacts and risks of confidentiality-vulnerable identifiers. During this approach, we established 1 attack model and detected 53 vulnerabilities. The vulnerabilities identified used to fortify protocol-level assumptions could further refine search space for the following detection cycles. Consequently, it addresses the prevalent scalability challenges in detecting vulnerabilities and unintended emergent behaviors in large-scale systems in 5G and beyond.