論文の概要: Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)

• arxiv url: http://arxiv.org/abs/2309.03442v1
• Date: Thu, 7 Sep 2023 01:51:41 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-25 22:59:44.364470
• Title: Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)
• Title（参考訳）: 仮定と検証:並行アプリケーションにおける漏洩情報の帰納的検証(拡張版)
• Authors: Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann,
• Abstract要約: 情報を意図的に漏洩する非自明な並行プログラムのセキュリティを特定・証明する問題を考察する。 本稿では,この問題を (a) 帰納的プログラム検証ですでに広く使用されているアノテーションを前提として,プログラムが情報のみを漏らすことを証明した手法を提案する。 また,既存のプログラム論理 SecCSL の拡張によって条件 (a) がどのように強制されるか,そして (b) が簡単な内容の集合を証明してどのようにチェックできるかを示す。
• 参考スコア（独自算出の注目度）: 1.3749490831384268
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information it has declassified via assume annotations already widely used in deductive program verification; and (b) auditing the declassifications against a declarative security policy. We show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments. Part of the challenge is to define respective semantic soundness criteria and to formally connect these to the logic rules and policy audit. We support our methodology in an auto-active program verifier, which we apply to verify the implementations of various case study programs against a range of declassification policies.
• Abstract（参考訳）: 情報を意図的に漏洩する非自明な並行プログラムのセキュリティを特定・証明する問題を考察する。 問題を分解する手法を提案する。 (a)演能的プログラム検証に既に広く使用されている前提アノテーションにより、プログラムが非分類化された情報のみを漏洩することを証明すること。 (b)宣言的安全保障政策に対する非分類の監査 私たちはどのようにして状態を示すか (a) は、既存のプログラムロジック SecCSL の拡張によって強制することができる。 (b) 簡単な内容のセットを証明して確認することができる。 課題の1つは、それぞれの意味音性基準を定義し、これらを論理規則とポリシー監査に正式に接続することである。 本手法を自動能動型プログラム検証器でサポートし,様々なケーススタディプログラムの実装を多種多様な非分類ポリシーに対して検証する。

関連論文リスト

• Handling expression evaluation under interference [0.0]
  プログラム構成のためのHoareスタイルの推論ルールは、プログラムテキストからの式とテストのコピーを論理的コンテキストに許可する。 のアプローチは、許容可能な干渉を記録する問題に取り組み、安全な推論ルールを提供する方法を提供する。
  論文  参考訳（メタデータ） (2024-09-12T04:16:22Z)
• Formally Verified Approximate Policy Iteration [11.602089225841633]
  形式化されたアルゴリズムが実行可能で検証可能な実装にどのように洗練されるかを示す。 実装は、その実行可能性を示すために、ベンチマーク問題で評価される。 この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。
  論文  参考訳（メタデータ） (2024-06-11T15:07:08Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。 このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。 我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
  論文  参考訳（メタデータ） (2024-01-02T03:37:11Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  データ認識参照プロセスに対する不確実なログの適合性を確認する方法を示す。 我々のアプローチはモジュラーであり、異なるタイプの不確実性に均質に適合する。 本研究は,概念実証によるアプローチの正しさと実現可能性を示す。
  論文  参考訳（メタデータ） (2022-06-15T11:39:45Z)
• Stateless and Rule-Based Verification For Compliance Checking Applications [1.7403133838762452]
  本稿では,インテリジェントなコンプライアンスチェックシステムを構築するための形式的な論理ベースのフレームワークを提案する。 SARVは、ステートレスおよびルールベースの検証問題の全体的な検証プロセスを単純化するために設計された検証フレームワークである。 300のデータ実験に基づいて、SARVベースのコンプライアンスソリューションは、3125レコードのソフトウェア品質データセット上で機械学習メソッドよりも優れています。
  論文  参考訳（メタデータ） (2022-04-14T17:31:33Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• An Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours [8.95294551927446]
  マルチエージェント強化学習(RL)はしばしば、学習エージェントの安全な行動を保証するために苦労する。 本稿では,形式検証と(深度)RLアルゴリズムを組み合わせることで,形式化された安全制約の満足度を保証する手法を提案する。
  論文  参考訳（メタデータ） (2021-02-02T11:12:30Z)
• Verification of indefinite-horizon POMDPs [63.6726420864286]
  本稿では,部分観測可能なMDPの検証問題について考察する。 本稿では,Lovejoy-approachの過去のインスタンス化を拡張した抽象化・リファインメント・フレームワークを提案する。
  論文  参考訳（メタデータ） (2020-06-30T21:01:52Z)
• Hierarchical Variational Imitation Learning of Control Programs [131.7671843857375]
  パラメータ化された階層的手順(PHP)で表される制御ポリシーの模倣学習のための変分推論手法を提案する。 本手法は, 教師による実演の観察・行動トレースのデータセットにおける階層構造を, 手続き呼び出しや用語の待ち行列に近似した後続分布を学習することによって発見する。 階層的模倣学習(hierarchical mimicion learning)の文脈における変分推論の新たな利点を実証する。
  論文  参考訳（メタデータ） (2019-12-29T08:57:02Z)

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

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