@inproceedings{fromherz2019a,
author = {Fromherz, Aymeric and Giannarakis, Nick and Hawblitzel, Chris and Parno, Bryan and Rastogi, Aseem and Swamy, Nikhil},
title = {A Verified, Efficient Embedding of a Verifiable Assembly Language},
booktitle = {Principles of Programming Languages (POPL 2019)},
year = {2019},
month = {January},
abstract = {High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system’s type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90% of secure Internet traffic.},
publisher = {ACM},
url = {http://approjects.co.za/?big=en-us/research/publication/a-verified-efficient-embedding-of-a-verifiable-assembly-language/},
}