A verified, efficient embedding of a verifiable assembly language
| Autor: | Aseem Rastogi, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Nikhil Swamy, Nick Giannarakis |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
0303 health sciences
Domain-specific language Correctness Assembly language Computer science Programming language business.industry 020207 software engineering Cryptography 02 engineering and technology computer.software_genre Dependent type 03 medical and health sciences Interoperation Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering Code (cryptography) Safety Risk Reliability and Quality business computer Software 030304 developmental biology computer.programming_language |
| Zdroj: | Proceedings of the ACM on Programming Languages. 3:1-30 |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3290376 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|