論文の概要: Towards a Formal Verification of Secure Vehicle Software Updates
- arxiv url: http://arxiv.org/abs/2511.15479v1
- Date: Wed, 19 Nov 2025 14:35:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-20 15:51:28.848167
- Title: Towards a Formal Verification of Secure Vehicle Software Updates
- Title（参考訳）: 安全車両ソフトウェアアップデートの形式的検証に向けて
- Authors: Martin Slind Hagen, Emil Lundqvist, Alex Phu, Yenan Wang, Kim Strandberg, Elad Michael Schiller,
- Abstract要約: ソフトウェアの脆弱性は、安全性、経済、社会に深刻な影響を与える可能性がある。
UniSUFは、既存の車両インフラとシームレスに統合するセキュアな更新フレームワークを提供するように設計されている。
我々は,UniSUFの必須セキュリティ要件への準拠を正式に検証するProVerifベースのフレームワークを開発する。
- 参考スコア（独自算出の注目度）: 6.180132192004852
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: With the rise of software-defined vehicles (SDVs), where software governs most vehicle functions alongside enhanced connectivity, the need for secure software updates has become increasingly critical. Software vulnerabilities can severely impact safety, the economy, and society. In response to this challenge, Strandberg et al. [escar Europe, 2021] introduced the Unified Software Update Framework (UniSUF), designed to provide a secure update framework that integrates seamlessly with existing vehicular infrastructures. Although UniSUF has previously been evaluated regarding cybersecurity, these assessments have not employed formal verification methods. To bridge this gap, we perform a formal security analysis of UniSUF. We model UniSUF's architecture and assumptions to reflect real-world automotive systems and develop a ProVerif-based framework that formally verifies UniSUF's compliance with essential security requirements - confidentiality, integrity, authenticity, freshness, order, and liveness - demonstrating their satisfiability through symbolic execution. Our results demonstrate that UniSUF adheres to the specified security guarantees, ensuring the correctness and reliability of its security framework.
- Abstract（参考訳）: ソフトウェア定義車両(SDV)の台頭により、ソフトウェアは接続性の向上とともにほとんどの車両機能を統制するようになり、セキュアなソフトウェアアップデートの必要性がますます重要になっている。
ソフトウェアの脆弱性は、安全性、経済、社会に深刻な影響を与える可能性がある。
この課題に応えて、Strandberg氏らは(ヨーロッパ、2021年)、既存の車両インフラとシームレスに統合するセキュアなアップデートフレームワークを提供するために設計されたUnified Software Update Framework(UniSUF)を導入した。
UniSUFはこれまで、サイバーセキュリティに関して評価されてきたが、これらの評価は正式な検証方法を採用していない。
このギャップを埋めるために、我々はUniSUFの正式なセキュリティ分析を行う。
我々は、UniSUFのアーキテクチャと仮定をモデル化し、現実世界の自動車システムを反映し、UniSUFの秘密性、完全性、真正性、新鮮性、秩序、生活性といった重要なセキュリティ要件に対するコンプライアンスを正式に検証するProVerifベースのフレームワークを開発する。
以上の結果から,UniSUFはセキュリティ保証を遵守し,セキュリティフレームワークの正しさと信頼性を保証する。
関連論文リスト
- Securing Generative AI in Healthcare: A Zero-Trust Architecture Powered by Confidential Computing on Google Cloud [0.0]
Confidential Zero-Trust Framework (CZF) は、Zero-Trust ArchitectureとConfidential Computingのハードウェア強化データアイソレーションを組み合わせたセキュリティパラダイムである。
CZFは、ハードウェアベースのTrusted Execution Environment内で使用中にデータが暗号化される詳細なアーキテクチャを提供する。
論文 参考訳（メタデータ） (2025-11-14T19:56:52Z) - Zero Trust Security Model Implementation in Microservices Architectures Using Identity Federation [0.0]
記事自体は、マイクロサービスエコシステムのゼロトラストセキュリティモデルの必要性に関するケースである。
ソリューションフレームワークは,業界標準の認証と認証とエンドツーエンドの信頼識別技術に基づくことが提案されている。
研究結果は、フェデレートされたアイデンティティとZero Trustの基本が組み合わさって、認証と認可に関するルールが保証されるだけでなく、マイクロサービスデプロイメントの最新のDevSecOps標準に完全に準拠する、というオーバーレイの結果だ。
論文 参考訳（メタデータ） (2025-11-07T02:03:05Z) - Bridging the Mobile Trust Gap: A Zero Trust Framework for Consumer-Facing Applications [51.56484100374058]
本稿では,信頼できないユーザ制御環境で動作するモバイルアプリケーションを対象としたZero Trustモデルを提案する。
デザインサイエンスの方法論を用いて、この研究は、実行時の信頼の強制をサポートする6つのピラーフレームワークを導入した。
提案したモデルは,デプロイ前コントロールを越えてモバイルアプリケーションをセキュアにするための,実用的で標準に準拠したアプローチを提供する。
論文 参考訳（メタデータ） (2025-08-20T18:42:36Z) - Zero-Trust Foundation Models: A New Paradigm for Secure and Collaborative Artificial Intelligence for Internet of Things [61.43014629640404]
Zero-Trust Foundation Models (ZTFM)は、ゼロトラストセキュリティの原則をIoT(Internet of Things)システムの基盤モデル(FM)のライフサイクルに組み込む。
ZTFMは、分散、異質、潜在的に敵対的なIoT環境にわたって、セキュアでプライバシ保護のAIを可能にする。
論文 参考訳（メタデータ） (2025-05-26T06:44:31Z) - SafeAgent: Safeguarding LLM Agents via an Automated Risk Simulator [77.86600052899156]
LLM(Large Language Model)ベースのエージェントは、現実のアプリケーションにますますデプロイされる。
完全自動合成データ生成によるエージェント安全性を体系的に向上する最初のフレームワークであるAutoSafeを提案する。
AutoSafeは安全性のスコアを平均で45%向上させ、現実世界のタスクでは28.91%の改善を実現している。
論文 参考訳（メタデータ） (2025-05-23T10:56:06Z) - AISafetyLab: A Comprehensive Framework for AI Safety Evaluation and Improvement [73.0700818105842]
我々は、AI安全のための代表的攻撃、防衛、評価方法論を統合する統合されたフレームワークとツールキットであるAISafetyLabを紹介する。
AISafetyLabには直感的なインターフェースがあり、開発者はシームレスにさまざまなテクニックを適用できる。
我々はヴィクナに関する実証的研究を行い、異なる攻撃戦略と防衛戦略を分析し、それらの比較効果に関する貴重な洞察を提供する。
論文 参考訳（メタデータ） (2025-02-24T02:11:52Z) - VMGuard: Reputation-Based Incentive Mechanism for Poisoning Attack Detection in Vehicular Metaverse [52.57251742991769]
車両メタバースガード(VMGuard)は、車両メタバースシステムをデータ中毒攻撃から保護する。
VMGuardは、参加するSIoTデバイスの信頼性を評価するために、評判に基づくインセンティブメカニズムを実装している。
当社のシステムは,従来は誤分類されていた信頼性の高いSIoTデバイスが,今後の市場ラウンドへの参加を禁止していないことを保証します。
論文 参考訳（メタデータ） (2024-12-05T17:08:20Z) - Securing Federated Learning with Control-Flow Attestation: A Novel Framework for Enhanced Integrity and Resilience against Adversarial Attacks [2.28438857884398]
分散機械学習パラダイムとしてのフェデレートラーニング(FL)は、新たなサイバーセキュリティ課題を導入した。
本研究では,従来サイバーセキュリティに用いられてきた制御フロー(CFA)機構にインスパイアされた,革新的なセキュリティフレームワークを提案する。
我々は、ネットワーク全体にわたるモデル更新の完全性を認証し、検証し、モデル中毒や敵対的干渉に関連するリスクを効果的に軽減する。
論文 参考訳（メタデータ） (2024-03-15T04:03:34Z) - SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection with LLMs? [3.566250952750758]
SecureFalconは、Falcon-40Bモデルから派生した1億1100万のパラメータしか持たない革新的なモデルアーキテクチャである。
SecureFalconはバイナリ分類で94%の精度、マルチクラス化で最大92%、即時CPU推論時間を実現している。
論文 参考訳（メタデータ） (2023-07-13T08:34:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。