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

Rei Ueno; Naofumi Homma; Sumio Morioka; Takafumi Aoki

doi:10.1109/MDAT.2021.3063337

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

Rei Ueno, Naofumi Homma, Sumio Morioka, Takafumi Aoki

Research output: Contribution to journal › Article › peer-review

Abstract

In this study, we propose a formal design system for automatically generating provably-secure register transfer level (RTL) description of cryptographic hardwares based on Generalized Masking Scheme (GMS). 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 Gröbner basis. The proposed automatic generation system for GMS-based GF multipliers can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 × 77) within 15 min.

Original language	English
Journal	IEEE Design and Test
DOIs	https://doi.org/10.1109/MDAT.2021.3063337
Publication status	Accepted/In press - 2021

Keywords

Adders
Cryptographic hardware
Cryptography
Design methodology
Differential power analysis
Formal verification
Galois-field arithmetic circuit
Hardware
Masking
Registers
Resistance
Side-channel attacks
and Side-channel attack

ASJC Scopus subject areas

Software
Hardware and Architecture
Electrical and Electronic Engineering

Access to Document

10.1109/MDAT.2021.3063337

Fingerprint Dive into the research topics of 'A Systematic Design Methodology of Formally-Proven Side-Channel-Resistant Cryptographic Hardware'. Together they form a unique fingerprint.

Cite this

@article{4ceccccbe2b547299c632629f46e1785,

title = "A Systematic Design Methodology of Formally-Proven Side-Channel-Resistant Cryptographic Hardware",

abstract = "In this study, we propose a formal design system for automatically generating provably-secure register transfer level (RTL) description of cryptographic hardwares based on Generalized Masking Scheme (GMS). 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 Gr{\"o}bner basis. The proposed automatic generation system for GMS-based GF multipliers can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 × 77) within 15 min.",

keywords = "Adders, Cryptographic hardware, Cryptography, Design methodology, Differential power analysis, Formal verification, Galois-field arithmetic circuit, Hardware, Masking, Registers, Resistance, Side-channel attacks, and Side-channel attack",

author = "Rei Ueno and Naofumi Homma and Sumio Morioka and Takafumi Aoki",

note = "Publisher Copyright: IEEE",

year = "2021",

doi = "10.1109/MDAT.2021.3063337",

language = "English",

journal = "IEEE Design and Test",

issn = "2168-2356",

publisher = "IEEE Computer Society",

}

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 - Publisher Copyright: IEEE

PY - 2021

Y1 - 2021

N2 - In this study, we propose a formal design system for automatically generating provably-secure register transfer level (RTL) description of cryptographic hardwares based on Generalized Masking Scheme (GMS). 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 Gröbner basis. The proposed automatic generation system for GMS-based GF multipliers can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 × 77) within 15 min.

AB - In this study, we propose a formal design system for automatically generating provably-secure register transfer level (RTL) description of cryptographic hardwares based on Generalized Masking Scheme (GMS). 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 Gröbner basis. The proposed automatic generation system for GMS-based GF multipliers can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 × 77) within 15 min.

KW - Adders

KW - Cryptographic hardware

KW - Cryptography

KW - Design methodology

KW - Differential power analysis

KW - Formal verification

KW - Galois-field arithmetic circuit

KW - Hardware

KW - Masking

KW - Registers

KW - Resistance

KW - Side-channel attacks

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

JO - IEEE Design and Test

JF - IEEE Design and Test

SN - 2168-2356

ER -

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

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Cite this