Proving SIFA Protection of Masked Redundant Circuits

Vedad Hadžić; Robert Primas; Roderick Bloem

doi:10.1007/978-3-030-88885-5_17

Proving SIFA Protection of Masked Redundant Circuits

Vedad Hadžić
, Robert Primas
, Roderick Bloem

Institute of Information Security (7050)

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Abstract

Implementation attacks like side-channel and fault attacks pose a considerable threat to cryptographic devices that are physically accessible by an attacker. As a consequence, devices like smart cards implement corresponding countermeasures like redundant computation and masking. Recently, statistically ineffective fault attacks (SIFA) were shown to be able to circumvent these classical countermeasure techniques. We present a new approach for verifying the SIFA protection of arbitrary masked implementations in both hardware and software. The proposed method uses Boolean dependency analysis, factorization, and known properties of masked computations to show whether the fault detection mechanism of redundant masked circuits can leak information about the processed secret values. We implemented this new method in a tool called Danira, which can show the SIFA resistance of cryptographic implementations like AES S-Boxes within minutes.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	19th International Symposium, ATVA 2021
Editors	Z. Hou, V. Ganesh
Place of Publication	Cham
Publisher	Springer
Pages	249-265
Number of pages	16
ISBN (Electronic)	978-3-030-88885-5
ISBN (Print)	978-3-030-88884-8
DOIs	https://doi.org/10.1007/978-3-030-88885-5_17
Publication status	Published - 2021
Event	19th International Symposium on Automated Technology for Verification and Analysis : ATVA 2021 - Virtuell, Australia Duration: 18 Oct 2021 → 22 Oct 2021

Publication series

Name	Lecture Notes in Computer Science
Volume	12971

Conference

Conference	19th International Symposium on Automated Technology for Verification and Analysis
Abbreviated title	ATVA 2021
Country/Territory	Australia
City	Virtuell
Period	18/10/21 → 22/10/21

Keywords

SIFA
verification
hardware security

ASJC Scopus subject areas

Hardware and Architecture
Computer Science (miscellaneous)

Access to Document

10.1007/978-3-030-88885-5_17

daniraSubmitted manuscript, 426 KB

2 Finished

FERMION - Formal Verification of Masked Hardware Implementations
Bloem, R. (Consortium manager resp. coordinator with external organisations)
2/01/19 → 1/01/22
Project: Research project
Dessnet - Dependable, secure and time-aware sensor networks
Deutschmann, B. (Attendee / Assistant), Görtschacher, L. J. (Attendee / Assistant), Shetty, D. (Contact person), Glanzer, C. (Attendee / Assistant), Mangard, S. (Project manager on research unit), Bösch, W. (Other function), Grosinger, J. (Project manager on research unit), Fischbacher, R. B. (Attendee / Assistant) & Grosinger, J. (Consortium manager resp. coordinator of internal research units)
1/06/17 → 31/05/21
Project: Research project

2 Article
1 Conference paper

Proving SIFA protection of masked redundant circuits
Hadzic, V., Primas, R. & Bloem, R., Sept 2022, In: Innovations in Systems and Software Engineering. 18, 3, p. 471-481 11 p.
Research output: Contribution to journal › Article › peer-review

Open Access
Formal Verification of Masked Hardware Implementations in the Presence of Glitches
Bloem, R., Groß, H., Iusupov, R., Könighofer, B., Mangard, S. & Winter, J., 2018, EUROCRYPT . Springer, Vol. 10821. p. 321-353 33 p. (Lecture Notes in Computer Science).
Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Open Access
File
SIFA: Exploiting Ineffective Fault Inductions on Symmetric Cryptography
Dobraunig, C. E., Eichlseder, M., Korak, T., Mangard, S., Mendel, F. & Primas, R., 2018, In: IACR Transactions on Cryptographic Hardware and Embedded Systems. 2018, 3, p. 547-572
Research output: Contribution to journal › Article › peer-review

Open Access

Cite this

Proving SIFA Protection of Masked Redundant Circuits. / Hadžić, Vedad; Primas, Robert; Bloem, Roderick.
Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021. ed. / Z. Hou; V. Ganesh. Cham: Springer, 2021. p. 249-265 (Lecture Notes in Computer Science; Vol. 12971).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Hadžić, V, Primas, R & Bloem, R 2021, Proving SIFA Protection of Masked Redundant Circuits. in Z Hou & V Ganesh (eds), Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021. Lecture Notes in Computer Science, vol. 12971, Springer, Cham, pp. 249-265, 19th International Symposium on Automated Technology for Verification and Analysis , Virtuell, Australia, 18/10/21. https://doi.org/10.1007/978-3-030-88885-5_17

