Paper 2009/322

Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS

Reynald Affeldt, David Nowak, and Kiyoshi Yamada

Abstract

With today's dissemination of embedded systems manipulating sensitive data, it has become important to equip low-level programs with strong security guarantees. Unfortunately, security proofs as done by cryptographers are about algorithms, not about concrete implementations running on hardware. In this paper, we show how to extend security proofs to guarantee the security of assembly implementations of cryptographic primitives. Our approach is based on a framework in the Coq proof-assistant that integrates correctness proofs of assembly programs with game-playing proofs of provable security. We demonstrate the usability of our approach using the Blum-Blum-Shub (BBS) pseudorandom number generator, for which a MIPS implementation for smartcards is shown cryptographically secure.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. An updated version appears in Automated Verification of Critical Systems 2009, volume 23 of Electronic Communications of the EASST
Keywords
Hoare logicSmartMIPSCoqPRNGprovable securitygame playing
Contact author(s)
david nowak @ aist go jp
History
2010-05-13: last of 2 revisions
2009-07-01: received
See all versions
Short URL
https://ia.cr/2009/322
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2009/322,
      author = {Reynald Affeldt and David Nowak and Kiyoshi Yamada},
      title = {Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS},
      howpublished = {Cryptology ePrint Archive, Paper 2009/322},
      year = {2009},
      note = {\url{https://eprint.iacr.org/2009/322}},
      url = {https://eprint.iacr.org/2009/322}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.