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

Kotaro Okamoto, Naofumi Homma, Takafumi Aoki, Sumio Morioka

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014
PublisherIEEE Computer Society
Pages76-79
Number of pages4
ISBN (Print)9781479941148
DOIs
Publication statusPublished - 2014
Event2014 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2014 - Arlington, VA, United States
Duration: 2014 May 62014 May 7

Publication series

NameProceedings 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
Country/TerritoryUnited States
CityArlington, VA
Period14/5/614/5/7

Keywords

  • Galois fields
  • arithmetic circuits
  • cryptographic processors
  • design methodology for secure hardware
  • formal design

ASJC Scopus subject areas

  • Hardware and Architecture
  • Safety, Risk, Reliability and Quality

Fingerprint

Dive into the research topics of 'A hierarchical formal approach to verifying side-channel resistant cryptographic processors'. Together they form a unique fingerprint.

Cite this