Open AccessFormal-Guided Fuzz Testing: Targeting Security Assurance from Specification to Implementation for 5G and Beyond
Author(s) -
Jingda Yang,
Sudhanshu Arya,
Ying Wang
Publication year - 2024
Publication title -
ieee access
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.587
H-Index - 127
ISSN - 2169-3536
DOI - 10.1109/access.2024.3369613
Subject(s) - aerospace , bioengineering , communication, networking and broadcast technologies , components, circuits, devices and systems , computing and processing , engineered materials, dielectrics and plasmas , engineering profession , fields, waves and electromagnetics , general topics for engineers , geoscience , nuclear engineering , photonics and electrooptics , power, energy and industry applications , robotics and control systems , signal processing and analysis , transportation
Softwarization and virtualization in 5G and beyond necessitate thorough testing to ensure the security of critical infrastructure and networks. This involves identifying vulnerabilities and unintended emergent behaviors, from protocol designs to their software stack implementation. Formal methods are efficient in abstracting specification models at the protocol level, while fuzz testing provides comprehensive experimental evaluations of system implementations. However, the state-of-the-art in formal and fuzz testing is both labor-intensive and computationally complex. To provide an efficient and comprehensive solution, we propose a novel, first-of-its-kind approach that combines the strengths and coverage of formal and fuzzing methods. This approach efficiently detects vulnerabilities across protocol logic and implementation stacks in a hierarchical manner. We design and implement formal verification to detect attack traces in critical protocols. These traces then guide subsequent fuzz testing, and feedback from fuzz testing is used to broaden the scope of formal verification. This innovative approach significantly improves efficiency and enables the auto-discovery of vulnerabilities and unintended emergent behaviors from the 3GPP protocols to software stacks. We demonstrate this approach with the 5G Non-Stand-Alone (NSA) security processes, which have more complicated designs and higher risks due to compatibility requirements with legacy and existing 4G networks, compared to 5G Stand-Alone (SA) processes. We focus on the Radio Resource Control (RRC), Non-access Stratum (NAS), and Access Stratum (AS) authentication processes. Guided by the identified formal analysis and attack models, we exploit 61 vulnerabilities, including 2 previously undiscovered ones, and demonstrate these vulnerabilities via fuzz testing on srsRAN platforms. These identified vulnerabilities contribute to fortifying protocol-level assumptions and refining the search space. Compared to state-of-the-art fuzz testing, our unified formal and fuzzing methodology enables auto-assurance by systematically discovering vulnerabilities.