論文の概要: Generalized Security-Preserving Refinement for Concurrent Systems

• arxiv url: http://arxiv.org/abs/2511.06862v1
• Date: Mon, 10 Nov 2025 09:06:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-11 21:18:45.176588
• Title: Generalized Security-Preserving Refinement for Concurrent Systems
• Title（参考訳）: コンカレントシステムのための汎用セキュリティ保存リファインメント
• Authors: Huan Sun, David Sanán, Jingyi Wang, Yongwang Zhao, Jun Sun, Wenhai Wang,
• Abstract要約: 本稿では,IFS特性が実装と抽象化の間に保持されていることを証明するための改良型合成手法を提案する。 我々は,セキュリティポリシーの収集に対する2つの非保存ケーススタディを検証するために,我々のアプローチを適用した。
• 参考スコア（独自算出の注目度）: 36.14488865240512
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ensuring compliance with Information Flow Security (IFS) is known to be challenging, especially for concurrent systems with large codebases such as multicore operating system (OS) kernels. Refinement, which verifies that an implementation preserves certain properties of a more abstract specification, is promising for tackling such challenges. However, in terms of refinement-based verification of security properties, existing techniques are still restricted to sequential systems or lack the expressiveness needed to capture complex security policies for concurrent systems. In this work, we present a generalized security-preserving refinement technique, particularly for verifying the IFS of concurrent systems governed by potentially complex security policies. We formalize the IFS properties for concurrent systems and present a refinement-based compositional approach to prove that the generalized security properties (e.g., intransitive noninterference) are preserved between implementation and abstraction. The key intuition enabling such reasoning, compared to previous refinement work, is to establish a step-mapping relation between the implementation and the abstraction, which is sufficient to ensure that every paired step (in the abstraction and the implementation, respectively) is either permitted or prohibited by the security policy. We apply our approach to verify two non-trivial case studies against a collection of security policies. Our proofs are fully mechanized in Isabelle/HOL, during which we identified that two covert channels previously reported in the ARINC 653 single-core standard also exist in the ARINC 653 multicore standard. We subsequently proved the correctness of the revised mechanism, showcasing the effectiveness of our approach.
• Abstract（参考訳）: 情報フローセキュリティ(IFS)への準拠を保証することは、特にマルチコアオペレーティングシステム(OS)カーネルのような大規模なコードベースを持つ並列システムでは難しいことが知られている。 実装がより抽象的な仕様の特定の特性を保存することを検証するRefinementは、このような課題に取り組むことを約束している。 しかし、セキュリティ特性の洗練に基づく検証に関しては、既存の技術はシーケンシャルなシステムに制限されているか、あるいは並列システムの複雑なセキュリティポリシーを捉えるのに必要な表現力が欠如している。 本研究では,セキュリティ保全技術,特に複雑なセキュリティポリシによって管理される並列システムのIFSを検証するために,汎用的なセキュリティ保全技術を提案する。 並列システムのためのIFS特性を形式化し、一般化されたセキュリティ特性(例えば、非推移的非干渉)が実装と抽象化の間に保持されていることを証明するために、改良に基づく構成アプローチを提案する。 このような推論を可能にする重要な直感は、以前の改良作業と比較して、実装と抽象化の間のステップマッピング関係を確立することである。 我々は,セキュリティポリシーの収集に対する2つの非自明なケーススタディを検証するために,我々のアプローチを適用した。 我々の証明はIsabelle/HOLで完全に機械化されており、ARINC 653シングルコア標準で以前に報告された2つの秘密チャネルがARINC 653マルチコア標準にも存在していることを確認した。 その後,提案手法の正しさを証明し,提案手法の有効性を示した。

関連論文リスト

• A Dynamical Systems Framework for Reinforcement Learning Safety and Robustness Verification [1.104960878651584]
  本稿では,学習方針の堅牢性と安全性を検証するための形式的手法の欠如に対処する新しい枠組みを提案する。 動的システム理論からツールを活用することで、システムの振る舞いを管理する隠れた「骨格」として機能するラグランジアンコヒーレント構造(LCS)を特定し視覚化する。 この枠組みは政策行動の包括的かつ解釈可能な評価を提供し、報酬のみに基づいて成功しているように見える政策の重大な欠陥の特定に成功していることを示す。
  論文  参考訳（メタデータ） (2025-08-21T14:00:26Z)
• Beyond Algorithmic Proofs: Towards Implementation-Level Provable Security [1.338174941551702]
  我々は,実世界の攻撃面に対して構造的に検証可能なレジリエンスの観点からセキュリティを定義する新しいパラダイムである,実装レベル確率セキュリティを提案する。 本稿では,ファイル破壊システムであるSEER(Secure and Efficient Encryption-based Erasure via Ransomware)について述べる。
  論文  参考訳（メタデータ） (2025-08-02T01:58:06Z)
• Provably Secure Retrieval-Augmented Generation [7.412110686946628]
  本稿では,RAG(Retrieval-Augmented Generation)システムのための,信頼性の高い最初のフレームワークを提案する。 我々のフレームワークは、検索したコンテンツとベクトル埋め込みの両方の二重保護を保証するために、プレストレージのフル暗号化方式を採用している。
  論文  参考訳（メタデータ） (2025-08-01T21:37:16Z)
• The Alignment Trap: Complexity Barriers [0.0]
  本稿は、AIアライメントは単に難しいだけでなく、基本的な論理的矛盾に基づくものである、と論じる。 私たちは、すべての必要な安全ルールを列挙できないため、マシンラーニングを正確に使用しています。 このパラドックスは、5つの独立した数学的証明によって確認される。
  論文  参考訳（メタデータ） (2025-06-12T02:30:30Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  安全クリティカルな業界における最近のセキュリティインシデントは、適切なメッセージ認証の欠如により、攻撃者が悪意のあるコマンドを注入したり、システムの振る舞いを変更することができることを明らかにした。 これらの欠点は、サイバーセキュリティを強化するために圧力をかける必要性を強調する新しい規制を引き起こしている。 我々は,レガシ産業通信をセキュアにするためのメッセージ認証ソリューションであるACRICを紹介する。
  論文  参考訳（メタデータ） (2024-11-21T18:26:05Z)
• Safe Inputs but Unsafe Output: Benchmarking Cross-modality Safety Alignment of Large Vision-Language Model [73.8765529028288]
  我々は、モダリティ間の安全アライメントを評価するために、セーフインプットとアンセーフアウトプット(SIUO)と呼ばれる新しい安全アライメントの課題を導入する。 この問題を実証的に調査するため,我々はSIUOを作成した。SIUOは,自己修復,違法行為,プライバシー侵害など,9つの重要な安全領域を含むクロスモダリティベンチマークである。 以上の結果から, クローズドおよびオープンソース両方のLVLMの安全性上の重大な脆弱性が明らかとなり, 複雑で現実的なシナリオを確実に解釈し, 応答する上で, 現行モデルが不十分であることが示唆された。
  論文  参考訳（メタデータ） (2024-06-21T16:14:15Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。 問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。 本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
  論文  参考訳（メタデータ） (2024-03-15T17:32:02Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)

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

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