論文の概要: SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits
- arxiv url: http://arxiv.org/abs/2307.00561v1
- Date: Sun, 2 Jul 2023 13:01:32 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-23 18:35:26.657699
- Title: SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits
- Title(参考訳): SATによる暗号回路の形式的フォールト抵抗検証
- Authors: Huiyu Tan and Pengfei Gao and Taolue Chen and Fu Song and Zhilin Wu
- Abstract要約: 本稿では,NP完全であることを示す耐故障性検証問題を定式化する。
そこで我々は,耐故障性検証問題をBoolean satisfiability (SAT)問題として符号化する新しい手法を考案した。
この手法は、リアルな暗号回路ベンチマークで広く評価されているオープンソースツールFIRMERで実装されている。
- 参考スコア(独自算出の注目度): 4.42563968195381
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Fault injection attacks represent a type of active, physical attack against
cryptographic circuits. Various countermeasures have been proposed to thwart
such attacks, the design and implementation of which are, however, intricate,
error-prone, and laborious. The current formal fault-resistance verification
approaches are limited in efficiency and scalability. In this paper, we
formalize the fault-resistance verification problem which is shown to be
NP-complete. We then devise a novel approach for encoding the fault-resistance
verification problem as the Boolean satisfiability (SAT) problem so that
off-the-shelf SAT solvers can be utilized. The approach is implemented in an
open-source tool FIRMER which is evaluated extensively on realistic
cryptographic circuit benchmarks. The experimental results show that FIRMER is
able to verify fault-resistance of almost all (46/48) benchmarks in 3 minutes
(the other two are verified in 35 minutes). In contrast, the prior approach
fails on 23 fault-resistance verification tasks even after 24 hours (per task).
- Abstract(参考訳): フォールトインジェクション攻撃は、暗号回路に対するアクティブで物理的攻撃の一種である。
このような攻撃を阻止するための様々な対策が提案されているが、その設計と実装は複雑で、エラーの危険性があり、厳しい。
現在の正式な耐障害性検証アプローチは、効率とスケーラビリティに制限がある。
本稿では,NP完全であることを示す耐故障性検証問題を定式化する。
そこで我々は,既設のSATソルバを活用できるように,耐故障性検証問題をBoolean satisfiability (SAT)問題として符号化する新しい手法を考案した。
この手法は、リアルな暗号回路ベンチマークで広く評価されているオープンソースツールFIRMERで実装されている。
実験の結果、FIRMERは3分でほぼ全ての(46/48)ベンチマークの耐故障性を検証することができる(他の2つは35分で検証される)。
対照的に、先行するアプローチは、24時間後(タスク毎)に23の耐障害性検証タスクで失敗する。
関連論文リスト
- Analysis of Maximum Threshold and Quantum Security for Fault-Tolerant
Encoding and Decoding Scheme Base on Steane Code [10.853582091917236]
エンコードされたブロックのCNOTゲートがエラーの伝播を引き起こす可能性があるため、オリジナルのSteaneコードはフォールトトレラントではない。
まず, 誤り訂正期間において, 量子ゲート毎に発生する全てのエラーを解析するフォールトトレラント符号化・復号方式を提案する。
次に、耐故障性の準備とアシラリー状態の検証を含む、普遍量子ゲート集合の耐故障性スキームを提供する。
論文 参考訳(メタデータ) (2024-03-07T07:46:03Z) - Token-Level Adversarial Prompt Detection Based on Perplexity Measures
and Contextual Information [67.78183175605761]
大規模言語モデルは、敵の迅速な攻撃に影響を受けやすい。
この脆弱性は、LLMの堅牢性と信頼性に関する重要な懸念を浮き彫りにしている。
トークンレベルで敵のプロンプトを検出するための新しい手法を提案する。
論文 参考訳(メタデータ) (2023-11-20T03:17:21Z) - Clover: Closed-Loop Verifiable Code Generation [2.771446134416298]
整合性チェックのよりアクセスしやすい問題に対する正当性チェックを削減できるCloverパラダイムを提案する。
Cloverの中核には、コード、ドキュストリング、フォーマルアノテーション間の一貫性チェックを実行するチェッカーがある。
注釈付きDafnyプログラムを教科書の難易度で記述した手書きデータセットの有効性を実証的に検討した。
論文 参考訳(メタデータ) (2023-10-26T22:58:19Z) - Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。
本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。
その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文 参考訳(メタデータ) (2023-10-19T15:40:00Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳(メタデータ) (2023-01-17T18:32:01Z) - Execution Time Program Verification With Tight Bounds [6.36836017515443]
本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。
3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。
証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
論文 参考訳(メタデータ) (2022-10-20T09:02:13Z) - Fault-tolerant parity readout on a shuttling-based trapped-ion quantum
computer [64.47265213752996]
耐故障性ウェイト4パリティチェック測定方式を実験的に実証した。
フラグ条件パリティ測定の単発忠実度は93.2(2)%である。
このスキームは、安定化器量子誤り訂正プロトコルの幅広いクラスにおいて必須な構成要素である。
論文 参考訳(メタデータ) (2021-07-13T20:08:04Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。
ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。
本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文 参考訳(メタデータ) (2020-10-07T08:19:48Z) - Accelerating Robustness Verification of Deep Neural Networks Guided by
Target Labels [8.9960048245668]
ディープニューラルネットワーク(DNN)は、自律運転や医療診断など、多くの安全クリティカルなアプリケーションの主要なコンポーネントとなっている。
DNNは、入力に対する小さな摂動が誤った予測をもたらすような敵の例に感受性があるため、ロバスト性に悩まされる。
本稿では,ロバスト性検証を目標ラベルで導くことによって,ロバスト性検証手法を高速化する手法を提案する。
論文 参考訳(メタデータ) (2020-07-16T00:51:52Z) - Robust Encodings: A Framework for Combating Adversarial Typos [85.70270979772388]
NLPシステムは入力の小さな摂動によって容易に騙される。
このような混乱に対して防御するための既存の手順は、最悪の場合の攻撃に対して確実な堅牢性を提供する。
モデルアーキテクチャに妥協を加えることなく、ロバスト性を保証するロブエン(RobEn)を導入します。
論文 参考訳(メタデータ) (2020-05-04T01:28:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。