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

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.