Cryptology ePrint Archive: Report 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. We then demonstrate our methods in a case study in which we generate a provably protected PRESENT implementation for an 8-bit AVR smartcard.

Category / Keywords: Implementation / Dual-rail, DPA, formal proof, static analysis, symbolic execution, implementation, smartcard, PRESENT, block cipher, Hamming distance, OCaml

Date: received 3 Sep 2013, last revised 5 Mar 2014

Contact author: rauzy at enst fr

Available format(s): PDF | BibTeX Citation

Note: This is an almost final version of this paper.

Version: 20140305:133152 (All versions of this report)

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]