2022年11月14日晚上，上海科技大学宋富教授就“密码程序安全语言与形式验证”这一主题与我院教师和研究生进行了在线分享和交流。本次讲座由我院邵俊老师主持。
宋富，上海科技大学常任副教授、研究员、博士生导师、系统与安全中心主任，主要研究系统与软件安全验证和测试技术、及相关逻辑和自动机理论。宋富于2013年获巴黎狄德罗大学博士学位，曾在华东师范大学担任讲师和副研究员。主持和参与多项国家自然科学基金委青年、面上和重点项目，曾获上海市浦江人才和上海市晨光学者人才计划资助、2021年秋季亚马逊研究奖，已在国际著名会议或期刊（如CAV、ESEC/FSE、ICSE、ASE、ISSTA、S&P、FM、TOSEM、TSE、TDSC、I&C）发表多篇论文。
宋老师首先介绍了当前面临的密码程序安全威胁，即设计层密码程序安全威胁、实现层密码程序安全威胁以及运行层密码程序安全威胁。随后，宋老师介绍了两种密码算法：EasyBC和FISCHER，并介绍了密码程序功耗的侧信道安全技术，包括随机掩码、安全模型、形式化验证需求、一阶布尔程序验证和高阶算术程序验证。最后，宋老师介绍了JIT时间侧信道安全。
报告结束后，老师和同学们积极向宋老师提出自己的问题和想法，如：“掩码密码算法正确性结果是如何度量的”“在算法设计好的前提下能否直接实现相应功能”“对于软件和硬件所面临的侧信道攻击，使用的防御方式是否一致”等问题，宋老师都一一进行回答。此次报告讨论热烈，气氛活跃，老师们深觉专家分享内容丰富详细，讲解精准到位。