You are looking at a specific version 20140926:152323 of this paper. See the latest version.

Paper 2013/554

Formally Proved Security of Assembly Code Against Power Analysis: A Case Study on Balanced Logic

Pablo Rauzy and Sylvain Guilley and Zakaria Najm

Abstract

In his keynote speech at CHES 2004, Kocher advocated that side-channel attacks were an illustration that formal cryptography was not as secure as it was believed because some assumptions (e.g., no auxiliary information is available during the computation) were not modeled. This failure is caused by formal methods' focus on models rather than implementations. In this paper we present formal methods and tools for designing protected code and proving its security against power analysis. These formal methods avoid the discrepancy between the model and the implementation by working on the latter rather than on a high-level model. Indeed, our methods allow us (a) to automatically insert a power balancing countermeasure directly at the assembly level, and to prove the correctness of the induced code transformation; and (b) to prove that the obtained code is balanced with regard to a reasonable leakage model, and we show how to characterize the hardware to use the resources which maximize the relevancy of the model. The tools implementing our methods are then demonstrated in a case study in which we generate a provably protected PRESENT implementation for an 8-bit AVR smartcard.

Note: This version of the paper will be presented at PROOFS 2014.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. PROOFS 2014
Keywords
Dual-railDPAformal proofstatic analysissymbolic executionimplementationsmartcardPRESENTblock cipherHamming distanceOCaml
Contact author(s)
rauzy @ enst fr
History
2015-06-21: last of 7 revisions
2013-09-04: received
See all versions
Short URL
https://ia.cr/2013/554
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.