SCloud+ KEM in Jasmin

Jasmin implementations of the SCloud+ KEM (current specification, five security levels, AES and SHAKE families; and version 1.1, three levels), with an EasyCrypt specification of the scheme and machine-checked proofs about it. See the project reports D2.1 and D2.2 for the description of the work.

spec/                        EasyCrypt specification and proofs
src/scloudplus_jasmin_opt/   optimised SCloud+ (AVX2), 10 units
src/scloudplus_jasmin_ref/   reference message codec, 5 units
src/scloud11_jasmin_opt/     optimised SCloud+ v1.1 (AVX2), 3 units
src/scloud11_cref/           v1.1 C baseline (shared libraries)
src/bench/                   benchmark harnesses
include/                     C headers of the exported ABI (generated)
env/                         Dockerfile of the toolchain

Running the checks

git clone --recurse-submodules https://github.com/haslab/JasminCode.git
cd JasminCode
make -C env build         # toolchain image (Jasmin, EasyCrypt, provers, gcc, OpenSSL, valgrind)
make -C env shell         # shell in the image with the repository mounted at /work

Inside the container:

ec-verify                 # toolchain sanity check
scripts/run-tests.sh      # build the 13 units and run all functional tests and KATs
make -j check-sct         # jasmin-ct --sct: speculative constant-time (implies CT) of the KEM exports
make -j check-ct          # jasmin-ct: sequential constant-time, prints the inferred contracts
make extract              # jasmin2ec on the reference codec, type-checked
make check-ec             # EasyCrypt: specification and proofs (runs extract first)
make check-headers        # include/*.h match the Jasmin export signatures
make memcheck             # valgrind memcheck over the functional tests
make bench                # build the benchmark harnesses and time the KEM operations
scripts/run-bench.sh      # full benchmark run, results and provenance in src/bench/results/

Knobs: USE_VAES=false scripts/run-tests.sh for CPUs without VAES; make bench BENCH_GROUPS="kem pke sample" or BENCH_GROUPS=all; MEMCHECK_KATS=1 make memcheck; tool paths in Makefile.conf.

Licence

Apache License 2.0 (LICENSE), except for the following third-party material: the Keccak/SHA-3 library submodules/formosa-keccak (CC0-1.0 or Apache-2.0); the SCloud+ C implementations submodules/scloudplus and submodules/scloudplus-1.1 (MIT); and the files copied from the Jasmin compiler distribution (MIT): src/common/jasmin_syscall.{c,h} and spec/eclib/.