CocoAlma: A Versatile Masking Verifier

Vedad Hadzic; Roderick Bloem

doi:10.34727/2021/isbn.978-3-85448-046-4_9

CocoAlma: A Versatile Masking Verifier

Vedad Hadzic, Roderick Bloem

Institut für Angewandte Informationsverarbeitung und Kommunikationstechnologie (7050)

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

Abstract

Masking techniques are an effective countermeasure against power side-channel attacks.
Unfortunately, correctly masking a hardware circuit is difficult, and mistakes may lead to functionally correct circuits with insufficient protection.
We present CocoAlma, a tool that formally verifies the side-channel resistance of stateful hardware circuits.
Although CocoAlma was initially used to verify programs running on CPUs, we extended it to verify the security of several industrial masked hardware implementations.
We give an overview of the tool's structure, implementation details, optimizations that make it faster and more scalable than its predecessor Rebecca, and changes that enable verifying the probing security of any stateful hardware circuit.
Finally, we evaluate CocoAlma with masked implementations of the Prince and AES ciphers.

Originalsprache	englisch
Titel	Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021
Redakteure/-innen	Ruzica Piskac, Michael W. Whalen, Warren A. Hunt, Georg Weissenbacher
Seiten	14-23
Seitenumfang	10
ISBN (elektronisch)	978-3-85448-046-4
DOIs	https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_9
Publikationsstatus	Veröffentlicht - 9 Juli 2021
Veranstaltung	21st International Conference on Formal Methods in Computer-Aided Design: FMCAD 2021 - Online, Virtuell, Österreich Dauer: 18 Okt. 2021 → 22 Okt. 2021 https://fmcad.org/FMCAD21/

Publikationsreihe

Name	Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021

Konferenz

Konferenz	21st International Conference on Formal Methods in Computer-Aided Design
Kurztitel	FMCAD 2021
Land/Gebiet	Österreich
Ort	Virtuell
Zeitraum	18/10/21 → 22/10/21
Internetadresse	https://fmcad.org/FMCAD21/

ASJC Scopus subject areas

Sicherheit, Risiko, Zuverlässigkeit und Qualität
Computergrafik und computergestütztes Design

Zugriff auf Dokument

10.34727/2021/isbn.978-3-85448-046-4_9Lizenz: CC BY 4.0

paperAkzeptiertes Autorenmanuskript, 329 KB

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

1 Abgeschlossen

FERMION - Formale Verifizierung maskierter Hardware-Implementierungen
Bloem, R.
2/01/19 → 1/01/22
Projekt: Foschungsprojekt

Dieses zitieren

CocoAlma: A Versatile Masking Verifier. / Hadzic, Vedad ; Bloem, Roderick.

Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021. Hrsg. / Ruzica Piskac; Michael W. Whalen; Warren A. Hunt; Georg Weissenbacher. 2021. S. 14-23 (Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

Hadzic, V & Bloem, R 2021, CocoAlma: A Versatile Masking Verifier. in R Piskac, MW Whalen, WA Hunt & G Weissenbacher (Hrsg.), Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021. Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021, S. 14-23, 21st International Conference on Formal Methods in Computer-Aided Design, Virtuell, Österreich, 18/10/21. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_9

@inproceedings{48d7ed22f18d493f81ea467708ccd1d2,

title = "CocoAlma: A Versatile Masking Verifier",

abstract = "Masking techniques are an effective countermeasure against power side-channel attacks.Unfortunately, correctly masking a hardware circuit is difficult, and mistakes may lead to functionally correct circuits with insufficient protection.We present CocoAlma, a tool that formally verifies the side-channel resistance of stateful hardware circuits. Although CocoAlma was initially used to verify programs running on CPUs, we extended it to verify the security of several industrial masked hardware implementations.We give an overview of the tool's structure, implementation details, optimizations that make it faster and more scalable than its predecessor Rebecca, and changes that enable verifying the probing security of any stateful hardware circuit.Finally, we evaluate CocoAlma with masked implementations of the Prince and AES ciphers.",

keywords = "Side Channels, Hardware Masking, Formal Verification, Side-channels, Hardware masking, Formal verification",

author = "Vedad Hadzic and Roderick Bloem",

year = "2021",

month = jul,

day = "9",

doi = "10.34727/2021/isbn.978-3-85448-046-4_9",

language = "English",

series = "Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021",

pages = "14--23",

editor = "Ruzica Piskac and Whalen, {Michael W.} and Hunt, {Warren A.} and Georg Weissenbacher",

booktitle = "Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021",

note = "21st International Conference on Formal Methods in Computer-Aided Design : FMCAD 2021, FMCAD 2021 ; Conference date: 18-10-2021 Through 22-10-2021",

url = "https://fmcad.org/FMCAD21/",

}

TY - GEN

T1 - CocoAlma: A Versatile Masking Verifier

AU - Hadzic, Vedad

AU - Bloem, Roderick

PY - 2021/7/9

Y1 - 2021/7/9

N2 - Masking techniques are an effective countermeasure against power side-channel attacks.Unfortunately, correctly masking a hardware circuit is difficult, and mistakes may lead to functionally correct circuits with insufficient protection.We present CocoAlma, a tool that formally verifies the side-channel resistance of stateful hardware circuits. Although CocoAlma was initially used to verify programs running on CPUs, we extended it to verify the security of several industrial masked hardware implementations.We give an overview of the tool's structure, implementation details, optimizations that make it faster and more scalable than its predecessor Rebecca, and changes that enable verifying the probing security of any stateful hardware circuit.Finally, we evaluate CocoAlma with masked implementations of the Prince and AES ciphers.

AB - Masking techniques are an effective countermeasure against power side-channel attacks.Unfortunately, correctly masking a hardware circuit is difficult, and mistakes may lead to functionally correct circuits with insufficient protection.We present CocoAlma, a tool that formally verifies the side-channel resistance of stateful hardware circuits. Although CocoAlma was initially used to verify programs running on CPUs, we extended it to verify the security of several industrial masked hardware implementations.We give an overview of the tool's structure, implementation details, optimizations that make it faster and more scalable than its predecessor Rebecca, and changes that enable verifying the probing security of any stateful hardware circuit.Finally, we evaluate CocoAlma with masked implementations of the Prince and AES ciphers.

KW - Side Channels

KW - Hardware Masking

KW - Formal Verification

KW - Side-channels

KW - Hardware masking

KW - Formal verification

UR - http://www.scopus.com/inward/record.url?scp=85123699523&partnerID=8YFLogxK

U2 - 10.34727/2021/isbn.978-3-85448-046-4_9

DO - 10.34727/2021/isbn.978-3-85448-046-4_9

M3 - Conference paper

T3 - Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021

SP - 14

EP - 23

BT - Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021

A2 - Piskac, Ruzica

A2 - Whalen, Michael W.

A2 - Hunt, Warren A.

A2 - Weissenbacher, Georg

T2 - 21st International Conference on Formal Methods in Computer-Aided Design

Y2 - 18 October 2021 through 22 October 2021

ER -

CocoAlma: A Versatile Masking Verifier

Abstract

Publikationsreihe

Konferenz

ASJC Scopus subject areas

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Projekte

FERMION - Formale Verifizierung maskierter Hardware-Implementierungen

Dieses zitieren