論文の概要: Checking and Automating Confidentiality Theory in Isabelle/UTP
- arxiv url: http://arxiv.org/abs/2310.10658v1
- Date: Thu, 7 Sep 2023 23:53:33 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-25 14:05:29.123271
- Title: Checking and Automating Confidentiality Theory in Isabelle/UTP
- Title（参考訳）: Isabelle/UTPにおける信頼度理論の検証と自動化
- Authors: Lex Bailey, Jim Woodcock, Simon Foster, Roberto Metere,
- Abstract要約: 我々は,プログラム検証の通常の部分として機密性を推し進めるべきであると主張している。
我々は、我々の機械化が銀行の業績からいくつかの例を前もって検証するのにどのように使えるかを示す。
- 参考スコア（独自算出の注目度）: 1.1849561189229347
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The severity of recent vulnerabilities discovered on modern CPUs, e.g., Spectre [1], highlights how information leakage can have devas-tating effects to the security of computer systems. At the same time, it suggests that confidentiality should be promoted as a normal part of program verification, to discover and mitigate such vulnerabili-ties early in development. The theory we propose is primarily based on Bank's theory [2], a framework for reasoning about confidentiali-ty properties formalised in the Unifying Theories of Programming (UTP) [3]. We mechanised our encoding in the current implementa-tion of UTP in the Isabelle theorem prover, Isabelle/UTP [4]. We have identified some theoretical issues in Bank's original framework. Finally, we demonstrate how our mechanisation can be used to for-mally verify of some of the examples from Bank's work.
- Abstract（参考訳）: 最近のCPUで発見された脆弱性の深刻さ、例えばSpectre [1]は、情報漏洩がコンピュータシステムのセキュリティに悪影響を及ぼす可能性があることを強調している。
同時に、機密性はプログラム検証の通常の部分として促進され、開発の初期段階においてそのようなヴァルネラビリ関係を発見し緩和するべきであることを示唆している。
我々が提案する理論は、主に、Unified Theories of Programming (UTP) [3] で定式化された機密性に関する推論の枠組みであるバンクの理論[2]に基づいています。
我々は、イザベル定理証明器イザベル/UTP[4]における現在の UTP 実装における符号化を機械化した。
我々はバンクの当初の枠組みにいくつかの理論的問題を特定した。
最後に、我々の機械化が銀行の業績の例のいくつかを前もって検証するためにどのように使えるかを実証する。
関連論文リスト
- A SAT-based approach to rigorous verification of Bayesian networks [13.489622701621698]
ベイジアンネットワークに適した検証フレームワークを導入し,これらの欠点に対処する。
本フレームワークは,(1)ベイジアンネットワークをブール論理リテラルに変換する2段階のコンパイルおよび符号化スキームと,(2)これらのリテラルを活用して制約として符号化された様々なプロパティを検証する形式的検証クエリの2つの主要なコンポーネントから構成される。
検証手法の効率をベンチマークし、実世界のシナリオでその実用性を実証する。
論文 参考訳（メタデータ） (2024-08-02T03:06:51Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - Mathematical Algorithm Design for Deep Learning under Societal and
Judicial Constraints: The Algorithmic Transparency Requirement [65.26723285209853]
計算モデルにおける透過的な実装が実現可能かどうかを分析するための枠組みを導出する。
以上の結果から,Blum-Shub-Smale Machinesは,逆問題に対する信頼性の高い解法を確立できる可能性が示唆された。
論文 参考訳（メタデータ） (2024-01-18T15:32:38Z) - Asynchronous Authentication [3.038642416291856]
デジタル資産盗難と個人情報盗難事件は、ユーザー認証の基礎を再考する緊急の必要性を示している。
非同期認証の一般的なケースを非有界メッセージ伝搬時間で定式化する。
我々のモデルは、暗号保証を維持するために実行時間を制限しながら、最終的なメッセージ配信を可能にします。
論文 参考訳（メタデータ） (2023-12-21T15:53:54Z) - Penetrating Shields: A Systematic Analysis of Memory Corruption Mitigations in the Spectre Era [6.212464457097657]
我々は、投機的実行攻撃を利用した投機的シールドバイパス攻撃を調査し、メモリ破損防止のセキュリティに重要な秘密を漏洩させる。
本稿では,すでに配備されている緩和機構と,最先端の2つの学術的提案を対象とする概念実証攻撃について述べる。
論文 参考訳（メタデータ） (2023-09-08T04:43:33Z) - Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive
Privacy Analysis and Beyond [57.10914865054868]
垂直ロジスティック回帰(VLR)をミニバッチ降下勾配で訓練した。
我々は、オープンソースのフェデレーション学習フレームワークのクラスにおいて、VLRの包括的で厳密なプライバシー分析を提供する。
論文 参考訳（メタデータ） (2022-07-19T05:47:30Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z) - Experimental quantum key distribution certified by Bell's theorem [0.0]
暗号鍵交換プロトコルは、伝統的に、盗聴攻撃に対するセキュリティを提供するために、計算予想に依存しています。
量子鍵分布プロトコルは、そのような攻撃に対して情報理論のセキュリティを提供する。
しかし、量子プロトコルは、関連する物理デバイスの実装欠陥を悪用する新たなタイプの攻撃の対象となっている。
ここでは、これらの脆弱性に免疫する完全量子鍵分布プロトコルの実験的実現について述べる。
論文 参考訳（メタデータ） (2021-09-29T17:52:48Z) - Certification of Iterative Predictions in Bayesian Neural Networks [79.15007746660211]
我々は、BNNモデルの軌道が与えられた状態に到達する確率に対して、安全でない状態の集合を避けながら低い境界を計算する。
我々は、制御と強化学習の文脈において、下限を用いて、与えられた制御ポリシーの安全性保証を提供する。
論文 参考訳（メタデータ） (2021-05-21T05:23:57Z) - Towards a Theoretical Understanding of the Robustness of Variational
Autoencoders [82.68133908421792]
敵攻撃や他の入力摂動に対する変分オートエンコーダ(VAE)の堅牢性を理解するために,我々は進出している。
確率モデルにおけるロバスト性のための新しい基準である$r$-robustnessを開発する。
遠心法を用いて訓練したVAEが、ロバストネスの指標でよく評価されていることを示す。
論文 参考訳（メタデータ） (2020-07-14T21:22:29Z) - Towards Probabilistic Verification of Machine Unlearning [30.892906429582904]
本稿では,データ削除要求に対する検証機構の設計について研究する形式的枠組みを提案する。
提案手法は,機械学習サービスの精度に最小限の影響を与えるが,未学習に対する信頼性の高い検証を可能にする。
論文 参考訳（メタデータ） (2020-03-09T16:39:46Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。