論文の概要: Protocols to Code: Formal Verification of a Next-Generation Internet Router

• arxiv url: http://arxiv.org/abs/2405.06074v1
• Date: Thu, 9 May 2024 19:57:59 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-13 17:16:40.257269
• Title: Protocols to Code: Formal Verification of a Next-Generation Internet Router
• Title（参考訳）: コーディングプロトコル:次世代インターネットルータの形式検証
• Authors: João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, Adrian Perrig,
• Abstract要約: SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
• 参考スコア（独自算出の注目度）: 9.971817718196997
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.
• Abstract（参考訳）: SCIONのインターネットアーキテクチャの一部である,初の公式なインターネットルータを提示する。 SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 より正確には、Isabelle/HOLの改良による一連のプロトコルモデルを開発し、我々は、ルータのGoコードがメモリ安全性、クラッシュの自由、データ競合からの自由を満足し、プロトコルモデルに準拠していることを証明するために、自動プログラム検証器を使用する。 どちらの検証も、しっかりと結びついている。 我々の研究は、ハイレベルなプロトコルモデルから独立チームが開発したパフォーマンス最適化プロダクションコードまで、重要なネットワークコンポーネントをコヒーレントに検証する可能性を示している。 その過程で、コード開発者が確認したプロトコルとその実装の重大なバグを発見し、プロトコルのセキュリティ特性を強化した。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装,継続的な変更の処理,採用する検証技術とツールに関する教訓を抽出する。

関連論文リスト

• On the Design and Security of Collective Remote Attestation Protocols [5.01030444913319]
  Collective Remote Attestation (CRA)は、(異種)ネットワークにおいて、侵入されたデバイスを効率的に識別することを目的としたセキュリティサービスである。 ここ数年、CRAプロトコルの提案が大幅に増加し、様々なネットワークトポロジによってガイドされた様々な設計が示されている。 CRAプロトコルを体系的に比較可能な統合フレームワークであるCatを提示する。
  論文  参考訳（メタデータ） (2024-07-12T12:06:49Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Ejafa_protocol: A custom INC secure protocol [0.0]
  このプロトコルには、鍵交換用のX25519や暗号化用のChaCha20など、現代の暗号プリミティブが含まれている。 プロトコルの重要な特徴は、セキュリティを犠牲にすることなく、リソース制限された環境への適応性である。
  論文  参考訳（メタデータ） (2024-01-05T12:51:19Z)
• A General Verification Framework for Dynamical and Control Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Practical quantum secure direct communication with squeezed states [55.41644538483948]
  CV-QSDCシステムの最初の実験実験を行い,その安全性について報告する。 この実現は、将来的な脅威のない量子大都市圏ネットワークへの道を歩み、既存の高度な波長分割多重化(WDM)システムと互換性がある。
  論文  参考訳（メタデータ） (2023-06-25T19:23:42Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)
• Byzantine-Robust Federated Learning with Optimal Statistical Rates and Privacy Guarantees [123.0401978870009]
  ほぼ最適な統計率を持つビザンチン・ロバスト・フェデレーション学習プロトコルを提案する。 競合プロトコルに対してベンチマークを行い、提案プロトコルの実証的な優位性を示す。 我々のバケットプロトコルは、プライバシー保証手順と自然に組み合わせて、半正直なサーバに対するセキュリティを導入することができる。
  論文  参考訳（メタデータ） (2022-05-24T04:03:07Z)
• Online Distributed Evolutionary Optimization of Time Division Multiple Access Protocols [4.87717454493713]
  我々は,環境駆動型分散ヒルクライミングアルゴリズムによって得られたネットワークの創発特性としてプロトコルを想定する。 エネルギー消費とプロトコル性能の観点から,分散ヒルクライミングがさまざまなトレードオフに達することを示す。
  論文  参考訳（メタデータ） (2022-04-27T20:47:48Z)
• Decoder Fusion RNN: Context and Interaction Aware Decoders for Trajectory Prediction [53.473846742702854]
  本稿では,動き予測のための反復的,注意に基づくアプローチを提案する。 Decoder Fusion RNN (DF-RNN) は、リカレント動作エンコーダ、エージェント間マルチヘッドアテンションモジュール、コンテキスト認識デコーダで構成される。 提案手法の有効性をArgoverseモーション予測データセットで検証し,その性能を公開ベンチマークで示す。
  論文  参考訳（メタデータ） (2021-08-12T15:53:37Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。 我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。 ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
  論文  参考訳（メタデータ） (2021-06-03T16:45:40Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。