Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification

This artifact consists of the two tools "scVerif" and "maskVerif", as well as masked implementations.

1. Prerequisites

Install the ocaml package manager "opam" according to
https://opam.ocaml.org/doc/Install.html

Make sure opam --version reports a version greater 2.0.0.
You might need to run opam init, opam update, or eval $(opam env).

This artifact has been tested with the ocaml compiler version "4.10.0".
Your version can be checked using:

opam switch

If necessary, the correct version can be created using:

opam switch create -v scverif ocaml-base-compiler.4.10.0

You might need to run eval $(opam env) again.

2. Build maskVerif

Detailed instructions are contained in "maskverif/README".
On some systems, such as macOS, it might be necessary to adopt the build system by removing -lrt from the flags and c_library_flags fields in the file "maskverif/src/dune".
In short:

sudo apt-get install libgmp-dev m4
opam pin add maskverif

maskVerif is now installed and available in your terminal after running eval $(opam env).

2. Build scVerif

Detailed instructions are contained in "scverif/README.md".
In short:

opam pin add scverif

scVerif is now installed and available in your terminal after running eval $(opam env).

3. Execute the examples

cd gadgets
ln -s ../scverif/models models
make

Run a specific example using e.g.

scverif --il present/second_order/asmpresent_order2.il

Documentation for scVerif is located at "scverif/documentation.md".

A tutorial for maskVerif is located at "maskverif/tutorial.mv" and can be run with

cat maskverif/tutorial.mv | maskverif