TY - GEN
T1 - From Ambiguity to Explicitness
T2 - 12th IEEE International Conference on Cloud Networking, CloudNet 2023
AU - Yuan, Shiyu
AU - Yang, Jingda
AU - Arya, Sudhanshu
AU - Lipizzi, Carlo
AU - Wang, Ying
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - 5G
KW - formal dependency table
KW - formal property
KW - identifier
KW - language model
KW - NLP
UR - http://www.scopus.com/inward/record.url?scp=85191264159&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85191264159&partnerID=8YFLogxK
U2 - 10.1109/CloudNet59005.2023.10490075
DO - 10.1109/CloudNet59005.2023.10490075
M3 - Conference contribution
AN - SCOPUS:85191264159
T3 - 2023 IEEE 12th International Conference on Cloud Networking, CloudNet 2023
SP - 229
EP - 237
BT - 2023 IEEE 12th International Conference on Cloud Networking, CloudNet 2023
Y2 - 1 November 2023 through 3 November 2023
ER -