报告摘要：

故障注入攻击在密码芯片运行时利用电磁、激光束等物理手段改变密码算法执行逻辑从而诱导产生错误的输出，通过分析错误结果来破解密钥，对密码芯片的安全造成严重威胁。本报告将首先证明密码电路故障注入安全性形式化验证问题是CoNP完全的；随后，提出基于SAT的验证方法，该方法通过隐式故障向量编码技术将验证问题规约到SAT求解，解决了此前显示枚举故障注入攻击向量和电路输入的挑战，带来了数量级的效率提升；最后，设计了基于轮的组合验证方法，将验证问题分治到轮子电路验证，进而实现完整密码电路故障注入安全性的自动化验证。

报告人简介：

宋富，中国科学院软件研究所研究员、博士生导师，长期在网络空间安全与形式化验证交叉领域开展基础理论和应用基础研究。2013年获巴黎狄德罗大学（现巴黎西岱大学）博士学位，2013年--2016年在华东师范大学历任讲师和副研究员，2016年--2023年在上海科技大学历任助理教授、常任副教授、研究员、博士生导师、系统与安全中心主任。已主持和参与多项国家自然科学基金委青年、面上和重点项目，曾获上海市浦江人才、上海市晨光学者、亚马逊研究奖、中国电子学会网络空间安全优秀论文、欧洲软件科学与技术协会最佳论文，已在形式化验证、系统安全和软件工程等领域国际著名会议/期刊发表90余篇论文（CCF-A类论文40多篇），指导的博士研究生连续两年入选CCF 形式化方法专业委员会博士学位论文激励计划。详见https://songfu1983.github.io。