1. Vale: Verifying High-Performance Cryptographic Assembly Code 2017 Implementation Usenix
    Barry Bond and Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson
    [View PDF on usenix.org]
    [Show BibTex Citation]

    @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},

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.