Verified Correctness and Security of mbedTLS HMAC-DRBG

TL;DR

This paper formalizes and proves the cryptographic security of HMAC-DRBG, verifies the correctness of the mbedTLS implementation, and ensures end-to-end security guarantees through machine-checked proofs in Coq.

Contribution

It provides the first formal, machine-checked proof of HMAC-DRBG's security and correctness, linking specifications, implementation, and compiler correctness.

Findings

Proved HMAC-DRBG's pseudorandomness using hybrid game-based proof.

Verified mbedTLS implementation matches the functional specification.

Ensured end-to-end security through composition of proofs in Coq.

Abstract

We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that 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. That 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. Therefore, our functional specification can serve as a high-assurance reference.