Vale: Verifying High-Performance Cryptographic Assembly Code

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 provencorrect code before being extracted into standard assembly. For example, we have developed a novel, provencorrect 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. errors to improve usability. Figures in these subsections present examples of Dafny and Vale code. Although the syntax for both languages is similar, Vale's syntax (see appendix) is independent from Dafny's syntax; the figure captions specify the language of each code snippet. Dafny declarations