論文の概要: 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マルチコア標準にも存在していることを確認した。 その後,提案手法の正しさを証明し,提案手法の有効性を示した。

関連論文リスト

• Kernel-Based Learning of Safety Barriers [0.9367224590861915]
  安全クリティカルなアプリケーションにおけるAIアルゴリズムの迅速な統合は、厳格な安全基準を満たす能力に対する懸念を高めている。 従来の安全検証ツールでは、AI駆動システムのブラックボックスの性質に苦戦している。 離散時間力学を用いたブラックボックスシステムの安全性検証と合成のためのデータ駆動方式を提案する。
  論文  参考訳（メタデータ） (2026-01-17T10:42:35Z)
• Secure Data Bridging in Industry 4.0: An OPC UA Aggregation Approach for Including Insecure Legacy Systems [0.4675863182439614]
  産業ネットワークの接続性の向上は、サイバー攻撃の急増につながった。 OPC UAのような現代産業の4.0技術は、これらの脅威に対して強化されたレジリエンスを提供する。 多くのシステムはこれらの技術をまだ実装していないし、一部しか実装していない。 本稿では,この課題に対処する既存のソリューションについて,そのアプローチ,利点,限界を分析して検討する。
  論文  参考訳（メタデータ） (2026-01-16T01:18:31Z)
• 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)
• Evaluating Model-free Reinforcement Learning toward Safety-critical Tasks [70.76757529955577]
  本稿では、国家安全RLの観点から、この領域における先行研究を再考する。 安全最適化と安全予測を組み合わせた共同手法であるUnrolling Safety Layer (USL)を提案する。 この領域のさらなる研究を容易にするため、我々は関連するアルゴリズムを統一パイプラインで再現し、SafeRL-Kitに組み込む。
  論文  参考訳（メタデータ） (2022-12-12T06:30:17Z)
• Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environments [84.3830478851369]
  本研究では,環境を協調的に学習し,制御ポリシーを最適化する安全な強化学習手法を提案する。 本手法は, 安全性の制約を効果的に適用し, シミュレーションにより測定したシステム安全率においてCMDPベースのベースライン法を著しく上回っている。
  論文  参考訳（メタデータ） (2022-09-29T20:49:25Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Safe Reinforcement Learning via Confidence-Based Filters [78.39359694273575]
  我々は,標準的な強化学習技術を用いて学習した名目政策に対して,国家安全の制約を認定するための制御理論的アプローチを開発する。 我々は、正式な安全保証を提供し、我々のアプローチの有効性を実証的に実証する。
  論文  参考訳（メタデータ） (2022-07-04T11:43:23Z)

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

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