Hierarchical Formal Verification Combining Algebraic Transformation with PPRM Expansion and Its Application to Masked Cryptographic Processors

Rei UENO; Naofumi HOMMA; Takafumi AOKI; Sumio MORIOKA

doi:10.1587/transfun.E100.A.1396

IEICE TRANSACTIONS on Fundamentals

Hierarchical Formal Verification Combining Algebraic Transformation with PPRM Expansion and Its Application to Masked Cryptographic Processors

Rei UENO, Naofumi HOMMA, Takafumi AOKI, Sumio MORIOKA

Full Text Views

0

Cite this

Summary :

This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2^m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2^m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2^m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed 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 any single conventional verification methods fail within a day or even more.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E100-A No.7 pp.1396-1408

Publication Date: 2017/07/01

Publicized

Online ISSN: 1745-1337

DOI: 10.1587/transfun.E100.A.1396

Type of Manuscript: Special Section PAPER (Special Section on Design Methodologies for System on a Chip)

Category

Authors

Rei UENO
  Tohoku University
Naofumi HOMMA
  Tohoku University
Takafumi AOKI
  Tohoku University
Sumio MORIOKA
  the Interstellar Technologies Inc.

Keyword

design methodology for security hardware, formal design, cryptographic processors, Galois field, arithmetic circuits

Cite this

Copy

Rei UENO, Naofumi HOMMA, Takafumi AOKI, Sumio MORIOKA, "Hierarchical Formal Verification Combining Algebraic Transformation with PPRM Expansion and Its Application to Masked Cryptographic Processors" in IEICE TRANSACTIONS on Fundamentals, vol. E100-A, no. 7, pp. 1396-1408, July 2017, doi: 10.1587/transfun.E100.A.1396.
Abstract: This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2^m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2^m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2^m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed 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 any single conventional verification methods fail within a day or even more.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E100.A.1396/_p

Copy

@ARTICLE{e100-a_7_1396,
author={Rei UENO, Naofumi HOMMA, Takafumi AOKI, Sumio MORIOKA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Hierarchical Formal Verification Combining Algebraic Transformation with PPRM Expansion and Its Application to Masked Cryptographic Processors},
year={2017},
volume={E100-A},
number={7},
pages={1396-1408},
abstract={This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2^m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2^m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2^m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed 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 any single conventional verification methods fail within a day or even more.},
keywords={},
doi={10.1587/transfun.E100.A.1396},
ISSN={1745-1337},
month={July},}

Copy

TY - JOUR
TI - Hierarchical Formal Verification Combining Algebraic Transformation with PPRM Expansion and Its Application to Masked Cryptographic Processors
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1396
EP - 1408
AU - Rei UENO
AU - Naofumi HOMMA
AU - Takafumi AOKI
AU - Sumio MORIOKA
PY - 2017
DO - 10.1587/transfun.E100.A.1396
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E100-A
IS - 7
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - July 2017
AB - This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2^m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2^m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2^m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed 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 any single conventional verification methods fail within a day or even more.
ER -

IEICE TRANSACTIONS on Fundamentals