Paper 2013/554
Formally Proved Security of Assembly Code Against Power Analysis
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. 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.
Note: This is a new (almost entirely rewritten) version of this paper. There are still TODOs left in it as it is a work-in-progress.
Metadata
- Available format(s)
- Category
- Implementation
- Publication info
- Preprint. MINOR revision.
- Keywords
- DPLDPAformal proofstatic analysissymbolic executionblock cipherPRESENTAVR
- 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
-
CC BY