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 JanDisplayed time zone: Belfast change
16:37 - 17:43 | Verified Compilation and ConcurrencyResearch Papers at Sala I Chair(s): Michael Greenberg Pomona College | ||
16:37 22mTalk | A Calculus for Esterel: If can, can. If no can, no can. Research Papers Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Jesse A. Tov Northwestern University, Department of Electrical Engineering and Computer Science, Robby Findler Northwestern University, USA Link to publication DOI Media Attached File Attached | ||
16:59 22mTalk | An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code Research Papers Link to publication DOI Media Attached File Attached | ||
17:21 22mTalk | A Verified, Efficient Embedding of a Verifiable Assembly Language Research Papers Aymeric Fromherz Carnegie Mellon University, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Bryan Parno , Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research Link to publication DOI Media Attached File Attached |