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 language

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

hacspec architecture

The hacspec architecture is depicted in the following graph.

Writing hacspec

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.

speclib

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.¹

spec-checker

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.²

hacspec-check <your-hacspec>

Executing hacspec

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.³ Check out the repository to use them. All tools can be easily called via make (see documentation in the repo /compiler/ for details).

Type checker

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>.

Compiler

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.

F* compiler

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.

Example

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)

@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

The test poly_test.py:

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 checker.native poly.py. 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

Next steps

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.