Hermes: Unlocking Security Analysis of Cellular Network Protocols by Synthesizing Finite State Machines from Natural Language Specifications

要約

この論文では、自然言語のセルラー仕様から形式表現を自動的に生成するエンドツーエンドのフレームワークである Hermes を紹介します。
まず、遷移関連テキストを処理し、遷移コンポーネント (つまり、状態、条件、アクション) を抽出するニューラル構成パーサー NEUTREX を開発します。
また、依存関係解析ツリーを活用して、これらの遷移コンポーネントを論理式に変換するドメイン固有の言語も設計します。
最後に、これらの論理式をコンパイルして遷移を生成し、有限状態マシンとして形式モデルを作成します。
Hermes の有効性を実証するために、4G NAS、5G NAS、および 5G RRC 仕様に基づいて Herme を評価し、81 ～ 87% の全体的な精度が得られました。これは、最先端のものよりも大幅な改善です。
抽出されたモデルのセキュリティ分析により、3 つの新たな脆弱性が明らかになり、4G および 5G 仕様における 19 件の以前の攻撃と、商用 4G ベースバンドにおける 7 件の逸脱が特定されました。

要約(オリジナル)

In this paper, we present Hermes, an end-to-end framework to automatically generate formal representations from natural language cellular specifications. We first develop a neural constituency parser, NEUTREX, to process transition-relevant texts and extract transition components (i.e., states, conditions, and actions). We also design a domain-specific language to translate these transition components to logical formulas by leveraging dependency parse trees. Finally, we compile these logical formulas to generate transitions and create the formal model as finite state machines. To demonstrate the effectiveness of Hermes, we evaluate it on 4G NAS, 5G NAS, and 5G RRC specifications and obtain an overall accuracy of 81-87%, which is a substantial improvement over the state-of-the-art. Our security analysis of the extracted models uncovers 3 new vulnerabilities and identifies 19 previous attacks in 4G and 5G specifications, and 7 deviations in commercial 4G basebands.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google