---
readstatus: false
dateread:
title: "A verified, efficient embedding of a verifiable assembly language"
year: 2019
authors:

  - "Fromherz, Aymeric"
  
  - "Giannarakis, Nick"
  
  - "Hawblitzel, Chris"
  
  - "Parno, Bryan"
  
  - "Rastogi, Aseem"
  
  - "Swamy, Nikhil"
  citekey: "fromherzVerifiedEfficientEmbedding2019"
journal: "Source code for Article: A Verified, Efficient Embedding of A Verifiable Assembly Language"
volume: 3
issue: POPL
pages: 63:1–63:30
---
# Indexing Information
## DOI
[10.1145/3290376](https://doi.org/10.1145/3290376)
## Tags:


- ["] A verified, efficient embedding of a verifiable assembly language #Reading 

>[!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 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.>[!seealso] Related Papers
>

# Annotations
## Notes

## Follow-Ups

### Imported: 2025-02-14 5:57 pm