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] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Security Proofs: the Case of BBS. Science of Computer Programming, in press, Elsevier, 2011. doi.
which is an improved version of:
[2] ---. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. In Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems (AVoCS 2009), September 23-25, 2009. pdf.

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 (July, 2011): certifying_bbs.tar.gz (requirement: SSReflect-1.3pl1 for Coq-8.3pl1).
  • Older version (January, 14 2011): certifying_bbs.14012011.tar.gz (requirements: SSReflect-1.2 and Coq-8.3);
    Installation: Edit vars.mk so that ROOT and SSRLIB point to appropriate files. Do make all (COQBIN better not be set).
• Online documentation: framework for assembly code, 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 above paper [2], the formal security proof of BBS in assembly can be summarized by the figure on the right. Here are links to the relevant files: BBS_Asm_CryptoProof.v. bbs_encode_decode.v, bbs_triple.v, bbs_termination.v, and bbs_prg.v. BBS.v.

Compilation and Execution of BBS in SmartMIPS Assembly

• From abstract to concrete syntax.
• From the bbs snippet to a runnable program.
• How to set up a cross-compilation environment with the GDB simulator.