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

Conference Day
Fri 18 Jan

Displayed time zone: Belfast change

16:37 - 17:43
Verified Compilation and ConcurrencyResearch Papers at Sala I
Chair(s): Michael GreenbergPomona College
16:37
22m
Talk
A Calculus for Esterel: If can, can. If no can, no can.
Research Papers
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 Media Attached File Attached
16:59
22m
Talk
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Research Papers
Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University
Link to publication DOI Media Attached File Attached
17:21
22m
Talk
A Verified, Efficient Embedding of a Verifiable Assembly Language
Research Papers
Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication DOI Media Attached File Attached