Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS

Reynald Affeldt, David Nowak, Kiyoshi Yamada


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 concreteimplementations running on hardware. In this paper, we show how to perform security proofs to guarantee the security of assembly language 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.

Full Text:


DOI: http://dx.doi.org/10.14279/tuj.eceasst.23.316

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.23.316.302

Hosted By Universit├Ątsbibliothek TU Berlin.