Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
| Autor: | Chris Hawblitzel, Bryan Parno, Sydney Gibson, Yao Li, Jay Bosamiya |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
050101 languages & linguistics
Assembly language business.industry Computer science Programming language 05 social sciences Cryptography 02 engineering and technology Hoare logic Mathematical proof computer.software_genre 0202 electrical engineering electronic engineering information engineering Code (cryptography) 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences business computer computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030636173 VSTTE |
| Popis: | Hand-optimized assembly language code is often difficult to formally verify. This paper combines Hoare logic with verified code transformations to make it easier to verify such code. This approach greatly simplifies existing proofs of highly optimized OpenSSL-based AES-GCM cryptographic code. Furthermore, applying various verified transformations to the AES-GCM code enables additional platform-specific performance improvements. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|