SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits

TL;DR

This paper introduces FIRMER, a SAT-based tool for efficiently verifying fault-resistance in cryptographic circuits, significantly outperforming previous methods in speed and scalability.

Contribution

It formalizes the NP-complete fault-resistance verification problem and encodes it as a SAT problem, enabling the use of SAT solvers for scalable verification.

Findings

FIRMER verifies 46 out of 48 benchmarks within 3 minutes.

Prior methods fail on 23 tasks after 24 hours.

FIRMER significantly improves verification efficiency and scalability.

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).