論文の概要: 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の耐障害性検証タスクで失敗する。

関連論文リスト

• FIRE: Fact-checking with Iterative Retrieval and Verification [63.67320352038525]
  FIREはエビデンス検索とクレーム検証を反復的に統合する新しいフレームワークである。 大きな言語モデル(LLM)のコストを平均7.6倍、検索コストを16.5倍削減しながら、パフォーマンスが若干向上している。 これらの結果から,FIREは大規模ファクトチェック業務における適用を約束していることが明らかとなった。
  論文  参考訳（メタデータ） (2024-10-17T06:44:18Z)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。 我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。 我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
  論文  参考訳（メタデータ） (2024-09-13T22:25:58Z)
• A Coin Has Two Sides: A Novel Detector-Corrector Framework for Chinese Spelling Correction [79.52464132360618]
  中国語のSpelling Correction(CSC)は、自然言語処理(NLP)の基本課題である。 本稿では,エラー検出・相関器の枠組みに基づく新しい手法を提案する。 我々の検出器は2つのエラー検出結果を得るように設計されており、それぞれ高精度とリコールが特徴である。
  論文  参考訳（メタデータ） (2024-09-06T09:26:45Z)
• Designing fault-tolerant circuits using detector error models [0.29998889086656577]
  本稿では,回路レベルでの耐故障性を完全に把握する検出誤差モデルの強力な形式性について検討する。 フォールトトレラント回路設計の工学サイクルにおける3つの抽象化レベルにフォーマリズムを適用した。
  論文  参考訳（メタデータ） (2024-07-18T18:00:05Z)
• Block Verification Accelerates Speculative Decoding [23.764655044837113]
  投機的復号法は高速モデルを用いて、ターゲットモデルによって並列に検証されるトークンのブロックをドラフトする。 以前の作業では、ドラフト検証は独立してトークン・バイ・トークンで行われる。 ブロック全体を共同で検証する単純なドラフト検証アルゴリズムであるBlock Verificationを提案する。
  論文  参考訳（メタデータ） (2024-03-15T16:28:22Z)
• 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)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• 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)

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

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