Earlier this year I introduced hacspec, a new specification language for cryptographic primitives. After Karthik presented the idea and very preliminary results at IETF 101 in March we made quite some progress and presented a paper with a little more detail at SSR earlier this week. In this blog post I’ll give the gist of the SSR paper and introduce the first version of hacspec.
All information about hacspec can be found at https://hacs-workshop.github.io/hacspec/.
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 ::= v values | 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 s1...sn elif e: s1'...sn' else s1''...sn'' | for i in range(e): for loop s1...sn | 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_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
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_tis an integer data type that provides modular arithmetic, e.g.
felem_t = natmod_t((2**130)-5)defines field elements modulo
- machine integers:
unitN_tdefine 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_tas well as the variable length versions
vlbytes_t. Note that the vector and matrix data types offer point-wise arithmetic.
refine_tallows to refine data types.
@contractannotation 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
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
FSTAR_HOME environment variables to be set.
The compiler is then invoked like this
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.
from hacspec.speclib import * p130m5: nat_t = (2 ** 130) - 5 felem_t = natmod_t(p130m5) @typechecked def felem(n: nat_t) -> felem_t: return natmod(n,p130m5) @typechecked def poly(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 return acc
from poly import * def main(): m = array([felem(0x6f4620636968706172676f7470797243), felem(0x6f7247206863726165736552206d7572)]) k = felem(0xa806d542fe52447f336d555778bed685) expected = natmod(0xa01b776a69ea8c1cd3ba00179dc218ab, p130m5) p = poly(m,k) if not expected == p: print("Error") print("Expected: " + str(expected)) print("Got: " + str(p)) else: print("Test successful") if __name__ == "__main__": main()
This can now be run with
python poly_test.py and checked with
hacspec-check poly.py and
Compiling this to F* can be done with
to_fstar.native poly.py, generating the following F* code.
module Poly open Speclib let 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 in let acc = repeati (array_length m) (fun i acc -> (acc +. m.[i]) *. r) acc in acc
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.