张 俊

1.中国科学院 上海微系统与信息技术研究所，上海200050

2.上海科技大学 信息科学与技术学院，上海201210

3.中国科学院大学，北京100049

+通信作者E-mail:zhangjun@shanghaitech.edu.cn

现代社会生活中，密码算法已经广泛应用于嵌入式计算设备，以构成其安全机制的支柱，嵌入式设备中硬件和软件系统的安全性分析变得越来越重要。一般来说，安全性是建立在攻击者只能访问输入输出，但是不能访问到中间计算结果的基础上。不幸的是，攻击者可以通过分析侧信道物理泄露信息，通过统计分析的方法来获得相关中间计算结果，从而推算出加密密钥。这些所谓的侧信道攻击利用密钥和计算设备的非功能属性，如执行时间[1]、功耗[2]、电磁辐射[3]等的统计依赖性，其中，差分功耗分析（differential power analysis，DPA）是一种极受欢迎且有效的攻击手段[4]。

到目前为止，已经有很多对策可以阻止侧信道攻击。针对功耗侧信道攻击，掩码技术仍然是使用最为广泛的一种技术，可以通过随机化的方式打破密钥和侧信道泄露信息之间的统计依赖性。例如，对于一个敏感的密钥变量k，使用布尔掩盖，利用一个随机变量r和异或操作⊕可以获得一个掩盖变量km=k⊕r，并且通过异或操作的可逆性可以利用相同的随机变量r恢复出密钥变量km⊕r=k。其他的随机化掩码对策有加法掩盖km=k+rmodn，乘法掩盖km=k*rmodn。虽然已经有了各种掩码的实现方式，如用于AES（advanced encryption standard）或其非线性组件（S-box）[5-7]，但是检查它们是否正确总是很困难且容易出错。因此，形式化验证这些掩码对策的正确性是十分重要的。……