A Verified, Efficient Embedding of a Verifiable Assembly Language

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2019
Accession Number
AD1105410

Entities

People

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

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Assembly Languages
  • Case Studies
  • Coding
  • Computer Programming
  • Computer Programs
  • Computers
  • Construction
  • Cryptography
  • Kernels (Operating System)
  • Language
  • New York
  • Operating Systems
  • Programming Languages
  • Simulations
  • Systems Engineering

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Computational Fluid Dynamics (CFD)
  • Computational Linguistics
  • Cybersecurity.