論文の概要: Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security

• arxiv url: http://arxiv.org/abs/2309.09997v1
• Date: Sun, 17 Sep 2023 03:41:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2023-10-23 07:21:52.849375
• Title: Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security
• Title（参考訳）: コンカレントメモリ管理に関する従属者推論--正しさ、安全性、セキュリティ
• Authors: Yongwang Zhao, David Sanan
• Abstract要約: メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。 本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification of concurrent operating systems (OSs) is challenging, in particular the verification of the dynamic memory management due to its complex data structures and allocation algorithm. An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks. This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS concerning a comprehensive set of properties, including functional correctness, safety and security. To achieve the highest assurance evaluation level, we develop a fine-grained formal specification of the Zephyr RTOS buddy memory management, which closely follows the C code easing validation of the specification and the source code. The rely-guarantee-based compositional verification technique has been enforced over the formal model. To support formal verification of the security property, we extend our rely-guarantee framework PiCore by a compositional reasoning approach for integrity. Whilst the security verification of the design shows that it preserves the integrity property, the verification of the functional properties shows several problems. These verification issues are translated into finding three bugs in the C implementation of Zephyr, after inspecting the source code corresponding to the design lines breaking the properties.
• Abstract（参考訳）: 並列オペレーティングシステム(OS)の形式的検証は、特に複雑なデータ構造と割り当てアルゴリズムによる動的メモリ管理の検証が困難である。 メモリ管理の誤った仕様と実装は、システムクラッシュや悪用可能な攻撃につながる可能性がある。 本稿では, 機能的正当性, 安全性, セキュリティなど, 総合的な特性セットに関する, 実世界のOS向け並列メモリ管理の最初の正式な仕様と機構的証明を示す。 最も高い保証評価レベルを達成するために、我々はzephyr rtos buddy memory managementの詳細な形式仕様を開発し、仕様とソースコードの検証を容易にするcコードに密接に従う。 従属保証に基づく構成検証技術は, 形式モデル上で適用されている。 セキュリティ特性の形式的検証を支援するため,信頼度保証フレームワークであるPiCoreを,整合性のための構成的推論アプローチにより拡張する。 設計のセキュリティ検証は完全性を維持することを示しているが、機能特性の検証にはいくつかの問題がある。 これらの検証問題は、プロパティを壊す設計ラインに対応するソースコードを検査した後、ZephyrのC実装で3つのバグを見つけるように変換される。

関連論文リスト

• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。 我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
  論文  参考訳（メタデータ） (2026-01-30T08:29:01Z)
• Proving Circuit Functional Equivalence in Zero Knowledge [4.301822791698451]
  ハードウェア形式検証のための最初のプライバシ保護フレームワークであるZK-CECを提案する。 正式な検証とゼロ知識証明(ZKP)を組み合わせることで、ZK-CECはIPの正当性とセキュリティを正式に検証する基盤を確立する。 ZK- CECは、AES S-Boxのような実用的な設計を実用時間内に検証することに成功した。
  論文  参考訳（メタデータ） (2026-01-16T10:43:30Z)
• Variable Record Table: A Unified Hardware-Assisted Framework for Runtime Security [0.0]
  本稿では,ハードウェア支援フレームワークを統一した可変レコードテーブル(VRT)を提案する。 VRTはバッファオーバーフロー、バックエンド制御フロー整合性(CFI)、投機的実行攻撃検出に対する空間メモリ安全性を強制する。
  論文  参考訳（メタデータ） (2025-12-14T07:04:49Z)
• Memory-Augmented Knowledge Fusion with Safety-Aware Decoding for Domain-Adaptive Question Answering [7.794451415614666]
  ケアシナリオにおけるQAパフォーマンス向上を目的とした新しいフレームワークであるKARMA(Knowled-Aware Reasoning and Memory-Augmented Adaptation)を紹介する。 KARMAには、構造化および非構造化の知識ソースを融合させるデュアルエンコーダアーキテクチャ、外部知識の統合を動的に制御するゲートメモリユニット、安全を意識した制御可能なデコーダが組み込まれている。
  論文  参考訳（メタデータ） (2025-12-02T03:12:14Z)
• BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation [0.0]
  サイバー物理システムは私たちの日常生活において重要な役割を担い、電力や水などの重要なサービスを提供してきた。 従来の脆弱性発見技術は、Cプログラムのバイナリコードに直接適用する場合、スケーラビリティと精度に苦労する。 この研究は、モデルチェックとココリック実行技術を活用することによって、これらの制限を克服するために設計された新しいアプローチを導入している。
  論文  参考訳（メタデータ） (2025-11-24T20:11:41Z)
• Provably Secure Retrieval-Augmented Generation [7.412110686946628]
  本稿では,RAG(Retrieval-Augmented Generation)システムのための,信頼性の高い最初のフレームワークを提案する。 我々のフレームワークは、検索したコンテンツとベクトル埋め込みの両方の二重保護を保証するために、プレストレージのフル暗号化方式を採用している。
  論文  参考訳（メタデータ） (2025-08-01T21:37:16Z)
• DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
  大規模言語モデル(LLM)は、強力な推論と計画能力のため、エージェントシステムの中心となってきています。 この相互作用は、外部ソースからの悪意のある入力がエージェントの振る舞いを誤解させる可能性がある、インジェクション攻撃のリスクも引き起こす。 本稿では,信頼に値するエージェントシステムのための動的ルールベースの分離フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-06-13T05:01:09Z)
• LeakGuard: Detecting Memory Leaks Accurately and Scalably [3.256598917442277]
  LeakGuardは、正確性とスケーラビリティの十分なバランスを提供するメモリリーク検出ツールである。 正確性のために、LeakGuardはライブラリと開発者が定義したメモリ割り当てとトランザクションロケーション関数の挙動を分析する。 スケーラビリティのために、LeakGuardは関数の要約と制約の少ないシンボル実行技術を用いて、興味のある各関数を独立に調べる。
  論文  参考訳（メタデータ） (2025-04-06T09:11:37Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Ownership Verification with Reasoning [58.57194301645823]
  大規模言語モデル (LLM) は、検索強化生成機構 (RAG) を通じて現実のアプリケーションに統合されつつある。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、通常、中毒攻撃を伴う。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• Formal Verification of Permission Voucher [1.4732811715354452]
  Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。 この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。 結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
  論文  参考訳（メタデータ） (2024-12-18T14:11:50Z)
• FRAMER/Miu: Tagged Pointer-based Capability and Fundamental Cost of Memory Safety & Coherence (Position Paper) [0.0]
  研究者はパフォーマンス、検出カバレッジ、相互運用性、精度、検出タイミングのトレードオフを行う。 本研究は,スタンドアロンソフトウェアソリューションと将来のハードウェア設計のためのプロトタイプとして,タグ付きポインタベースの機能システムを提案する。
  論文  参考訳（メタデータ） (2024-08-27T17:31:26Z)
• VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
  CHERIはハードウェアに直接、きめ細かいメモリ保護を提供し、強制する。 VeriCHERIはISA仕様を一切必要としないという点で、従来のものと概念的に異なる。 CHERIの変種を実装したRISC-Vベースのプロセッサ上で,VeriCHERIの有効性とスケーラビリティを示す。
  論文  参考訳（メタデータ） (2024-07-26T11:48:55Z)
• OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
  OpenFactCheckは、カスタマイズされたファクトチェックシステムを構築するためのフレームワークである。 ユーザーは自動的にファクトチェッカーをカスタマイズし、文書やクレームの事実的正当性を検証できる。 CheckerEVALは、人間の注釈付きデータセットを使用して、自動ファクトチェッカーの検証結果の信頼性を高めるソリューションである。
  論文  参考訳（メタデータ） (2024-05-09T07:15:19Z)
• Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications [0.0]
  この記事では、CRSの正式な仕様と検証のための依存型推論フレームワークであるPiCoreを提案する。 我々は、複雑な反応構造をサポートするイベント仕様言語を設計し、イベントの振る舞いからCRSのリアクティブな側面の仕様とロジックを分離する。 この設計により、仕様や証明の変更なしに既存の2つの言語とそれらの信頼保証証明システムを統合することに成功した。
  論文  参考訳（メタデータ） (2023-09-17T03:43:25Z)
• Towards Formal Verification of a TPM Software Stack [0.5074812070492739]
  本稿では,Frama-C 検証プラットフォームを用いた tpm2-ts の形式的検証について述べる。 リンクされたリストと複雑なデータ構造に基づいて、ライブラリのコードは検証ツールにとって非常に難しいように思える。
  論文  参考訳（メタデータ） (2023-07-31T16:35:16Z)
• A Novel Approach to Identify Security Controls in Source Code [4.598579706242066]
  本稿では,一般的なセキュリティ制御の包括的リストを列挙し,それぞれにデータセットを作成する。 最新のNLP技術であるBERT(Bidirectional Representations from Transformers)とTactic Detector(Tactic Detector)を使って、セキュリティコントロールを高い信頼性で識別できることを示しています。
  論文  参考訳（メタデータ） (2023-07-10T21:14:39Z)
• Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation [79.89605349842569]
  オンラインプロパティのコレクション・リファインメント(CROP)フレームワークをトレーニング時にプロパティを設計するために導入する。 CROPは、安全でない相互作用を識別し、安全特性を形成するためにコストシグナルを使用する。 本手法をいくつかのロボットマップレスナビゲーションタスクで評価し,CROPで計算した違反量によって,従来のSafe DRL手法よりも高いリターンと低いリターンが得られることを示す。
  論文  参考訳（メタデータ） (2023-02-13T21:19:36Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  データ認識参照プロセスに対する不確実なログの適合性を確認する方法を示す。 我々のアプローチはモジュラーであり、異なるタイプの不確実性に均質に適合する。 本研究は,概念実証によるアプローチの正しさと実現可能性を示す。
  論文  参考訳（メタデータ） (2022-06-15T11:39:45Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  本稿では,専門家によるデモンストレーションの部分的な観察から,安全な出力フィードバック制御法を考察する。 まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。 次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
  論文  参考訳（メタデータ） (2021-11-18T23:21:00Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。 我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。 ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
  論文  参考訳（メタデータ） (2021-06-03T16:45:40Z)

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

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