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

要約

5G ワイヤレス通信プロトコルの正式な手法に基づく分析は、論理的な脆弱性を特定し、特に設計段階で包括的なセキュリティ評価を促進するために重要です。
自然言語処理 (NLP) 支援技術とツールのほとんどは、業界や研究コミュニティに広く採用されていません。
数学的アプローチによる従来の形式的な検証は、手動の論理抽象化に大きく依存しており、時間がかかり、エラーが発生しやすい傾向がありました。
NLP 支援手法が産業研究に適用されなかった理由は、プロトコル設計の自然言語のあいまいさが原因である可能性がありますが、形式的検証の明示性に関しては議論の余地があります。
自然言語で記述された 3GPP (targeting) プロトコルを対象としたプロトコル設計における形式的手法の採用という課題に対処するために、この研究では、プロトコルの分析を合理化するハイブリッド アプローチを提案します。
最初に NLP ツールを使用してデータを構築し、次に構築されたデータを使用して NLP モデルを使用して識別子と形式的プロパティを抽出する 2 段階のパイプラインを導入します。
識別子と形式的プロパティはさらに形式的な分析に使用されます。
識別子と形式的プロパティ間の異なる依存関係を基準とする 3 つのモデルを実装しました。
最適モデルの結果は、識別子の抽出については 39%、形式的プロパティの予測については 42% の有効精度に達しました。
私たちの研究は、特に 5G および NextG 通信における大規模で複雑な仕様およびプロトコル分析の形式分析を実行する効率的な手順の概念実証です。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google