TY - GEN
T1 - A hierarchical formal approach to verifying side-channel resistant cryptographic processors
AU - Okamoto, Kotaro
AU - Homma, Naofumi
AU - Aoki, Takafumi
AU - Morioka, Sumio
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Galois fields
KW - arithmetic circuits
KW - cryptographic processors
KW - design methodology for secure hardware
KW - formal design
UR - http://www.scopus.com/inward/record.url?scp=84905965868&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84905965868&partnerID=8YFLogxK
U2 - 10.1109/HST.2014.6855572
DO - 10.1109/HST.2014.6855572
M3 - Conference contribution
AN - SCOPUS:84905965868
SN - 9781479941148
T3 - Proceedings of the 2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014
SP - 76
EP - 79
BT - Proceedings of the 2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014
PB - IEEE Computer Society
T2 - 2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014
Y2 - 6 May 2014 through 7 May 2014
ER -