5G Specifications Formal Verification with Over-the-Air Validation: Prompting is All You Need

The critical role of 5G and other complex systems in infrastructure necessitates rigorous protocol verification and system validation to ensure security and reliability. This paper explores the application of applying Large Language Model enabled auto Formal Verification with Real-world Prompting on Large Language Models (LLMs) for 5G and NextG protocols, addressing ambiguities and security concerns in network infrastructure protocol and specification design. By leveraging generative transformer-based LLMs, we present a formal approach to prompt engineering that validates complex specifications and implements formal verification techniques to detect and eliminate hallucinations. Our approach is agnostic to specific LLMs, with performance comparisons across currently popular models. We thoroughly examine the human processes involved to identify entry points where Prompt Engineering can reduce process overhead. We have developed a novel framework for iterative prompting and self-monitoring to aid in formal verification using 5G reasoner, enabling closed-loop automatic 5G protocol verification. Focusing on the RRC layer of 5G release 17, specifically sections 5.3.3.3, 5.3.3.4, and 5.3.5.3, we examined the liveness properties and detected a total of seven vulnerabilities, including variations of Null Cipher, Denial of Service (DoS), Lullaby, and Incarceration attacks. Further, we established a general testing framework that spans conception, virtualization, and over-the-air testing, providing a holistic approach to security assessment. This comprehensive framework underscores the importance of robust protocol verification and system validation in the deployment of critical infrastructure technologies.