@inproceedings{32e5cd47adba49c2a3bf949d7af88006,

title = "Proving SIFA Protection of Masked Redundant Circuits",

abstract = "Implementation attacks like side-channel and fault attacks pose a considerable threat to cryptographic devices that are physically accessible by an attacker. As a consequence, devices like smart cards implement corresponding countermeasures like redundant computation and masking. Recently, statistically ineffective fault attacks (SIFA) were shown to be able to circumvent these classical countermeasure techniques. We present a new approach for verifying the SIFA protection of arbitrary masked implementations in both hardware and software. The proposed method uses Boolean dependency analysis, factorization, and known properties of masked computations to show whether the fault detection mechanism of redundant masked circuits can leak information about the processed secret values. We implemented this new method in a tool called Danira, which can show the SIFA resistance of cryptographic implementations like AES S-Boxes within minutes.",

keywords = "SIFA, verification, hardware security",

author = "Vedad Had{\v z}i{\'c} and Robert Primas and Roderick Bloem",

year = "2021",

doi = "10.1007/978-3-030-88885-5\_17",

language = "English",

isbn = "978-3-030-88884-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "249--265",

editor = "Hou, \{ Z.\} and V. Ganesh",

booktitle = "Automated Technology for Verification and Analysis",

address = "United States",

note = "19th International Symposium on Automated Technology for Verification and Analysis : ATVA 2021, ATVA 2021 ; Conference date: 18-10-2021 Through 22-10-2021",

}

TY - GEN

T1 - Proving SIFA Protection of Masked Redundant Circuits

AU - Hadžić, Vedad

AU - Primas, Robert

AU - Bloem, Roderick

PY - 2021

Y1 - 2021

N2 - Implementation attacks like side-channel and fault attacks pose a considerable threat to cryptographic devices that are physically accessible by an attacker. As a consequence, devices like smart cards implement corresponding countermeasures like redundant computation and masking. Recently, statistically ineffective fault attacks (SIFA) were shown to be able to circumvent these classical countermeasure techniques. We present a new approach for verifying the SIFA protection of arbitrary masked implementations in both hardware and software. The proposed method uses Boolean dependency analysis, factorization, and known properties of masked computations to show whether the fault detection mechanism of redundant masked circuits can leak information about the processed secret values. We implemented this new method in a tool called Danira, which can show the SIFA resistance of cryptographic implementations like AES S-Boxes within minutes.

AB - Implementation attacks like side-channel and fault attacks pose a considerable threat to cryptographic devices that are physically accessible by an attacker. As a consequence, devices like smart cards implement corresponding countermeasures like redundant computation and masking. Recently, statistically ineffective fault attacks (SIFA) were shown to be able to circumvent these classical countermeasure techniques. We present a new approach for verifying the SIFA protection of arbitrary masked implementations in both hardware and software. The proposed method uses Boolean dependency analysis, factorization, and known properties of masked computations to show whether the fault detection mechanism of redundant masked circuits can leak information about the processed secret values. We implemented this new method in a tool called Danira, which can show the SIFA resistance of cryptographic implementations like AES S-Boxes within minutes.

KW - SIFA

KW - verification

KW - hardware security

U2 - 10.1007/978-3-030-88885-5_17

DO - 10.1007/978-3-030-88885-5_17

M3 - Conference paper

SN - 978-3-030-88884-8

T3 - Lecture Notes in Computer Science

SP - 249

EP - 265

BT - Automated Technology for Verification and Analysis

A2 - Hou, Z.

A2 - Ganesh, V.

PB - Springer

CY - Cham

T2 - 19th International Symposium on Automated Technology for Verification and Analysis

Y2 - 18 October 2021 through 22 October 2021

ER -

Proving SIFA Protection of Masked Redundant Circuits

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Projects

FERMION - Formal Verification of Masked Hardware Implementations

Dessnet - Dependable, secure and time-aware sensor networks

Research output

Proving SIFA protection of masked redundant circuits

Formal Verification of Masked Hardware Implementations in the Presence of Glitches

SIFA: Exploiting Ineffective Fault Inductions on Symmetric Cryptography

Cite this