Softwarization and virtualization in 5G and beyond necessitate thorough testing to ensure the security of critical infrastructure and networks, requiring the identification of vulnerabilities and unintended emergent behaviors from protocol designs to their software stack implementation. To provide an efficient and comprehensive solution, we propose a novel and first-of-its-kind approach that connects the strengths and coverage of formal and fuzzing methods to efficiently detect vulnerabilities across protocol logic and implementation stacks in a hierarchical manner. We design and implement formal verification to detect attack traces in critical protocols, which are used to guide subsequent fuzz testing and incorporate feedback from fuzz testing 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. Following this approach, we discover one identifier leakage model, one DoS attack model, and two eavesdrop attack models due to the absence of rudimentary MITM protection within the protocol, despite the existence of a Transport Layer Security (TLS) solution to this issue for over a decade. More remarkably, guided by the identified formal analysis and attack models, we exploit 61 vulnerabilities using fuzz testing demonstrated 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 united formal and fuzzing methodology enables auto-assurance by systematically discovering vulnerabilities. It significantly reduces computational complexity, transforming the non-practical exponential growth in computational cost into linear growth.

翻译：5G及未来网络的软化和虚拟化要求对关键基础设施和网络进行彻底测试，以发现从协议设计到其软件栈实现中的漏洞和意外涌现行为。为提供高效且全面的解决方案，我们提出了一种新颖且首创的方法，该方法将形式化方法与模糊测试的优势和覆盖范围相结合，以分层方式高效检测协议逻辑和实现栈中的漏洞。我们设计并实现了形式化验证，用于检测关键协议中的攻击轨迹，这些轨迹用于引导后续的模糊测试，并整合模糊测试的反馈以扩大形式化验证的范围。这一创新方法显著提升了效率，并实现了从3GPP协议到软件栈的漏洞与意外涌现行为的自动发现。通过该方法，我们发现了协议因缺乏基本中间人攻击防护而导致的一个标识符泄露模型、一个拒绝服务攻击模型和两个窃听攻击模型——尽管传输层安全（TLS）解决方案已存在十余年。更值得注意的是，在识别出的形式化分析与攻击模型的引导下，我们在srsRAN平台上利用模糊测试挖掘出61个漏洞。这些已识别的漏洞有助于强化协议级假设并优化搜索空间。与现有最先进的模糊测试相比，我们统一的形式化与模糊测试方法通过系统性发现漏洞实现了自动化安全验证。该方法显著降低了计算复杂度，将原本不切实际的指数级计算成本增长转化为线性增长。