vale-crypto

Vale Crypto in libcrux

##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. Each assembly implementation in Vale is verified for:

• Memory Safety in the x86 memory model
• Functional Correctness against a formal specification written in F* or Dafny
• Secret Independence, i.e. that control flow and memory accesses do not depend on secrets

Vale Crypto includes verified Intel assembly implementations of AES-GCM, SHA-2, Poly1305, and the field arithmetic used in Curve25519

Vale Algorithms in libcrux

The libcrux library currently uses the following verified implementations from Vale:

• AES-GCM - Intel AES-NI

Verifying Vale* and Generating Intel assembly

We pull code from the HACL* repository and run the verification on the whole repository using the provided Makefile. The build depends upon F* and Vale. Once all the code is verified, the generated assembly code and C header files are taken from dist/.

Wrapping the Vale C APIs within Rust

For each algorithm we import into libcrux, we inspect the high-level verified APIs provided by Vale and reflect the correct types and pre-conditions in the libcrux Rust APIs. This is a manual process and is carefully reviewed by multiple developers. We include pointers to the formal specs, the F* APIs, and the C APIs for all the algorithms we use in libcrux:

• AES-GCM - Spec, F* API, C API

Spec Equivalence between Hacspec and Vale

We can formally relate crypo specification in hacspec to those used by HACL*, by first compiling the hacspec to F* and then proving that the two specifications are equivalent in F*. At this time we have not proved spec equivalence between the two AES-GCM specs.

References

Vale and its associated proof methodologies have been published in the following papers:

• 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.
• Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
  Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel. In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) 2020.