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

• arxiv url: http://arxiv.org/abs/2405.12187v1
• Date: Mon, 20 May 2024 17:18:26 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-21 12:25:40.579597
• 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} を使って自動的に確立される。 ブリュワーナッシュが当初提案した全ての定理を網羅し、近代的な精度と機械化を実現し、より複雑なセキュリティポリシーモデルの自動チェックのための方法論への一歩として、本研究を提案する。

関連論文リスト

• Strands Rocq: Why is a Security Protocol Correct, Mechanically? [3.6840775431698893]
  StrandsRocq は Coq のストランド空間の機械化である。 新しい証明技法と、新しい最大貫入器の概念が組み込まれている。 これは2つの単純な認証プロトコルに対するセキュリティの合成証明を提供する。
  論文  参考訳（メタデータ） (2025-02-18T13:34:58Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• 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)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
  不完全予想と不完全証明を完遂する枠組みを提案する。 このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。 また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
  論文  参考訳（メタデータ） (2024-01-22T12:49:08Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• 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)

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

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