TY - GEN
T1 - Verified correctness and security of mbed TLS HMAC-DRBG
AU - Ye, Katherine Q.
AU - Green, Matthew
AU - Sanguansin, Naphat
AU - Beringer, Lennart
AU - Petcher, Adam
AU - Appel, Andrew W.
N1 - Publisher Copyright:
© 2017 author(s).
PY - 2017/10/30
Y1 - 2017/10/30
N2 - We have formalized the functional specication 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 specication. 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 satises our functional specication. Therefore, our functional specication can serve as a high-assurance reference.
AB - We have formalized the functional specication 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 specication. 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 satises our functional specication. Therefore, our functional specication can serve as a high-assurance reference.
UR - http://www.scopus.com/inward/record.url?scp=85041431806&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85041431806&partnerID=8YFLogxK
U2 - 10.1145/3133956.3133974
DO - 10.1145/3133956.3133974
M3 - Conference contribution
AN - SCOPUS:85041431806
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 2007
EP - 2020
BT - CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery
T2 - 24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017
Y2 - 30 October 2017 through 3 November 2017
ER -