TY - JOUR
T1 - A Systematic Design Methodology of Formally Proven Side-Channel-Resistant Cryptographic Hardware
AU - Ueno, Rei
AU - Homma, Naofumi
AU - Morioka, Sumio
AU - Aoki, Takafumi
N1 - Funding Information:
We are grateful to Yukihiro Sugawara for his corporation. This work was supported by JSPS KAKENHI under Grant 17H00729 and Grant 20K19765.
PY - 2021/6
Y1 - 2021/6
N2 - This article proposes a formal design system for automatically generating provably secure register transfer level description of cryptographic hardware based on generalized masking scheme. To address the above problems, we propose a formal design and verification method for generalized masking schem (GMS)-based Galois-field (GF) arithmetic circuits. The proposed method is based on a formal approach to describing and verifying GF arithmetic circuits. The basic ideas revolve around the description of GF arithmetic circuits using a high-level mathematical graph called GF arithmetic circuit graph (GF-ACG) and its verification using an algebraic procedure based on a GroÄbner basis (GB) and a polynomial reduction technique. The proposed methodology automatically generates the GMS-based GF arithmetic circuits from circuit function and GMS order, and then its functionality is verified on the basis of GF-ACG.
AB - This article proposes a formal design system for automatically generating provably secure register transfer level description of cryptographic hardware based on generalized masking scheme. To address the above problems, we propose a formal design and verification method for generalized masking schem (GMS)-based Galois-field (GF) arithmetic circuits. The proposed method is based on a formal approach to describing and verifying GF arithmetic circuits. The basic ideas revolve around the description of GF arithmetic circuits using a high-level mathematical graph called GF arithmetic circuit graph (GF-ACG) and its verification using an algebraic procedure based on a GroÄbner basis (GB) and a polynomial reduction technique. The proposed methodology automatically generates the GMS-based GF arithmetic circuits from circuit function and GMS order, and then its functionality is verified on the basis of GF-ACG.
KW - Cryptographic hardware
KW - Differential power analysis
KW - Formal verification
KW - Galois-field arithmetic circuit
KW - Masking
KW - and Side-channel attack
UR - http://www.scopus.com/inward/record.url?scp=85102265197&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85102265197&partnerID=8YFLogxK
U2 - 10.1109/MDAT.2021.3063337
DO - 10.1109/MDAT.2021.3063337
M3 - Article
AN - SCOPUS:85102265197
VL - 38
SP - 84
EP - 92
JO - IEEE Design and Test
JF - IEEE Design and Test
SN - 2168-2356
IS - 3
M1 - 9367223
ER -