Skip to content
/ vale Public
forked from project-everest/vale

Verified Assembly Language for Everest

License

Notifications You must be signed in to change notification settings

mamonet/vale

 
 

Repository files navigation

Vale (Verified Assembly Language for Everest)

Vale is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool.

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 the repository.

Documentation

See the Vale documentation for a description of the Vale language and Vale tool.

You can also see our academic papers describing Vale:

Projects using Vale

For cryptography implementations verified with Vale/F*, see HACL*.
For cryptography implementations verified with Vale/Dafny, see the Dafny legacy branch.
For the Komodo secure enclave reference monitor, see here and here.

License

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

Version History

  • 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.

About

Verified Assembly Language for Everest

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • F# 50.1%
  • Dafny 13.9%
  • F* 8.9%
  • Python 8.1%
  • Boogie 6.9%
  • C# 6.6%
  • Other 5.5%