The hacspec language is a DSL for cryptographic algorithms.
But it can also be seen as a typed subset of Python.
The following describes the language.
Values v ::=
n integer constants
| True | False boolean constants
| '...' | "..." string constants
| (v1,...,vn) tuple constant
| array([v1,...,vn]) array constant
Expressions e ::=
| x | m.x local and global variables
| (e1,...,en) tuple construction
| array([e1,...,en]) array construction
| array.length(e) array length
| e[e0] array access
| e[e0:e1] array slice
| e(e1,...,en) function call
| e1 binop e2 builtin binary operators
| unaryop e builtin unary operators
Types t ::=
int, str, bool basic types
| tuple_t(t1,...,tn) tuples
| vlarray_t(t) variable-length array
| x user-defined or builtin type
| x(t1,...,tn,e1,...,em) builtin type application
Statements s ::=
x: Type = t type declaration
| x: t variable declaration
| x = e variable assignment
| x binop= e augmented variable assignment
| (x1,..,xn) = e tuple matching
| x[i] = e array update
| x[i] binop= e augmented array update
| x[i:j] = e array slice update
| if e: if-elif-else conditional
| for i in range(e): for loop
| break break from loop
| def x(x1:t1,...,xn:tn) -> t: function declaration
s1 ... sn
| return e return from function
| from x import x1, x2,..., xn module import
Specs σ ::= s1...sn sequence of statements
The hacspec architecture is depicted in the following graph.
Every spec should be accompanied by a test and some test vectors leaving the author with at least two files, e.g. poly.py and poly_test.py (also see Example section).
Note that only the spec file has to be hacspec syntax.
The test file can make use of all of Python.
hacspec comes with a standard library called speclib and a spec-checker.
To use the hacspec speclib and spec-checker install them via pip install hacspec or from the source (the setup.py for the Python package can be found in /build/).
Running hacspec requires a Python interpreter version 3.6.4 or newer.
Commonly used functionality is provided in speclib (from hacspec.speclib import *).
The full speclib documentation can be found here.
Some highlights are
modular arithmetic: natmod_t is an integer data type that provides modular arithmetic, e.g. felem_t = natmod_t((2**130)-5) defines field elements modulo (2**130)-5.
machine integers: unitN_t define commonly used machine integer types for N = 8, 16, 32, 64, 128.
byte arrays, vectors, and matrices: provided data structures are array_t, bytes_t, vector_t, matrix_t as well as the variable length versions vlarray_t and vlbytes_t. Note that the vector and matrix data types offer point-wise arithmetic.
refinements: refine_t allows to refine data types.
contracts: @contract annotation on functions can be used for pre- and post-conditions.1
Since hacspecs are executed with a Python interpreter it is not sufficient to run hacspec to check their syntax.
To check that the syntax is valid a spec-checker is provided.2
hacspec tests are executed with the Python interpreter.
Executing tests on a spec can yield three different results.
The execution is successful and all test vectors pass. In this case the spec is most likely correct and doesn’t contain any obvious typing issues.
The execution fails because of a failing test case. In this case the spec is probably wrong (or the test vectors are incorrect).
The execution fails because of a type error. The speclib as well as typeguard are used to perform runtime type checks.
Checking and compiling hacspec
To use hacspecs for formal verification such as verification of cryptographic properties of an algorithm, generating code in other languages from the spec, or verifying correctness of other implementations with it, a second set of tools is provided.
These tools are written in OCaml and thus require additional setup and are not packaged right now.3
Check out the repository to use them.
All tools can be easily called via make (see documentation in the repo /compiler/ for details).
To perform proper type checking Python is impractical.
A native type checker is implemented in OCaml that performs syntax and type checking for hacspec.
To run the type checker on a spec simply run ./checker.native <your-spec>.
The type checker also produces a typed AST that can be used to generate the spec in another formal language.
There are currently compiler for EasyCrypt and F*.
I’ll only describe the F* compiler as it’s more complete.
The F* compiler requires HACL_HOME and FSTAR_HOME environment variables to be set.
The compiler is then invoked like this ./to_fstar <your-spec>.
The generated F* spec can then be type checked or executed on test vectors to check correctness of the spec.
Using kremlin the F* code can also be used to generate C code.
The hacspec repo has many examples.
I’ll only give a short one here.
The spec poly.py:
from hacspec.speclib import*
p130m5: nat_t = (2**130) -5
felem_t = natmod_t(p130m5)
@typecheckeddeffelem(n: nat_t) -> felem_t:
@typecheckeddefpoly(m: vlarray_t(felem_t), r: felem_t) -> felem_t:
acc: felem_t = felem(0)
for i in range(array.length(m)):
acc = (acc + m[i]) * r
The test poly_test.py:
from poly import*defmain():
m = array([felem(0x6f4620636968706172676f7470797243),
k = felem(0xa806d542fe52447f336d555778bed685)
expected = natmod(0xa01b776a69ea8c1cd3ba00179dc218ab, p130m5)
p = poly(m,k)
ifnot expected == p:
print("Expected: "+ str(expected))
print("Got: "+ str(p))
if __name__ =="__main__":
This can now be run with python poly_test.py and checked with hacspec-check poly.py and checker.native poly.py.
Compiling this to F* can be done with to_fstar.native poly.py, generating the following F* code.
modulePolyopenSpecliblet p130m5 : nat_t =(2 **. 130)-. 5
let felem_t :Type0= natmod_t p130m5
let felem (n : nat_t): felem_t = natmod n p130m5
let poly (m : vlarray_t felem_t)(r : felem_t): felem_t =let acc = felem 0 inlet acc = repeati (array_length m)(fun i acc ->(acc +. m.[i])*. r) acc in
We hope that hacspec is a useful tool for spec authors and many people indeed voiced interest already.
While the tooling isn’t perfect yet, the language is developed enough to start using it.
The next steps for hacspec is to get some usage from spec authors and improve tooling.
We also hope to get more compilers for different formal languages implemented.
Note that contracts are still in development and not fully supported yet.
In future hacspec syntax checks and running test vectors on the spec should be done in one invocation.
In future pre-built binaries should be distributed to make this easier.
hacspec is mostly a spare time project for me at the moment. Development is therefore not always as fast as I’d like.