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:
- Science of Computer Programming article which is an improved version of:
- 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.
- Formalization:
- Last version : on github
- requirements: Coq-8.7.1, Mathcomp-1.7.0
- Older version : certifying_bbs.tar.gz
- requirements: Coq-8.7.0, Mathcomp-1.6.2
- Installation: see the file
BBSINSTALLin the root directory
- Last version : on github
- Online documentation:
- framework for assembly code (look at "cryptoasm")
- framework for security proofs
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:
