基于 SAT 的密码学电路形式化故障抵抗验证
密码学与安全
2023-07-04 v1 硬件体系结构
软件工程
摘要
故障注入攻击是一类针对密码学电路的主动物理攻击。人们已提出多种对策以抵御此类攻击，但其设计与实现复杂、易出错且繁琐。现有的形式化故障抵抗验证方法在效率与可扩展性上受限。本文形式化了故障抵抗验证问题，并证明其是 NP 完全的。随后我们设计了一种将故障抵抗验证问题编码为布尔可满足性（SAT）问题的新方法，从而可利用现成的 SAT 求解器。该方法实现于开源工具 FIRMER 中，并在真实密码学电路基准上进行了广泛评估。实验结果表明，FIRMER 能够在 3 分钟内验证几乎全部（46/48）基准的故障抵抗性（其余两个在 35 分钟内验证）。相比之下，先前的方法即使在每个任务 24 小时后，仍有 23 个故障抵抗验证任务失败。
引用
@article{arxiv.2307.00561,
title = {SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits},
author = {Huiyu Tan and Pengfei Gao and Taolue Chen and Fu Song and Zhilin Wu},
journal= {arXiv preprint arXiv:2307.00561},
year = {2023}
}