From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis

Formal method-based analysis of the 5G Wireless Communication Protocol is crucial for identifying logical vulnerabilities and facilitating an all-encompassing security assessment. Natural Language Processing (NLP) assisted techniques are not widely adopted by the industry application such as formal analysis. Traditional formal verification through a mathematics approach heavily relied on manual logical abstraction prone to being time-consuming, and error-prone. To address the challenges of incorporating formal methods into protocol designs, especially for 3GPP protocols that are articulated in natural language, we present an NLP-assisted methodology to streamline the analysis of protocols. We introduce a two-step pipeline that first uses NLP tools to construct data and then uses constructed data to extract identifiers and formal properties. The identifiers and formal properties are further used for formal analysis. We implemented three models that take different dependencies between identifiers and formal properties as criteria. Our results of the optimal model reach valid accuracy of 39% for identifier extraction and 42% for formal properties predictions. Considering the complexity and ambiguity inherent in the natural language of protocol designs, the modest result represents a meaningful leap towards automating a traditionally manual process. Our work is proof of concept for an efficient procedure in performing formal analysis for large-scale complicate specification and protocol analysis, especially for 5G and nextG communications. By leveraging NLP-assisted techniques, our method aims to automate the verification process and seeks to bridge the gap between the rigorousness of formal methods and the real-world application of analyzing large-scale and complex industrial documents.