A Hierarchical Formal Approach to Verifying Side-channel Resistant Cryptographic Processors
A Hierarchical Formal Approach to Verifying Side-channel Resistant Cryptographic Processors
复制标题
验证抗侧信道密码处理器的分层形式方法
DOI：
10.1109/hst.2014.6855572
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Takafumi Aoki and Sumio Morioka
中科院分区：
文献类型：
--
作者：
Kotaro Okamoto;Naofumi Homma;Takafumi Aoki and Sumio Morioka
本文提出了一种基于字级计算机代数过程和使用 PPRM（正极性 Reed-Muller）扩展的位级决策过程相结合的密码处理器的分层形式验证方法。在所提出的方法中，密码处理器的整个数据路径结构以分层图的形式描述。在此图表示上，通过代数方法验证了整个电路功能的正确性，并分别通过PPRM方法验证了各个元件的功能。我们已将所提出的验证方法应用于复杂的 AES（高级加密标准）电路，并具有针对侧信道攻击的屏蔽对策。结果表明，该方法可以在4分钟内自动验证此类实用电路，而传统方法则无法验证。
This paper presents a hierarchical formal verification method for cryptographic processors based on a combination of a word-level computer algebra procedure and a bit-level decision procedure using PPRM (Positive Polarity Reed-Muller) expansion. In the proposed method, the entire datapath structure of a cryptographic processor is described in the form of a hierarchical graph . The correctness of the entire circuit function is verified on this graph representation, by the algebraic method, and the function of each component is verified by the PPRM method, respectively. We have applied the proposed verification method to a complicated AES (Advanced Encryption Standard) circuit with a masking countermeasure against side-channel attack. The results show that the proposed method can verify such practical circuit automatically within 4 minutes while the conventional methods fail.