Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits（密码电路故障注入安全性形式化验证）

2024年11月21日（周四）早上10:00-11:00

信管学院308会议室

Fu Song（宋富）is a Research Professor at Institute of Software Chinese Academy of Sciences. He received Ph.D. from University Paris Diderot (Paris 7) in 2013. He was an Associate Professor (Tenured) and Assistant Professor School of Information Science and Technology ShanghaiTech University (2016-2023), an Associate Research Professor and Lecturer at School of Computer Science and Software Engineering in the East China Normal University (2013-2016). His research mainly focuses on the intersection of cybersecurity and formal methods. More details please refer to https://songfu1983.github.io.

‍‍密码电路故障注入安全性形式化验证

Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits

Fault injection attacks represent a type of active, physical attack against cryptographic circuits. Various countermeasures have been proposed to thwart such attacks, however, the design and implementation of which are intricate, error-prone, and laborious. The current formal fault-resistance verification approaches are limited in efficiency and scalability. In this talk, we first formalize the fault-resistance verification problem and show that it is coNP-complete; we then devise a novel approach for encoding the fault-resistance verification problem as the Boolean satisfiability (SAT) problem so that modern off-the-shelf SAT solvers can be utilized; finally we present the first compositional verification approach for round-based hardware implementations of cryptographic algorithms, decomposing a circuit into a set of single-round sub-circuits which are verified individually by either SAT/SMT- or BDD-based tools. The experimental results show that our approach is significantly more effective and efficient than the state-of-the-art.