HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust

Abstract : Despite significant progress in the formal verification of security-critical components like cryptographic libraries and protocols, the secure integration of these components into larger unverified applications remains an open challenge. The first problem is that any memory safety bug or side-channel leak in the unverified code can nullify the security guarantees of the verified code. A second issue is that application developers may misunderstand the specification and assumptions of the verified code and so use it incorrectly. In this paper, we propose a novel verification framework that seeks to close these gaps for applications written in Rust. At the heart of this framework is hacspec, a new language for writing succinct, executable, formal specifications for cryptographic components. Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts. An application developer can use hacspec to specify and prototype cryptographic components in Rust, and then replace this specification with a verified implementation before deployment. We present the hacspec language, its formal semantics and type system, and describe a translation from hacspec to F. We evaluate the language and its toolchain on a library of popular cryptographic algorithms. An earlier attempt in this direction by some of the same authors, was also called hacspec, and sought to embed a cryptographic specification language into Python. We now believe that the strong typing of Rust provides an essential improvement to the specification and programming workflow. This work subsumes and obsoletes that earlier attempt. Hereafter, we use hacspec-python to refer to this prior version.
Complete list of metadata

Contributor : Denis Merigoux Connect in order to contact the contributor
Submitted on : Monday, March 22, 2021 - 2:01:42 PM
Last modification on : Thursday, February 3, 2022 - 11:13:48 AM
Long-term archiving on: : Wednesday, June 23, 2021 - 6:46:18 PM


Files produced by the author(s)


  • HAL Id : hal-03176482, version 1



Denis Merigoux, Franziskus Kiefer, Karthikeyan Bhargavan. Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust. [Technical Report] Inria. 2021. ⟨hal-03176482⟩



Record views


Files downloads