A hierarchical formal approach to verifying side-channel resistant cryptographic processors

Kotaro Okamoto, Naofumi Homma, Takafumi Aoki, Sumio Morioka

研究成果: Conference contribution

2 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルProceedings of the 2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014
出版社IEEE Computer Society
ページ76-79
ページ数4
ISBN(印刷版)9781479941148
DOI
出版ステータスPublished - 2014
イベント2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014 - Arlington, VA, United States
継続期間: 2014 5月 62014 5月 7

出版物シリーズ

名前Proceedings of the 2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014

Other

Other2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014
国/地域United States
CityArlington, VA
Period14/5/614/5/7

ASJC Scopus subject areas

  • ハードウェアとアーキテクチャ
  • 安全性、リスク、信頼性、品質管理

フィンガープリント

「A hierarchical formal approach to verifying side-channel resistant cryptographic processors」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル