A Verified, Efficient Embedding of a Verifiable Assembly Language
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.
Slides (Vale-popl19.pdf) | 448KiB |
Fri 18 Jan
16:37 - 17:43: Research Papers - Verified Compilation and Concurrency at Sala I Chair(s): Michael GreenbergPomona College | ||||||||||||||||||||||||||||||||||||||||||
16:37 - 16:59 Talk | Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Jesse A. TovNorthwestern University, Department of Electrical Engineering and Computer Science, Robby FindlerNorthwestern University, USA Link to publication DOI File Attached | |||||||||||||||||||||||||||||||||||||||||
16:59 - 17:21 Talk | Link to publication DOI File Attached | |||||||||||||||||||||||||||||||||||||||||
17:21 - 17:43 Talk | Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research Link to publication DOI File Attached |