論文の概要: Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification

• arxiv url: http://arxiv.org/abs/2503.13762v1
• Date: Mon, 17 Mar 2025 22:55:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-19 14:17:17.335559
• Title: Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
• Title（参考訳）: ユニット証明は機能するのか? : メモリ安全性検証のための構成境界モデル検査の実証的研究
• Authors: Paschal C. Amusuo, Owen Cochell, Taylor Le Lievre, Parth V. Patil, Aravind Machiry, James C. Davis,
• Abstract要約: メモリ安全性の欠陥は、ソフトウェアの信頼性に大きな脅威をもたらし、サイバー攻撃、停電、クラッシュを可能にします。 これらのリスクを軽減するため、組織はコンポジション境界モデルチェック(BMC)を採用し、ユニット証明を使用してメモリ安全性を正式に検証する。 しかし、ユニットテストを作成する方法は組織によって異なり、同じプロジェクト内で一貫性がないため、エラーや欠陥が失われる。 本研究は,メモリ安全性検証のためのユニット証明に関する最初の実証的研究である。
• 参考スコア（独自算出の注目度）: 4.826167697662746
• License:
• Abstract: Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded Model Checking (BMC), using unit proofs to formally verify memory safety. However, methods for creating unit proofs vary across organizations and are inconsistent within the same project, leading to errors and missed defects. In addition, unit proofing remains understudied, with no systematic development methods or empirical evaluations. This work presents the first empirical study on unit proofing for memory safety verification. We introduce a systematic method for creating unit proofs that leverages verification feedback and objective criteria. Using this approach, we develop 73 unit proofs for four embedded operating systems and evaluate their effectiveness, characteristics, cost, and generalizability. Our results show unit proofs are cost-effective, detecting 74\% of recreated defects, with an additional 9\% found with increased BMC bounds, and 19 new defects exposed. We also found that embedded software requires small unit proofs, which can be developed in 87 minutes and executed in 61 minutes on average. These findings provide practical guidance for engineers and empirical data to inform tooling design.
• Abstract（参考訳）: メモリ安全性の欠陥は、ソフトウェアの信頼性に大きな脅威をもたらし、サイバー攻撃、停電、クラッシュを可能にします。 これらのリスクを軽減するため、組織はコンポジション境界モデルチェック(BMC)を採用し、ユニット証明を使用してメモリ安全性を正式に検証する。 しかし、ユニットテストを作成する方法は組織によって異なり、同じプロジェクト内で一貫性がないため、エラーや欠陥が失われる。 さらに、体系的な開発方法や経験的評価は行わず、ユニットテストも検討されている。 本研究は,メモリ安全性検証のためのユニット証明に関する最初の実証的研究である。 本稿では,検証フィードバックと客観的基準を利用する単位証明を作成するための体系的手法を提案する。 提案手法を用いて, 組込みオペレーティングシステムの73個のユニット証明を開発し, その有効性, 特性, コスト, 一般化性を評価する。 その結果, ユニット証明は費用対効果が高く, 74 %の再生欠陥が検出され, さらに9 %のBMC境界が増加し, 19 件の新たな欠陥が露出した。 また、組込みソフトウェアには、87分で開発でき、平均61分で実行される小さなユニット証明が必要であることもわかりました。 これらの知見は、技術者や経験的データに対して、ツール設計を通知するための実践的なガイダンスを提供する。

関連論文リスト

• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Enabling Unit Proofing for Software Implementation Verification [2.7325338323814328]
  本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
  論文  参考訳（メタデータ） (2024-10-18T18:37:36Z)
• What Makes and Breaks Safety Fine-tuning? A Mechanistic Study [64.9691741899956]
  安全性の微調整は、大規模な言語モデル(LLM)を、安全なデプロイメントのための人間の好みに合わせるのに役立つ。 安全でない入力の健全な側面をキャプチャする合成データ生成フレームワークを設計する。 これを用いて,3つのよく知られた安全微調整手法について検討する。
  論文  参考訳（メタデータ） (2024-07-14T16:12:57Z)
• Unlearning Backdoor Threats: Enhancing Backdoor Defense in Multimodal Contrastive Learning via Local Token Unlearning [49.242828934501986]
  マルチモーダルコントラスト学習は高品質な機能を構築するための強力なパラダイムとして登場した。 バックドア攻撃は 訓練中に モデルに 悪意ある行動を埋め込む 我々は,革新的なトークンベースの局所的忘れ忘れ学習システムを導入する。
  論文  参考訳（メタデータ） (2024-03-24T18:33:15Z)
• Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
  メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。 本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
  論文  参考訳（メタデータ） (2023-09-17T03:41:10Z)
• SureFED: Robust Federated Learning via Uncertainty-Aware Inward and Outward Inspection [29.491675102478798]
  本稿では,堅牢なフェデレーション学習のための新しいフレームワークであるSureFEDを紹介する。 SureFEDは、良識のあるクライアントのローカル情報を使って信頼を確立する。 理論的には、データとモデル中毒攻撃に対するアルゴリズムの堅牢性を証明する。
  論文  参考訳（メタデータ） (2023-08-04T23:51:05Z)
• Unleashing Mask: Explore the Intrinsic Out-of-Distribution Detection Capability [70.72426887518517]
  Out-of-Distribution(OOD)検出は、機械学習モデルを現実世界のアプリケーションにデプロイする際に、セキュアAIの必須の側面である。 本稿では,IDデータを用いた学習モデルのOOD識別能力を復元する新しい手法であるUnleashing Maskを提案する。 本手法では, マスクを用いて記憶した非定型サンプルを抽出し, モデルを微調整するか, 導入したマスクでプルーする。
  論文  参考訳（メタデータ） (2023-06-06T14:23:34Z)
• Avoid Adversarial Adaption in Federated Learning by Multi-Metric Investigations [55.2480439325792]
  Federated Learning(FL)は、分散機械学習モデルのトレーニング、データのプライバシの保護、通信コストの低減、多様化したデータソースによるモデルパフォーマンスの向上を支援する。 FLは、中毒攻撃、標的外のパフォーマンス劣化とターゲットのバックドア攻撃の両方でモデルの整合性を損なうような脆弱性に直面している。 我々は、複数の目的に同時に適応できる、強い適応的敵の概念を新たに定義する。 MESASは、実際のデータシナリオで有効であり、平均オーバーヘッドは24.37秒である。
  論文  参考訳（メタデータ） (2023-06-06T11:44:42Z)
• A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
  本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。 我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と事前訓練されたトランスフォーマーモデルを活用する。 本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。
  論文  参考訳（メタデータ） (2023-05-24T05:54:10Z)
• PAC-Based Formal Verification for Out-of-Distribution Data Detection [4.406331747636832]
  本研究は、VAEの符号化プロセスを用いて、OOD検出に基づくほぼ正しい(PAC)保証を行う。 ユーザ定義の信頼性で不慣れなインスタンスに検出エラーをバインドするために使用される。
  論文  参考訳（メタデータ） (2023-04-04T07:33:02Z)
• No Need to Know Physics: Resilience of Process-based Model-free Anomaly Detection for Industrial Control Systems [95.54151664013011]
  本稿では,システムの物理的特性に反する逆スプーフ信号を生成するための新しい枠組みを提案する。 トップセキュリティカンファレンスで公表された4つの異常検知器を分析した。
  論文  参考訳（メタデータ） (2020-12-07T11:02:44Z)

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

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