At Real World Crypto 2023 in Tokyo, we gave a talk on the hacspec language, the hax tool, and the libcrux crypto library.
Designing and implementing cryptographic software is a perilous endeavor. Experts (like us) will tell you not to “roll your own crypto” and instead rely on standard mechanisms and well-vetted open-source implementations. Or else you take the risk of falling prey to embarrassing attacks, with dedicated logos, backronyms, and long-lived websites listing your design flaws and coding bugs. Of course, published standards and popular crypto libraries are not infallible, but the argument goes that at least you share their vulnerabilities and subsequent patches with a larger community of users.
If none of the existing cryptographic solutions will do the job, and you do need to build something new, you will be told to only consider solutions based on peer-reviewed research. But as anyone who has read papers from Crypto or EuroCrypt knows very well, there is always a large gap between academic results and deployable solutions. So, unless you are able to hire a cryptographer (or three) to interpret these papers and turn them into production-ready code, you are likely to struggle to find the answers to your particular problem.
This is why Real World Crypto (RWC) (no, not the Rugby World Cup) is one of my favorite conferences of the year. It brings together academic cryptographers with professional developers who implement cryptographic systems for a living. The conference has no proceedings, just three days of talks that are chosen as much for presentation quality as technical depth. RWC is where you go if you want your cryptographic research idea to be noticed by industry, or if you want to understand how the latest research may be relevant to your security product.
At Cryspen, we straddle the boundary between academic research and cryptographic software development, so of course RWC is highly relevant to our work. This year, at RWC 2023 in Tokyo, we presented a talk on the third day, titled “hacspec: a gateway to high-assurance cryptography”. Franziskus and I described work we are doing in collaboration with our colleagues at Inria, Aarhus, Porto, and Meta, on the hacspec language, the hax tool, and the libcrux crypto library.
The talk slides and video are below, and so is a slightly longer version of this talk I gave at RuhrSec 2023, an IT security conference at Bochum, Germany.
hacspec, hax, and libcrux
hacspec is a side-effect free subset of Rust that is designed to make it easy to write formal specifications for high-assurance cryptographic software, such as crypto algorithms, constructions, and protocols. In hacspec, you can write small, simple, succinct, purely-functional programs in Rust that are easy to reason about, and hence can serve as specifications for your complex, ugly, feature-rich implementation that has been optimized for speed and memory.
The hax tool translates specifications written in hacspec to the formal input languages used by several proof environments, such as F*, Coq and Easycrypt. You can then use these provers to prove properties of your specification or to verify your optimized implementation against your high-level hacspec.
Using hacspec and hax, we built a new cryptographic library called libcrux that brings together, for the first time, formally verified code from multiple libraries into a single Rust library with a unified defensive API. The library contains formally verified C implementations from the HACL* library, verified assembly implementations from Vale and Jasmin, and verified Rust crypto from AUCurves. The resulting library, libcrux, has best-in-class performance on Intel and ARM processors, comparable to unverified libraries like OpenSSL.
All three projects, hacspec, hax, and libcrux, are open source collaborative efforts being actively developed on GitHub. Try them out, give us feedback, and get in touch if you like to understand how they can work better for your use-case:
- hacspec design: paper
- hax repository: code and tools
- libcrux repository: code