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

Institute of Information Security (7050)

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

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.

Original language	English
Title of host publication	Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021
Editors	Ruzica Piskac, Michael W. Whalen, Warren A. Hunt, Georg Weissenbacher
Pages	14-23
Number of pages	10
ISBN (Electronic)	978-3-85448-046-4
DOIs	https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_9
Publication status	Published - 9 Jul 2021
Event	21st International Conference on Formal Methods in Computer-Aided Design: FMCAD 2021 - Online, Virtuell, Austria Duration: 18 Oct 2021 → 22 Oct 2021 https://fmcad.org/FMCAD21/

Publication series

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

Conference

Conference	21st International Conference on Formal Methods in Computer-Aided Design
Abbreviated title	FMCAD 2021
Country/Territory	Austria
City	Virtuell
Period	18/10/21 → 22/10/21
Internet address	https://fmcad.org/FMCAD21/

Keywords

Side Channels
Hardware Masking
Formal Verification
Side-channels
Hardware masking
Formal verification

ASJC Scopus subject areas

Safety, Risk, Reliability and Quality
Computer Graphics and Computer-Aided Design

Access to Document

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

paperAccepted author manuscript, 329 KB

Cite this

CocoAlma: A Versatile Masking Verifier. / Hadzic, Vedad; Bloem, Roderick.
Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021. ed. / Ruzica Piskac; Michael W. Whalen; Warren A. Hunt; Georg Weissenbacher. 2021. p. 14-23 (Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021).

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

Hadzic, V & Bloem, R 2021, CocoAlma: A Versatile Masking Verifier. in R Piskac, MW Whalen, WA Hunt & G Weissenbacher (eds), Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021. Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021, pp. 14-23, 21st International Conference on Formal Methods in Computer-Aided Design, Virtuell, Austria, 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

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

FERMION - Formal Verification of Masked Hardware Implementations

Power Contracts: Provably Complete Power Leakage Models for Processors

Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs

Formal Verification of Masked Hardware Implementations in the Presence of Glitches

Cite this

CocoAlma: A Versatile Masking Verifier

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

FERMION - Formal Verification of Masked Hardware Implementations

Research output

Power Contracts: Provably Complete Power Leakage Models for Processors

Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs

Formal Verification of Masked Hardware Implementations in the Presence of Glitches

Cite this