hacspec

A specification language for crypto primitives in Rust.

This is the successor of https://github.com/HACS-workshop/hacspec.

For a quick intro, you can look at the presentation slides. More information is available in the book. Also, see the Publications below.

Crates

Name	Crates.io	Docs	CI
hacspec
hacspec-lib

Usage

Writing hacspec

hacspec is always valid Rust code such that starting to write hacspec is as simple as writing Rust code that is compliant with the language specification. However, this is very tedious. It is recommended to use the hacspec standard library to write hacspec. In order to ensure that the code is a hacspec one can use the typecheker.

Typechecking

Make sure you have at least rustup 1.23.0. The rust-toolchain automatically picks the correct Rust nightly version and components. The compiler version is currently pinned to nightly-2023-01-15.

Installing the typechecker from the repository

cargo install --path language

Installing the typechecker from crates.io (not always up to date)

cargo install hacspec --version 0.2.0-beta.4

Manually installing dependencies

First ensure that Rust nightly is installed and the typechecker is installed.

cd language
rustup toolchain install nightly-2023-01-15
rustup component add --toolchain nightly-2023-01-15 rustc-dev
cargo +nightly-2023-01-15 install hacspec

Depending on your system you might also need llvm-tools-preview

rustup component add --toolchain nightly-2023-01-15 llvm-tools-preview

Usage

In a hacspec crate or workspace directory typechecking can be done as follows now: (Specifying +nightly-2023-01-15 is only necessary if it’s not specified in the toolchain as it is in this main repository.)

cargo +nightly-2023-01-15 hacspec <crate-name>

Note that the crate dependencies need to be compiled before it can be typechecked.

cargo +nightly-2023-01-15 build

If typechecking succeeds, it should show

> Successfully typechecked.

Generating code

To generate F*, EasyCrypt, or Coq code from hacspec the typechecker (see above) is required.

cargo +nightly-2021-11-14 hacspec -o <fst-name>.fst <crate-name>
cargo +nightly-2021-11-14 hacspec -o <ec-name>.ec <crate-name>
cargo +nightly-2021-11-14 hacspec -o <coq-name>.v <crate-name>

Publications & Other material

• 📕 Tech report
• 📕 HACSpec: A gateway to high-assurance cryptography
• 📕 Original hacspec paper

Secondary literature, using hacspec:

• 📕 Last yard

Repository Structure

This is a cargo workspace consisting of three main crates:

• hacspec: the compiler, typechecker and language infrastructure for the hacspec subset of Rust
  • Note that the language infrastructure is excluded from the main workspace of crates, so it won’t be build when you launch cargo build from the root of the repository.
• hacspec-lib: the standard library of hacspec programs
• hacspec-provider: a cryptography provider with a set of cryptographic primitives written in hacspec
  • This combines the individual crates from the examples directory and implements the RustCrypto API on top to use them from regular Rust code.

The three main crates make use of a set of additional crates:

• abstract-integers: wrapper around BigInt for modular natural integers
• secret-integers: wrapper around integer types for constant-timedness
• unsafe-hacspec-examples: cryptographic specs written in hacspec but not formally typechecked yet(hence the unsafety) as hacspec is a work in progress
• examples: cryptographic primitives that have passed the hacspec typechecking
• hacspec-attributes: helper for the hacspec library
• hacspec-dev: utilities that are not part of the language

Compiled code:

• fstar: contains F* translations of the cryptographic specs, produced by the hacspec compiler
• easycrypt: contains EasyCrypt translations of the cryptographic specs, produced by the hacspec compiler

Contributing

Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.

The main entry points for contributions and some general work items are

• the language if you want to work on the hacspec language itself
  • improve the typechecker
  • improve the existing compiler backends (F* and EasyCrypt)
  • add a new compiler backend
• hacspec implementations
  • implementing new cryptographic primitives in hacspec
  • improve the provider
• the standard library
  • enhance numeric implementations
  • enhance vector arithmetic

Examples

There’s a set of example specs, divided between the safe and unsafe. To run all examples one can use cargo test.

Examples

• Chacha20
• Poly1305
• Chacha20Poly1305
• AES 128
• GF 128
• AES-GCM 128
• SHA256
• SHA512
• Curve25519
• NTRU-prime
• SHA-3
• HKDF-SHA256
• HMAC-SHA256
• BLS12-381
• BLS12-381 Hash To Curve
• RIOT bootloade
• GIMLI
• P256
• ECDSA-P256-SHA256
• Ed25519
• RSA-FDH-VRF
• ECVRF
• BIP-340 text blog, including secp.
• merlin
• ristretto

Unsafe examples

• AES 128/256
• AES-GCM 128/256
• Blake2b