计算机科学与探索

作者：张俊

单位：1. 中国科学院 上海微系统与信息技术研究所，上海 2000502. 上海科技大学 信息科学与技术学院，上海 2012103. 中国科学院大学，北京 100049

关键词：侧信道攻击,可满足性模理论（SMT）,软件验证,类型推导,形式化验证

功耗侧信道攻击，通过使用统计分析技术推断出加密算法中的密钥，已成为物理网络设备的一个巨大威胁。随机掩码是一种被广泛使用的用来消除密钥数据和侧信道泄露数据之间关联性的对策。尽管现有技术可以验证加密软件代码是否被随机掩码保护，但是它们在准确性和可扩展性方面受到限制。为消除此类限制，提出了一种基于原有技术改进过的验证随机掩码策略的方法，该方法比已有的基于句法类型的推断技术更准确，比使用SAT（SMT）模型计数的方法更具有可扩展性。实际上，该方法使用一系列语义类型推导规则去推导分布类型，这些规则最初保持抽象以允许快速推导，然后具体化那些抽象规则推导解决不了的验证问题。此类细化方法集成在验证工具SCVerify中，并使用包含AES和MAC-Keccak等加密算法的测试用例进行了验证，实验结果表明此方法在准确性和可扩展性方面明显优于当前的技术。

来源：2021年第6期

《计算机科学与探索》期刊编辑部

查看计算机科学与探索杂志2021年第6期