HacSpec is a proposal for a new specification language for cryptographic primitives that is succinct, that is easy to read and implement, and that lends itself to formal verification. It aims to formalise the pseudocode used in cryptographic standards by proposing a formal syntax that can be checked for simple errors. HacSpec specifications are further executable to test against test vectors specified in a common syntax.
The main focus of HacSpec is to allow specifications to be compiled to formal languages such as cryptol, coq, F*, and easycrypt and thus make it easier to formally verify implementations. This allows a specification using HacSpec to be the basis not only for implementations but also for formal proofs of functional correctness, cryptographic security, and side-channel resistance.
The idea of having a language like HacSpec stems from discussions at the recent HACS workshop in Zurich. The High-Assurance-Cryptographic-Software workshop (HACS) is an invite-only workshop co-located with the Real World Crypto symposium.
Anyone interested in moving this project forward should subscribe to the mailing list or file issues and pull requests against the Github repository.
How far are we?
We discussed and hacked at HACS a month ago and improved a little over the last weeks. The current state can be found at Github repository.
The language
There are examples written in what we believe could be the HacSpec. The language is valid Python 3.6 using PEP484 and PEP526 for typing. It further uses comments (similar to PEP484 types) to define lengths and ranges.
There are also experiments using Rust as basis for HacSpec. While Rust’s type system makes it a compelling candidate, limitations in handling integers of arbitrary size means we probably won’t be basing HacSpec on Rust.
The language specification is currently vague and not fully formalised yet. It lives in a markdown document but will move to an RFC layout later.
Formal specifications
To show how cryptographic primitives are modelled in formal languages we added a number of specifications in different languages such as cryptol, coq, F*, and easycrypt to the repository.
Spec checker
In order to verify whether a specification is a valid HacSpec Aaron started to implement a spec-checker. Basing HacSpec on another language like Python means that not all valid Python programs are valid HacSpec programs. The spec checker is supposed to tell authors whether a given python program is a valid HacSpec.
Compilers
There’s currently a very basic HacSpec to F* compiler from Karthik. Eventually we would like to have compilers from HacSpec to all common formal languages such as cryptol, coq, F*, and easycrypt.
Call for participation
We invite contributions in the following areas.
- We invite people to submit “standalone" formal specs for inclusion in the formal-models directory.
- We invite formal methods people to build compilers from HacSpec to their favourite modelling language.
- We invite spec authors and developers to comment on HacSpec and provide examples of what they consider good crypto specs or beautiful “obviously correct” crypto implementations.
- We invite developers to build compilers from HacSpec to their favourite programming language.
What HacSpec is not about
HacSpec does not aim to be general enough to express protocols at this point. While this might be a target in the future the first iteration of HacSpec is only targeting crypto primitives.