Automatic Generation of Formally-Proven Tamper-Resistant Galois-Field Multipliers Based on Generalized Masking Scheme
Rei Ueno1,a, Naofumi Homma1, Sumio Morioka2 and Takafumi Aoki1
1Tohoku University, Aramaki Aza Aoba 6-6-05, Sendai-shi, 980-8579, Japan.
aueno@aoki.ecei.tohoku.ac.jp
2Interstellar Technologies Inc., 690-4 Memu, Taiki, Hiroo-gun, Hokkaido, 089-2113, Japan
ABSTRACT
In this study, we propose a formal design system for tamper-resistant cryptographic hardwares based on Generalized Masking Scheme (GMS). The masking scheme, which is a stateof-the-art masking-based countermeasure against higher-order differential power analyses (DPAs), can securely construct any kind of Galois-field (GF) arithmetic circuits at the register transfer level (RTL) description, while most other ones require specific physical design. In this study, we first present a formal design methodology of GMS-based GF arithmetic circuits based on a hierarchical dataflow graph, called GF arithmetic circuit graph (GF-ACG), and present a formal verification method for both functionality and security property based on Gr38#246;bner basis. In addition, we propose an automatic generation system for GMSbased GF multipliers, which can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 38 215;77) within 15 min.
Keywords: Formal verification, Arithmetic circuits, Galois-field, Threshold implementation, Side-channel attack.
