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.

翻译：5G及未来网络的软化和虚拟化要求对关键基础设施和网络安全保障进行严格的漏洞及非预期涌现行为测试。形式化方法在协议级抽象规范模型中高效运行，而模糊测试则提供系统实现的全面实验评估。本文提出一种新型框架，利用形式化方法与模糊测试各自的优势与覆盖范围，从协议逻辑至实现堆栈层次化高效检测漏洞。由关键协议形式化验证结果检测到的攻击轨迹指导模糊测试的用例生成，而模糊测试的反馈则进一步扩展形式化验证的范围。我们以5G非独立组网（NSA）安全流程为对象检验所提框架，重点研究无线资源控制（RRC）连接过程。首先通过形式化方法识别用户凭证的协议级漏洞，随后实施位级模糊测试评估完整性易受攻击的标识符变异的潜在影响与风险；同时通过固定假设标识符进行基于变异的命令级模糊测试，评估机密性易受攻击的标识符的潜在影响与风险。在此过程中，我们建立1个攻击模型并检测到53个漏洞。用于强化协议级假设的已识别漏洞可进一步优化后续检测周期的搜索空间。因此，该方法有效解决了5G及未来网络大规模系统中漏洞与非预期涌现行为检测中普遍存在的可扩展性挑战。