Vale (Verified Assembly Language for Everest)
Cryptographic Libraries

This directory contains the Vale cryptographic libraries, i.e., formally verified high-performance
cryptographic code in assembly language. They rely
on the Vale tool to produce
code and proofs in F*.

The code currently targets x64, but it will be expanded to support
other hardware platforms, such as x86 and ARM. Our toolchain
produces assembly that is suitable for Windows, Mac, and Linux,
and that is compatible with both MSVC and GCC based toolchains.

Vale is part of the Everest project,
which aims to build and deploy a verified HTTPS stack.

Installation

See the INSTALL file for installing Vale and its dependencies.

Code Organization

See the CODE file for more details on the various files in this directory.

Documentation

You can see our academic papers describing Vale:

• Vale: Verifying High-Performance Cryptographic Assembly Code
  Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson.
  In Proceedings of the USENIX Security Symposium, 2017.
  Distinguished Paper Award

• A Verified, Efficient Embedding of a Verifiable Assembly Language
  Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy. In Proceedings of the Symposium on Principles of Programming Languages (POPL), 2019.

License

Our Vale code is licensed under the Apache license in the LICENSE file.

Version History

• v0.2: Vale/F* code release.
• v0.1: Initial code release, containing code written by:
  Andrew Baumann, Barry Bond, Andrew Ferraiuolo, Chris Hawblitzel,
  Jon Howell, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch,
  Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson.