侧信道攻击能够利用成本较低的设备高效破解包括AES、DES、RSA等在内的大部分密码程序，对密码设备安全性造成重大威胁。以随机掩码为代表的抗侧信道攻击方案被广泛采用，但密码学家设计开发的随机掩码密码程序仍然存在侧信道漏洞。因此，如何证明密码程序的侧信道安全性是一项重要而又艰巨的任务。
为积极响应国家网络空间安全战略，我校信息学院宋富课题组与合作者在密码程序侧信道高阶安全性验证方面进行了长期深入的研究，并取得了系列重要进展。相关成果陆续发表在ACM Transactions on Software Engineering Methodology（ACM TOSEM）和IEEE Transactions on Software Engineering（IEEE TSE）。ACM TOSEM和IEEE TSE是国际上公认的最权威、最高水平的软件工程领域两大顶级期刊，也是中国计算机协会（CCF）推荐 A类期刊。ACM TOSEM近三年（2017年-2019年）平均每年接收文章20余篇，以中国内地为第一单位的论文平均每年仅有3篇，录用率极低。IEEE TSE具有6.112的影响因子，2019年在IEEE的所有计算机期刊中，影响因子排名第四。
2020年10月3日，课题组题为A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs的论文被ACM TOSEM接收。针对密码程序侧信道高阶安全性验证时出现的组合爆炸问题和模型计数约束求解的可扩展问题，课题组首次提出了一种基于分治的验证方法来解决组合爆炸问题和基于GPU并行计算的模型计数约束求解方法，同时开创性地提出了基于图同构的验证方法，从而为密码程序侧信道高阶安全性验证提供了理论基础和工具支持（图1）。该方法在可验证密码程序类型和规模、验证的精度和效率上引领国际先进水平。
图1 | HOME方法框架
除了上述在密码程序侧信道高阶安全性验证展开的研究，课题组在基于精化的密码程序侧信道一阶安全性验证（ACM Transactions on Software Engineering Methodology, 2019）和可组合类型推导系统（IEEE Transactions on Software Engineering，2020）方面也取得了不错的进展。
在发表于2019年ACM TOSEM的文章中，宋富教授和2018级博士研究生高鹏飞首次提出了基于精化的密码程序侧信道安全性验证方法学和语义层的类型推导系统（图2）。该验证方法学有机结合高效但不完备的类型推导系统和完备但低效的模型计数技术，在效率和精度上达到完美的互补。对于给定的密码程序，首先通过类型推导系统自动推理程序中间计算过程的概率分布类型；在大部分情况下，可以通过概率分布类型证明密码程序侧信道安全性。当类型推导系统无法证明密码程序部分中间计算过程侧信道安全时，采用模型计数技术进行验证，并将验证结果反馈给类型推导系统，精化类型推导过程。实验证明，此方法在验证速度和精确度上都处于国际领先水平。
图2 | 方法框架
在发表于2020年IEEE TSE的文章中，他们将该方法扩展到对算术程序的证明，同时创新地提出了可组合类型推导系统。该类型推导系统通过避免大部分函数调用的内联，大大提高了验证效率。设计开发的工具首次完成包括AES、DES等在内的十数个密码程序的自动化验证。
三篇论文中，高鹏飞为第一作者，宋富教授为通讯作者，上海科技大学为第一完成单位。该项目得到了国家自然科学基金委重点项目、中德国际合作项目和上科大科研启动基金的支持。
文章链接:
2020 ACM TOSEM论文http://faculty.sist.shanghaitech.edu.cn/faculty/songfu/publications/TOSEM20.pdf
2020 IEEE TSE论文https://ieeexplore.ieee.org/document/9139284
2019 ACM TOSEM论文 https://dl.acm.org/doi/10.1145/3330392
沪公网安备 31011502006855号