Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 17:21 - 17:43 at Sala I - Verified Compilation and Concurrency Chair(s): Michael Greenberg

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
POPL-2019-Research-Papers16:37 - 16:59
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
POPL-2019-Research-Papers16:59 - 17:21
Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University
Link to publication DOI File Attached
POPL-2019-Research-Papers17:21 - 17:43
Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication DOI File Attached