掩码是防御密码程序功耗侧信道攻击的一种有效方案，但是实现安全的掩码程序是一项艰巨而易错的工作，亟需形式化验证方法保障密码程序掩码实现的正确性，从而避免功耗侧信道攻击。

      本报告将介绍我们在功耗侧信道安全性问题上取得的一些进展，包括基于精化的验证方法学、组合概率分布类型推导、基于GPU的模型计数约束求解算法等。

      宋富，上海科技大学助理教授、研究员、博导，系统与安全中心主任。宋富博士于2013年4月获得巴黎大学（原巴黎狄德罗大学）计算机科学博士学位，同年8月加入华东师范大学任讲师，2016年1月破格晋升为副研究员，于2015年分别荣获上海市“浦江人才”和上海市“晨光学者”称号。2016年8月全职加入上海科技大学信息科学与技术学院，担任tenure-track助理教授、研究员。研究领域包括模型检验、程序分析与验证、系统和AI安全，已在国际一流期刊和会议发表50余篇论文，包括I&C、IEEE TSE、ACM TOSEM、CAV、ICSE、ISSTA、IEEE S&P等。