Welcome to the resource topic for 2025/1882
Title:
MATCHI: formal verification of hardware private circuits
Authors: Gaëtan Cassiers
Abstract:Hardware Private Circuits (HPC) provide a compositional framework for designing masked hardware circuits, ensuring security against side-channel attacks in the robust probing model with glitches and transitions. There is however a gap between the simplified circuit models and real-world implementations. In particular, some parts are of real circuits are ignored in the simplified models. Further, designing implementations such that they have a simple static correspondence to the theory can be challenging (e.g., around the requirement of splitting the computation into gadgets), or even infeasible (e.g., when some hardware elements like memory are used for different purposes during the executions). In this work, we close this gap by introducing a new model for hardware circuits that include the control and randomness distribution logic. It also allows some computation on the shares to be performed outside the delimited gadgets. We introduce a new open-source compositional masking verification tool, MATCHI. Thanks to the formalization of a composition framework for the new circuit model, we prove that any circuit successfully verified by MATCHI is secure in the threshold probing model with glitches and transitions.
ePrint: https://eprint.iacr.org/2025/1882
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .