Vale: Verifying High-Performance Cryptographic Assembly Code

Authors: 

Barry Bond and Chris Hawblitzel, Microsoft Research; Manos Kapritsos, University of Michigan; K. Rustan M. Leino and Jacob R. Lorch, Microsoft Research; Bryan Parno, Carnegie Mellon University; Ashay Rane, The University of Texas at Austin; Srinath Setty, Microsoft Research; Laure Thompson, Cornell University
Distinguished Paper Award Winner!

Abstract: 

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.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {203642,
author = {Barry Bond and Chris Hawblitzel and Manos Kapritsos and K. Rustan M. Leino and Jacob R. Lorch and Bryan Parno and Ashay Rane and Srinath Setty and Laure Thompson},
title = {Vale: Verifying High-Performance Cryptographic Assembly Code},
booktitle = {26th {USENIX} Security Symposium ({USENIX} Security 17)},
year = {2017},
isbn = {978-1-931971-40-9},
address = {Vancouver, BC},
pages = {917--934},
url = {https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/bond},
publisher = {{USENIX} Association},
}