Certifying Assembly with Formal Security Proofs: the Case of BBS

The purpose of this webpage is to provide the material of the certification of an assembly implementation of the BBS PRNG with its security proof.

The experiment is described in:

  1. Science of Computer Programming article which is an improved version of:
  2. AVoCS 2009 paper

Certification of assembly code with security proofs is made possible by a formal framework developed in the Coq proof-assistant; this framework results from the integration of two existing frameworks.

Put it All Together: Formal Security Proof of BBS in Assembly

As explained at the end of Section 5 in the AVoCS 2009 paper, the formal security proof of BBS in assembly can be summarized by the figure below. Here are links to the relevant files:


Compilation and Execution of BBS in SmartMIPS Assembly