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

Shiyu Yuan, Jingda Yang, Sudhanshu Arya, Carlo Lipizzi, Ying Wang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publication2023 IEEE 12th International Conference on Cloud Networking, CloudNet 2023
Pages229-237
Number of pages9
ISBN (Electronic)9798350313062
DOIs
StatePublished - 2023
Event12th IEEE International Conference on Cloud Networking, CloudNet 2023 - Hoboken, United States
Duration: 1 Nov 20233 Nov 2023

Publication series

Name2023 IEEE 12th International Conference on Cloud Networking, CloudNet 2023

Conference

Conference12th IEEE International Conference on Cloud Networking, CloudNet 2023
Country/TerritoryUnited States
CityHoboken
Period1/11/233/11/23

Keywords

  • 5G
  • formal dependency table
  • formal property
  • identifier
  • language model
  • NLP

Fingerprint

Dive into the research topics of 'From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis'. Together they form a unique fingerprint.

Cite this