Projects per year
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.
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 | |
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 |
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
Fingerprint
Dive into the research topics of 'CocoAlma: A Versatile Masking Verifier'. Together they form a unique fingerprint.Projects
- 1 Finished
-
FERMION - Formal Verification of Masked Hardware Implementations
2/01/19 → 1/01/22
Project: Research project