論文の概要: Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation

• arxiv url: http://arxiv.org/abs/2405.12187v2
• Date: Tue, 28 May 2024 13:06:13 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-30 00:29:50.713111
• Title: Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation
• Title（参考訳）: Brewer-Nash Scrutinized:Write Revocationを特徴とするポリシーの機械的チェック
• Authors: Alfredo Capozucca, Maximiliano Cristiá, Ross Horne, Ricardo Katz,
• Abstract要約: 倫理的中国壁政策に触発されたブルワー・ナッシュの安全政策モデルを再考する。 書き込みアクセスのための現代的なオペレーションセマンティクスを提供します。 本稿では,Brewer-Nashモデルにおける情報フローの解析を近代化する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in the Brewer-Nash model, by adopting a more precise definition adapted from Kessler. For our modernised reformulation, we provide full mechanised coverage for all theorems proposed by Brewer & Nash. Most theorems are established automatically using the tool {log} with the exception of a theorem regarding information flow, which combines a lemma in {log} with a theorem mechanised in Coq. Having covered all theorems originally posed by Brewer-Nash, achieving modern precision and mechanisation, we propose this work as a step towards a methodology for automated checking of more complex security policy models.
• Abstract（参考訳）: 本稿では,倫理的中国壁政策に触発されたブルワー・ナッシュ・セキュリティ・ポリシー・モデルを再考する。 我々はBrewer-Nashモデルで書き込みアクセスを無効にできるという事実に注意を払っている。 書き込みアクセスのセマンティクスはもともと不特定であり、現代の運用セマンティクスを提供する複数の解釈につながった。 我々は、Kesslerのより正確な定義を採用することにより、Brewer-Nashモデルにおける情報フローの分析を近代化する。 近代化された改革のために、Brewer & Nashによって提案された全ての定理について完全な機械化されたカバレッジを提供する。 ほとんどの定理は、情報フローに関する定理を除いて、ツール {log} を使って自動的に確立される。 ブリュワーナッシュが当初提案した全ての定理を網羅し、近代的な精度と機械化を実現し、より複雑なセキュリティポリシーモデルの自動チェックのための方法論への一歩として、本研究を提案する。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• Rigorous Probabilistic Guarantees for Robust Counterfactual Explanations [80.86128012438834]
  モデルシフトに対する反ファクトの堅牢性を計算することはNP完全であることを示す。 本稿では,頑健性の厳密な推定を高い保証で実現する新しい確率論的手法を提案する。
  論文  参考訳（メタデータ） (2024-07-10T09:13:11Z)
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
  不完全予想と不完全証明を完遂する枠組みを提案する。 このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。 また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
  論文  参考訳（メタデータ） (2024-01-22T12:49:08Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems [3.222802562733787]
  我々は、特異な論理に容易に適応したり、新たな推論プロセスを統合するように設計された、自動定理のための新しいフレームワークMATRを提案する。 我々はMATRの高レベル設計と実装の詳細について説明する。 次に、G"odelの不完全性定理の証明に適した形式化されたメタロジックを記述し、MATRにおける我々のメタロジックを用いて、第一不完全性定理と第二不完全性定理の両方の証明を半自動生成する進捗について報告する。
  論文  参考訳（メタデータ） (2020-05-06T03:29:34Z)
• Pre-training Is (Almost) All You Need: An Application to Commonsense Reasoning [61.32992639292889]
  事前学習されたトランスモデルの微調整は、一般的なNLPタスクを解決するための標準的なアプローチとなっている。 そこで本研究では,可視性ランキングタスクをフルテキスト形式でキャストする新たなスコアリング手法を提案する。 提案手法は, ランダム再起動にまたがって, より安定した学習段階を提供することを示す。
  論文  参考訳（メタデータ） (2020-04-29T10:54:40Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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