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, with the examples of wave differential dynamic logic (WDDL) and balanced cell-based differential logic (BCDL).
Category / Keywords: implementation / implementation, smart cards Publication Info: Accepted for publication at PROOFS 2012 and in JCEN 2013 Date: received 30 Jul 2012, last revised 3 Apr 2013 Contact author: sylvain guilley at TELECOM-ParisTech fr Available format(s): PDF | BibTeX Citation Note: Extended version of PROOFS 2012 (<a href="http://perso.telecom-paristech.fr/guilley/proofs_2012/program.html">paper and slides</a>). <br /> <br /> Preliminary version, without COQ code examples, of JCEN 2013 (<a href="http://dx.doi.org/10.1007/s13389-013-0054-6">on-line document at Springer</a>). Version: 20130403:213458 (All versions of this report) Short URL: ia.cr/2012/430 Discussion forum: Show discussion | Start new discussion