International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News item: 05 August 2012

Sébastien Briais, Sylvain Guilley, Jean-Luc Danger
ePrint Report ePrint Report
Secure electronic circuits must implement countermeasures against a wide range of attacks.

Often, the protection against side channel attacks requires to be tightly integrated within the functionality to be protected.

It is now part of the designer\'s job to implement them.

But this task is known to be error-prone, and with current development processes, countermeasures are evaluated often very late (at circuit fabrication).

In order to improve the confidence of the designer in the efficiency of the countermeasure,

we suggest in this article to resort to formal methods early in the design flow for two reasons.

First of all, we intend to check that the process of transformation of the design from the vulnerable description to the protected one does not alter the functionality.

Second, we wish to prove that the security properties (that can derive from a formal security functional specification) are indeed met after transformation.

Our first contribution is to show how such a framework can be setup (in COQ) for netlist-level protections.

The second contribution is to illustrate that this framework indeed allows to detect vulnerabilities in dual-rail logics.

Expand

Additional news items may be found on the IACR news page.