SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits

• URL: http://arxiv.org/abs/2307.00561v1
• Date: Sun, 2 Jul 2023 13:01:32 GMT
• Title: SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits
• Authors: Huiyu Tan and Pengfei Gao and Taolue Chen and Fu Song and Zhilin Wu
• Abstract summary: This paper formalizes 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. The approach is implemented in an open-source tool FIRMER which is evaluated extensively on realistic cryptographic circuit benchmarks.
• Score: 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).

Related papers

• FIRE: Fact-checking with Iterative Retrieval and Verification [63.67320352038525]
  FIRE is a novel framework that integrates evidence retrieval and claim verification in an iterative manner. It achieves slightly better performance while reducing large language model (LLM) costs by an average of 7.6 times and search costs by 16.5 times. These results indicate that FIRE holds promise for application in large-scale fact-checking operations.
  arXiv  Detail & Related papers  (2024-10-17T06:44:18Z)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  Satisfiability-based automated reasoning is successfully used in software engineering to validate complex software. We tackle the challenge of validating the correctness of FOL* unsatisfiability results. We develop a proof-based diagnosis to explain the cause of unsatisfiability.
  arXiv  Detail & Related papers  (2024-09-13T22:25:58Z)
• A Coin Has Two Sides: A Novel Detector-Corrector Framework for Chinese Spelling Correction [79.52464132360618]
  Chinese Spelling Correction (CSC) stands as a foundational Natural Language Processing (NLP) task. We introduce a novel approach based on error detector-corrector framework. Our detector is designed to yield two error detection results, each characterized by high precision and recall.
  arXiv  Detail & Related papers  (2024-09-06T09:26:45Z)
• Scalable Similarity-Aware Test Suite Minimization with Reinforcement Learning [6.9290255098776425]
  TripRL is a novel technique to produce a diverse reduced test suite with high test effectiveness. We show that TripRL's runtime scales linearly with the magnitude of the Multi-Criteria Test Suite Minimization problem.
  arXiv  Detail & Related papers  (2024-08-24T08:43:03Z)
• Designing fault-tolerant circuits using detector error models [0.29998889086656577]
  We explore the powerful formalism of detector error models, which fully captures fault-tolerance at the circuit level. We apply the formalism to three different levels of abstraction in the engineering cycle of fault-tolerant circuit designs.
  arXiv  Detail & Related papers  (2024-07-18T18:00:05Z)
• Block Verification Accelerates Speculative Decoding [23.764655044837113]
  Speculative decoding uses a fast model to draft a block of tokens which are verified in parallel by the target model. In prior works, draft verification is performed independently token-by-token. We propose Block Verification, a simple draft verification algorithm that verifies the entire block jointly.
  arXiv  Detail & Related papers  (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]
  The original Steane code is not fault-tolerant because the CNOT gates in an encoded block may cause error propagation. We first propose a fault-tolerant encoding and decoding scheme, which analyzes all possible errors caused by each quantum gate in an error-correction period. We then provide the fault-tolerant scheme of the universal quantum gate set, including fault-tolerant preparation and verification of ancillary states.
  arXiv  Detail & Related papers  (2024-03-07T07:46:03Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Fault-tolerant parity readout on a shuttling-based trapped-ion quantum computer [64.47265213752996]
  We experimentally demonstrate a fault-tolerant weight-4 parity check measurement scheme. We achieve a flag-conditioned parity measurement single-shot fidelity of 93.2(2)%. The scheme is an essential building block in a broad class of stabilizer quantum error correction protocols.
  arXiv  Detail & Related papers  (2021-07-13T20:08:04Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels [8.9960048245668]
  Deep Neural Networks (DNNs) have become key components of many safety-critical applications such as autonomous driving and medical diagnosis. DNNs suffer from poor robustness because of their susceptibility to adversarial examples such that small perturbations to an input result in misprediction. We propose a novel approach that can accelerate the robustness verification techniques by guiding the verification with target labels.
  arXiv  Detail & Related papers  (2020-07-16T00:51:52Z)
• Robust Encodings: A Framework for Combating Adversarial Typos [85.70270979772388]
  NLP systems are easily fooled by small perturbations of inputs. Existing procedures to defend against such perturbations provide guaranteed robustness to worst-case attacks. We introduce robust encodings (RobEn) that confer guaranteed robustness without making compromises on model architecture.
  arXiv  Detail & Related papers  (2020-05-04T01:28:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.