Revision 6807cc0db50338532fbe805f58509f365da751a2 authored by Santiago Zanella-Beguelin on 05 November 2019, 13:23:49 UTC, committed by Santiago Zanella-Beguelin on 05 November 2019, 14:45:37 UTC
1 parent 28f131a
README.Vale.md
Vale (Verified Assembly Language for Everest) <br>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](https://github.com/project-everest/vale) to produce
code and proofs in [F\*](https://github.com/FStarLang/FStar).
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](https://project-everest.github.io),
which aims to build and deploy a verified HTTPS stack.
# Installation
See the [INSTALL](./vale/INSTALL.md) file for installing Vale and its dependencies.
# Code Organization
See the [CODE](./vale/CODE.md) 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](https://project-everest.github.io/assets/vale2017.pdf)
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](https://www.microsoft.com/en-us/research/publication/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](./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.
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...