論文の概要: Securing P4 Programs by Information Flow Control
- arxiv url: http://arxiv.org/abs/2505.09221v1
- Date: Wed, 14 May 2025 08:42:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-15 21:44:09.403327
- Title: Securing P4 Programs by Information Flow Control
- Title（参考訳）: 情報フロー制御によるP4プログラムのセキュア化
- Authors: Anoud Alshnakat, Amir M. Ahmadian, Musard Balliu, Roberto Guanciale, Mads Dam,
- Abstract要約: 本稿では,P4プログラムにおける情報フローを解析するための新しいセキュリティ型システムを提案する。
我々は、この型システムを形式化し、それを証明し、適切に型付けされたプログラムが非干渉を満たすことを保証した。
- 参考スコア（独自算出の注目度）: 4.6847954792167
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Software-Defined Networking (SDN) has transformed network architectures by decoupling the control and data-planes, enabling fine-grained control over packet processing and forwarding. P4, a language designed for programming data-plane devices, allows developers to define custom packet processing behaviors directly on programmable network devices. This provides greater control over packet forwarding, inspection, and modification. However, the increased flexibility provided by P4 also brings significant security challenges, particularly in managing sensitive data and preventing information leakage within the data-plane. This paper presents a novel security type system for analyzing information flow in P4 programs that combines security types with interval analysis. The proposed type system allows the specification of security policies in terms of input and output packet bit fields rather than program variables. We formalize this type system and prove it sound, guaranteeing that well-typed programs satisfy noninterference. Our prototype implementation, Tap4s, is evaluated on several use cases, demonstrating its effectiveness in detecting security violations and information leakages.
- Abstract（参考訳）: Software-Defined Networking (SDN)は、制御とデータプレーンを分離することでネットワークアーキテクチャを変換し、パケット処理と転送のきめ細かい制御を可能にする。
データプレーンデバイスをプログラムするために設計された言語であるP4では、開発者はプログラム可能なネットワークデバイス上で、独自のパケット処理動作を定義できる。
これにより、パケット転送、検査、修正の制御がより強化される。
しかしながら、P4が提供する柔軟性の向上は、特に機密データの管理とデータプレーン内の情報漏洩の防止において、セキュリティ上の大きな課題をもたらす。
本稿では、セキュリティタイプとインターバル分析を組み合わせたP4プログラムにおける情報フローを解析するための新しいセキュリティ型システムを提案する。
提案した型システムでは,プログラム変数ではなく,入力および出力パケットビットフィールドのセキュリティポリシを指定できる。
我々は、この型システムを形式化し、それを証明し、適切に型付けされたプログラムが非干渉を満たすことを保証した。
プロトタイプ実装であるTap4sをいくつかのユースケースで評価し,セキュリティ違反や情報漏洩の検出の有効性を実証した。
関連論文リスト
- Output Constraints as Attack Surface: Exploiting Structured Generation to Bypass LLM Safety Mechanisms [0.9091225937132784]
我々は、従来のデータプレーンの脆弱性に対して、重要な制御プレーン攻撃面を明らかにする。
本稿では、構造的出力制約を武器として安全機構をバイパスする新しいジェイルブレイククラスであるConstrained Decoding Attackを紹介する。
本研究は, 現状のLLMアーキテクチャにおける重要なセキュリティ盲点を明らかにし, 制御面脆弱性に対処するため, LLM安全性のパラダイムシフトを促すものである。
論文 参考訳（メタデータ） (2025-03-31T15:08:06Z) - Pareto Control Barrier Function for Inner Safe Set Maximization Under Input Constraints [50.920465513162334]
入力制約下での動的システムの内部安全集合を最大化するPCBFアルゴリズムを提案する。
逆振り子に対するハミルトン・ヤコビの到達性との比較と,12次元四元数系のシミュレーションにより,その有効性を検証する。
その結果,PCBFは既存の手法を一貫して上回り,入力制約下での安全性を確保した。
論文 参考訳（メタデータ） (2024-10-05T18:45:19Z) - P4Control: Line-Rate Cross-Host Attack Prevention via In-Network Information Flow Control Enabled by Programmable Switches and eBPF [14.787290539225245]
P4Controlは、ネットワーク内のエンド・ツー・エンドの情報フローを制限し、ラインレートでのクロスホスト攻撃を防ぐネットワーク防御システムである。
我々は、P4Controlがクロスホスト攻撃を効果的にリアルタイムに防ぐことができることを示すため、広範囲な評価を行う。
論文 参考訳（メタデータ） (2024-05-23T18:19:10Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳（メタデータ） (2024-01-17T00:56:23Z) - Secure Instruction and Data-Level Information Flow Tracking Model for RISC-V [0.0]
不正アクセス、障害注入、およびプライバシー侵害は、信頼できないアクターによる潜在的な脅威である。
本稿では,実行時セキュリティがシステム完全性を保護するために,IFT(Information Flow Tracking)技術を提案する。
本研究では,ハードウェアベース IFT 技術とゲートレベル IFT (GLIFT) 技術を統合したマルチレベル IFT モデルを提案する。
論文 参考訳（メタデータ） (2023-11-17T02:04:07Z) - Towards Formal Verification of a TPM Software Stack [0.5074812070492739]
本稿では,Frama-C 検証プラットフォームを用いた tpm2-ts の形式的検証について述べる。
リンクされたリストと複雑なデータ構造に基づいて、ライブラリのコードは検証ツールにとって非常に難しいように思える。
論文 参考訳（メタデータ） (2023-07-31T16:35:16Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳（メタデータ） (2021-06-03T16:45:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。