Vale: Verifying High-Performance Cryptographic Assembly Code

Proceedings of the USENIX Security Symposium |

Published by USENIX

High-performance cryptographic code often relies on complex hand-tuned assembly language that is customized for individual hardware platforms. Such code is difficult to understand or analyze. We introduce a new programming language and tool called Vale that supports flexible, automated verification of high-performance assembly code. The Vale tool transforms annotated assembly language into an abstract syntax tree (AST), while also generating proofs about the AST that are verified via an SMT solver. Since the AST is a first-class proof term, it can be further analyzed and manipulated by proven-correct code before being extracted into standard assembly. For example, we have developed a novel, proven-correct taint-analysis engine that verifies the code’s freedom from digital side channels. Using these tools, we verify the correctness, safety, and security of implementations of SHA-256 on x86 and ARM, Poly1305 on x64, and hardware-accelerated AES-CBC on x86. Several implementations meet or beat the performance of unverified, state-of-the-art cryptographic libraries.

Téléchargements de publications

EverCrypt

juin 26, 2019

EverCrypt is a high-performance, cross-platform, formally verified modern cryptographic provider distributed as a combined C/ASM library. EverCrypt packages cryptographic implementations from the HACL* and ValeCrypt projects, and automatically picks the fastest one available, depending on processor support and the target execution environment (multiplexing). Furthermore, EverCrypt offers an (agile) API that makes it simple to switch between algorithms (e.g., from SHA2 to SHA3). Code from EverCrypt has been integrated in Linux, Firefox, the Tezos blockchain, the Election Guard project, and many more.

Vale

juin 26, 2019

Vale (Verified Assembly Language for Everest) is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code.  It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux.  Additional architectures and platforms can be supported with no changes to the Vale tool. The Everest project uses Vale to provide verified assembly language code for performance-critical cryptographic algorithms, including AES-GCM, Curve25519, Poly1305, and SHA.  Everest's EverCrypt API automatically chooses between Vale's assembly language code and HACL*'s C code depending on the cryptographic algorithm and the machine the code is running on.