Certifying assembly with formal security proofs: The case of BBS

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 article, 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 pseudorandom number generator, for which an MIPS implementation for smartcards is shown cryptographically secure.

► We formally verify the provably-secure Blum–Blum–Shub pseudorandom number generator. ► We deal with a concrete implementation in assembly code for smartcards (SmartMIPS). ► Our verification comprises both the functional correctness and the security proof. ► The integration is articulated in terms of the game-playing methodology. ► The experiment is supported by a reusable library for the Coq proof assistant.