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

Displayed time zone: Belfast change

16:37 - 17:43
Verified Compilation and ConcurrencyResearch Papers at Sala I
Chair(s): Michael Greenberg Pomona College
16:37
22m
Talk
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, Robert Bruce Findler Northwestern 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 Wang Yale University, Pierre Wilke Yale University, Zhong Shao Yale 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 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