Accession Number:

AD1105410

Title:

A Verified, Efficient Embedding of a Verifiable Assembly Language

Descriptive Note:

Journal Article - Open Access

Corporate Author:

Carnegie Mellon University Pittsburgh United States

Personal Author(s):

• Giannarakis,Nick
• Hawblitzel,Chris
• Parno,Bryan
• Rastogi,Aseem
• Swamy,Nikhil
• Fromherz,Aymeric

Report Date:

2019-01-01

Pagination or Media Count:

30.0

Abstract:

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 systems 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.

Descriptors:

• assembly languages
• cryptography
• computer programming
• automation
• cybersecurity
• programming languages
• embedded systems
• software development

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE