Paper 2025/142
hax: Verifying Security-Critical Rust Software using Multiple Provers
Abstract
We present hax, a verification toolchain for Rust targeted at security-critical software such as cryptographic libraries, protocol imple- mentations, authentication and authorization mechanisms, and parsing and sanitization code. The key idea behind hax is the pragmatic observation that different verification tools are better at handling different kinds of verification goals. Consequently, hax supports multiple proof backends, including domain-specific security analysis tools like ProVerif and SSProve, as well as general proof assistants like Coq and F*. In this paper, we present the hax toolchain and show how we use it to translate Rust code to the input languages of different provers. We describe how we systematically test our translated models and our models of the Rust system libraries to gain confidence in their correctness. Finally, we briefly overview various ongoing verification projects that rely on hax.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Published elsewhere. 16th International Conference on Verified Software: Theories, Tools, and Experiments
- Keywords
- Formal VerificationProtocol AnalysisCryptographic Libraries
- Contact author(s)
- karthik @ cryspen com
- History
- 2025-01-31: approved
- 2025-01-29: received
- See all versions
- Short URL
- https://ia.cr/2025/142
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2025/142,
author = {Karthikeyan Bhargavan and Maxime Buyse and Lucas Franceschino and Lasse Letager Hansen and Franziskus Kiefer and Jonas Schneider-Bensch and Bas Spitters},
title = {hax: Verifying Security-Critical Rust Software using Multiple Provers},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/142},
year = {2025},
url = {https://eprint.iacr.org/2025/142}
}
