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

翻译：故障注入攻击是针对密码电路的一种主动物理攻击类型。研究人员已提出多种防护措施来抵御此类攻击，但其设计与实现过程复杂、易错且耗时。现有形式化故障抵抗验证方法在效率和可扩展性方面存在局限。本文首先将故障抵抗验证问题形式化为NP完全问题，进而提出一种创新方法，将该验证问题编码为布尔可满足性问题（SAT），从而可利用现成的SAT求解器解决。该方法已在开源工具FIRMER中实现，并在实际密码电路基准测试中进行了全面评估。实验结果表明，FIRMER能在3分钟内完成几乎所有（46/48个）基准电路的故障抵抗验证（剩余两个在35分钟内完成）。相比之下，现有方法即使在24小时内仍无法完成23个故障抵抗验证任务（每个任务独立计时）。