Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/hal-03176482
Contributor : Denis Merigoux <>
Submitted on : Monday, March 22, 2021 - 2:01:42 PM
Last modification on : Tuesday, March 23, 2021 - 3:28:09 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03176482, version 1

Collections

Citation

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

Share

Metrics

Record views

439

Files downloads

680