論文の概要: Segment-Based Formal Verification of WiFi Fragmentation and Power Save Mode
- arxiv url: http://arxiv.org/abs/2312.07877v2
- Date: Sat, 16 Dec 2023 22:56:08 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-18 12:26:52.779266
- Title: Segment-Based Formal Verification of WiFi Fragmentation and Power Save Mode
- Title（参考訳）: WiFiフラグメンテーションと省電力モードのセグメントベース形式検証
- Authors: Zilin Shen, Imtiaz Karim, Elisa Bertino,
- Abstract要約: IEEE 802.11ファミリ(英: IEEE 802.11 family of standards)は、何十億ものユーザーが広く使用しているプロトコルである。
WiFiの形式的検証に関するこれまでの研究は、主に4方向ハンドシェイクやその他のセキュリティ面に重点を置いていた。
WiFiプロトコルの機能的側面を推論できる形式的解析手法は存在しない。
- 参考スコア（独自算出の注目度）: 12.534466199973316
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The IEEE 802.11 family of standards, better known as WiFi, is a widely used protocol utilized by billions of users. Previous works on WiFi formal verification have mostly focused on the four-way handshake and other security aspects. However, recent works have uncovered severe vulnerabilities in functional aspects of WiFi, which can cause information leakage for billions of devices. No formal analysis method exists able to reason on the functional aspects of the WiFi protocol. In this paper, we take the first steps in addressing this gap and present an extensive formal analysis of the functional aspects of the WiFi protocol, more specifically, the fragmentation and the power-save-mode process. To achieve this, we design a novel segment-based formal verification process and introduce a practical threat model (i.e. MAC spoofing) in Tamarin to reason about the various capabilities of the attacker. To this end, we verify 68 properties extracted from WiFi protocol specification, find 3 vulnerabilities from the verification, verify 3 known attacks, and discover 2 new issues. These vulnerabilities and issues affect 14 commercial devices out of 17 tested cases, showing the prevalence and impact of the issues. Apart from this, we show that the proposed countermeasures indeed are sufficient to address the issues. We hope our results and analysis will help vendors adopt the countermeasures and motivate further research into the verification of the functional aspects of the WiFi protocol.
- Abstract（参考訳）: IEEE 802.11ファミリ(英: IEEE 802.11 family of standards)は、何十億ものユーザーが広く使用しているプロトコルである。
WiFiの形式的検証に関するこれまでの研究は、主に4方向ハンドシェイクやその他のセキュリティ面に重点を置いていた。
しかし、最近の研究でWiFiの機能面で深刻な脆弱性が発見され、何十億ものデバイスに情報漏洩を引き起こす可能性がある。
WiFiプロトコルの機能的側面を推論できる形式的解析手法は存在しない。
本稿では,このギャップに対処する第一歩として,WiFiプロトコルの機能的側面,具体的にはフラグメンテーションと省電力モードプロセスの広範な形式的解析について述べる。
そこで本研究では,新たなセグメントベース形式検証プロセスを設計し,タマリンにおける攻撃者の多様な能力の解明を目的とした実用的脅威モデル(MACスプーフィング)を導入する。
この目的のために、WiFiプロトコル仕様から抽出された68のプロパティを検証し、検証から3つの脆弱性を発見し、3つの既知の攻撃を検証し、2つの新しい問題を発見する。
これらの脆弱性と問題は17の試験ケースのうち14の商用デバイスに影響を与える。
これとは別に,提案した対策が問題に対処するのに十分であることを示す。
弊社の結果と分析は、ベンダーが対策を取り入れ、WiFiプロトコルの機能的側面の検証に関するさらなる研究を動機付けることを願っている。
関連論文リスト
- Excavating Vulnerabilities Lurking in Multi-Factor Authentication Protocols: A Systematic Security Analysis [2.729532849571912]
単一要素認証(SFA)プロトコルは、しばしばサイドチャネルや他の攻撃技術によってバイパスされる。
この問題を軽減するため,近年,MFAプロトコルが広く採用されている。
論文 参考訳（メタデータ） (2024-07-29T23:37:38Z) - CellularLint: A Systematic Approach to Identify Inconsistent Behavior in Cellular Network Specifications [12.370608043864944]
4G と 5G の標準内での不整合検出のための半自動フレームワークを導入する。
提案手法は,ドメイン適応型大規模言語モデルに対して,改良された数ショット学習機構を用いる。
調査では,Non-Access Stratum (NAS)と4Gおよび5Gネットワークのセキュリティ仕様に注目し,最終的に82.67%の精度で157の矛盾を発見した。
論文 参考訳（メタデータ） (2024-07-18T17:48:46Z) - DeFiTail: DeFi Protocol Inspection through Cross-Contract Execution Analysis [4.891180928768215]
DeFi(Decentralized Finance)プロトコルは、ブロックチェーン上に開発された暗号通貨で、デジタル資産を管理する。
本稿では,DeFiTailを提案する。DeFiTailは,ディープラーニングを利用してアクセス制御とフラッシュローンのエクスプロイトを検出する最初のフレームワークである。
DeFiTailは98.39%のアクセス制御、97.43%のフラッシュローンのエクスプロイトを達成している。
論文 参考訳（メタデータ） (2024-05-17T18:14:19Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - Tamper-Evident Pairing [55.2480439325792]
Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。
TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。
本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
論文 参考訳（メタデータ） (2023-11-24T18:54:00Z) - Empirical Review of Smart Contract and DeFi Security: Vulnerability
Detection and Automated Repair [36.46679501556185]
分散ファイナンス(DeFi)はピアツーピア金融エコシステムとして台頭している。
スマートコントラクトには 膨大な価値があります 攻撃の魅力的なターゲットになります
本稿では,脆弱性検出と自動修復の観点から,スマートコントラクトとDeFiセキュリティの分野における進歩を概観する。
論文 参考訳（メタデータ） (2023-09-05T17:00:42Z) - An anomaly detection approach for backdoored neural networks: face
recognition as a case study [77.92020418343022]
本稿では,異常検出の原理に基づく新しいバックドアネットワーク検出手法を提案する。
バックドアネットワークの新たなデータセット上で本手法を検証し,完全スコアで検出可能性について報告する。
論文 参考訳（メタデータ） (2022-08-22T12:14:13Z) - GraSens: A Gabor Residual Anti-aliasing Sensing Framework for Action
Recognition using WiFi [52.530330427538885]
WiFiベースのヒューマンアクション認識(HAR)は、スマートリビングやリモート監視といったアプリケーションにおいて、有望なソリューションと見なされている。
本稿では,無線機器からのWiFi信号を用いた動作を,多様なシナリオで直接認識する,エンド・ツー・エンドのGabor残差検知ネットワーク(GraSens)を提案する。
論文 参考訳（メタデータ） (2022-05-24T10:20:16Z) - Backdoor Attack against Speaker Verification [86.43395230456339]
学習データを汚染することにより,話者検証モデルに隠れたバックドアを注入できることを示す。
また,既存のバックドア攻撃が話者認証攻撃に直接適用できないことも実証した。
論文 参考訳（メタデータ） (2020-10-22T11:10:08Z) - The Dark (and Bright) Side of IoT: Attacks and Countermeasures for
Identifying Smart Home Devices and Services [4.568911586155096]
3つの一般的なIoTスマートホームデバイスを特徴付けるトラフィックパターンを記述するモデルを構築した。
上記のデバイスによって動作しているサービスと、その存在の圧倒的な確率で検出および識別することが可能であることを実証する。
論文 参考訳（メタデータ） (2020-09-16T13:28:59Z) - Mind the GAP: Security & Privacy Risks of Contact Tracing Apps [75.7995398006171]
GoogleとAppleは共同で,Bluetooth Low Energyを使用した分散型コントラクトトレースアプリを実装するための公開通知APIを提供している。
実世界のシナリオでは、GAP設計は(i)プロファイリングに脆弱で、(ii)偽の連絡先を生成できるリレーベースのワームホール攻撃に弱いことを実証する。
論文 参考訳（メタデータ） (2020-06-10T16:05:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。