A Systematic Design Methodology of Formally Proven Side-Channel-Resistant Cryptographic Hardware

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.