From Ambiguity to Explicitness: NLP-Assisted 5G Specification
  Abstraction for Formal Analysis
Shiyu Yuan Jingda Yang Sudhanshu Arya Carlo Lipizzi Ying Wang
Formal method-based analysis of the 5G Wireless Communication Protocol is
crucial for identifying logical vulnerabilities and facilitating an
all-encompassing security assessment, especially in the design phase. Natural
Language Processing (NLP) assisted techniques and most of the tools are not
widely adopted by the industry and research community. Traditional formal
verification through a mathematics approach heavily relied on manual logical
abstraction prone to being time-consuming, and error-prone. The reason that the
NLP-assisted method did not apply in industrial research may be due to the
ambiguity in the natural language of the protocol designs nature is
controversial to the explicitness of formal verification. To address the
challenge of adopting the formal methods in protocol designs, targeting (3GPP)
protocols that are written in natural language, in this study, we propose a
hybrid approach 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 by using the NLP
model. 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. Our work is proof of concept for an efficient procedure
in performing formal analysis for largescale complicate specification and
protocol analysis, especially for 5G and nextG communications.