論文の概要: 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つのバグを見つけるように変換される。
関連論文リスト
- 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。