Verified Correctness and Security of mbedTLS HMAC-DRBG

We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic securitythat its output is pseudorandom-using a hybrid game-based proof. We have also proved that the mbedTLS implementation (C program) correctly implements this functional specification. at proof composes with an existing C compiler correctness proof to guarantee, end-to-end, that the machine language program gives strong pseudorandomness. All proofs (hybrid games, C program verification, compiler, and their composition) are machine-checked in the Coq proof assistant. Our proofs are modular: the hybrid game proof holds on any implementation of HMAC-DRBG that satisfies our functional specification. erefore, our functional specification can serve as a high-assurance reference. 1 A note on terminology: we use "entropy" loosely to denote randomness that is not predictable by an adversary. We use "sampled uniformly at random" and "ideally random" interchangeably. We use PRG, the acronym for "pseudo-random generator," to refer to the abstract cryptographic concept, whereas we use DRBG, the acronym for "deterministic random bit generator," to denote the specifications and implementations of PRGs. Instead of DRBG, some papers use "PRNG," the acronym for "pseudorandom number generator." e terms are synonymous.