You are looking at a specific version 20130904:142054 of this paper. See the latest version.

Paper 2013/554

Formally Proved Security of Assembly Code Against Leakage

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 due to the fact that formal methods work with models rather than implementations. Of course, we can use formal methods to prove non-functional security properties such as the absence of side-channel leakages. But a common obstacle is that those properties are very low-level and appear incompatible with formalization. To avoid the discrepancy between the model and the implementation, we apply formal methods directly on the implementation. Doing so, we can formally prove that an assembly code is leak-free, provided that the hardware it runs on satisfies a finite (and limited) set of properties that we show are realistic. We apply this technique to prove that a PRESENT implementation in 8~bit AVR assembly code is leak-free.

Note: This paper is an early draft version of a work presented during the poster session at CHES 2013.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint. MINOR revision.
Keywords
side-channelsbalancing countermeasureformal methodssymbolic evaluation
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.