43 lines
1.8 KiB
Markdown
43 lines
1.8 KiB
Markdown
---
|
||
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 ⏳ 2025-02-28 📅 2025-02-28 ❌ 2025-03-10
|
||
|
||
>[!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
|