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.
