Libjade is a formally verified cryptographic library written in the jasmin programming language with computer-verified proofs in EasyCrypt. Libjade is part of the Formosa-Crypto project.
The primary focus is on offering high-assurance implementations of post-quantum crypto (PQC) primitives to support the migration to the next generation of asymmetric cryptography. The library additionally contains implementations of various symmetric primitives and—to enable hybrid deployment of PQC—also widely used elliptic-curve-based schemes.
This section contains information for anybody who would like to integrate code from Libjade into a higher-level cryptographic library or application. If you would like to compile Libjade yourself, run tests, or reproduce proofs, please see information for developers below.
The jasmin compiler produces assembly, so all code in Libjade is platform specific. In the latest release of Libjade, the only supported architecture is AMD64 (aka x86_64 or x64). All code in the latest release is in AT&T assembly format and is following the System V AMD64 ABI, which is used by, e.g., Linux, FreeBSD, and (Intel-based) macOS.
The latest release of Libjade includes implementations of the following primitives (asymmetric post-quantum primitives in boldface):
- Hash functions: SHA-256, SHA-512, SHA3-224, SHA3-256, SHA3-384, SHA3-512
- Extendable output functions (XOFs): SHAKE-128, SHAKE-256
- One-time authenticators: Poly1305
- Stream ciphers: ChaCha12, ChaCha20, Salsa20, XSalsa20
- Authenticated encryption ("secretbox"): XSalsa20Poly1305
- Scalar multiplication: Curve25519
- Key-encapsulation: Kyber-512, Kyber-768
- Signatures: Falcon512 (verification only)
For users of Libjade we recommend the latest release package as an entry point. Release packages contain already compiled assembly files.
Libjade is currently not set up to be used as a standalone library, but rather
as a collection of implementations of different primitives that can easily be
integrated into higher-level libraries.
Each of the subdirectories under the libjade
directory of the release package
contains implementations for one cryptographic functionality.
For example, under libjade/crypto_hash
you will find implementations of hash
functions in the leaf directories under libjade/crypto_kem
you will find implementations of key encapsulation mechanisms (KEMs).
Each implementation consists of five files:
- a C header (
.h
) file; - an assembly (
.s
) file; - the jasmin (
.jazz
) input file that was used to produce the.s
file; - a file called
example.c
; and - a
Makefile
.
In order to use code from Libjade in a higher-level library or application,
only the .h
and .s
files are needed.
The .jazz
file is included only for users who are interested in the original source.
The file example.c
illustrates how to use the functions defined in the .h
file
and implemented in the .s
file, and the Makefile
illustrates how to compile example.c
.
The API of Libjade is largely following the C API of libsodium1, which, in turn,
is building on the C API of NaCl2.
This means that all cryptographic objects (keys, messages, ciphertexts, signatures) are
passed through the API in "wire format", i.e., as byte arrays.
Unlike libsodium and NaCl, Libjade currently does not offer opinionated API functions;
for example, there is no crypto_kem
functionality with underlying primitives chosen
by the library designers, but only functions like
jade_kem_kyber_kyber768_amd64_ref_keypair
,
jade_kem_kyber_kyber768_amd64_ref_enc
, and
jade_kem_kyber_kyber768_amd64_ref_dec
,
which make the underlying primitive (here: Kyber7683) and concrete
implementation (here: a reference implementation targeting AMD64) explicit.
For more information about the APIs of the different cryptographic functionalities
offered by Libjade, see the full API documentation.
The overarching security goal of Libjade is to provide assembly-code that is connected through computer-verified proofs to a cryptographic security notion and that offers computer-verified protections against a well-defined class of implementation attacks. Part of the guarantees are offered by the jasmin compiler, others through (ongoing) interactive proofs in the EasyCrypt proof assistant.
- The jasmin compiler is proven (in Coq) to preserve semantics of a program through compilation.
- The jasmin compiler is proven (in Coq) to maintain secret-independence of control flow and secret-independence of locations of memory access through compilation4.
- Thread safety is guaranteed by the fact that jasmin does not support global variables (as long as the caller respects the function's contract).
- Functional correctness of implementations with respect to a high-level EasyCrypt specification is guaranteed by interactive proofs in EasyCrypt. This is ongoing work for many implementations in Libjade; for details see see the section on functional-correctness proofs.
- Cryptographic security (e.g., indistinguishability or unforgeability notions) of the high-level EasyCrypt specification is guaranteed by computer-verified proofs in EasyCrypt. This is ongoing work for many primitives in Libjade; for details see see the section on security proofs.
Libjade is actively developed and there are multiple features we are currently working on:
- Support using Libjade in code built to run under Microsoft Windows
- Integrate jasmin's safety checker into continuous integration
- Add reference implementation for Falcon signature verification
- Support additional primitives, most notably Dilithium5 and SPHINCS+6 signatures
- Use the jasmin security type system to guarantee absence of secret-dependent control flow and access to memory at secret-dependent locations on source level.
- Use the jasmin security type system to enforce Spectre v1 protection7 on source level
- Ensure zeroization of jasmin stack memory before returning from Libjade functions
- Cover all implementations by proofs of functional correctness
- Provide cryptographic proofs of security for all primitives included in Libjade
- Support other architectures (next step: ARMv7-M)
Libjade uses the following structure of branches:
- For each release of Libjade we creat one
release
branch, named ``release/YYYY.MM, where YYYY is replaced by the year and MM by the month of the release. Such branches is created frommain
(see below) and this branching is a one-way street. After branching, we ensure that all code in the branch builds with the latest release of the jasmin compiler, that all tests pass, and that all proofs of functional correctness are reproducible with the latest release of EasyCrypt. We then assign a `release-YYYY.MM` tag and create the release package (see above) from that tagged commit. The latest release of Libjade additionally gets a `latest` tag. We do not accept any PRs from feature branches (see below) into release branches, but will apply relevant bugfixes (see below) through PRs. For every bugfix that is merged into a release branch, we add a tag that additionally contains a counter, i.e., release-YYYY.MM-X, for the X'th bugfix PR applied to release/YYYY.MM. For bugfixes applied to the `latest` release, we move the `latest` tag to the version that contains all bugfixes. If you would like to build libjade from the jasmin source for production use, or run tests, we recommend to work with release branches, typically thelatest
release. Note that code in non-release branches is not guaranteed to have the high-assurance guarantees that Libjade aims for. - The
main
branch is used to work towards the next release of Libjade. Pull requests into this branch are checked by CI, but some particularly time-consuming CI tests may run only periodically and not with every merge into this branch. Code inmain
is expected to build with themain
branch of the jasmin compiler and all proofs are expected to be reproducible with themain
branch of EasyCrypt. We accept and solicit pull requests intomain
. - All other branches are feature branches, bugfix branches,
or experimental branches named
feature/XXX
,bugfix/YYY
, orexperimental/ZZZ
, whereXXX
,YYY
, andZZZ
are short descriptions of the goal of the branch. Generally,feature
branches are created with the goal to be eventually merged intomain
;bugfix
branches are created with the goal to be merged intomain
and possibly relevantrelease
branches andexperimental
branches are created to try something out without the expectation that they will ever be merged intomain
. Once afeature
branch or abugfix
branch has been merged or anexperimental
branch is no longer needed, these branches should be deleted.
In order to build Libjade, you will first need to
obtain and build the jasmin compiler.
In the following we will assume that you have built the correct branch of the jasmin compiler
(e.g., the latest release in order to build code in the release
branch of Libjade or the
head of the jasmin main
branch if you are working with the main
branch of Libjade) and
that jasminc
is in your PATH
environment variable.
In order to build all code in Libjade, simply run
cd src/ && make
This will, in each leaf directory under src/crypto_*/
, build one .s
file from the corresponding .jazz
file.
For example, it will build
src/crypto_kem/kyber/kyber768/amd64/ref/kem.s
from
src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz
and it will build
src/crypto_hash/sha3-256/amd64/bmi1/hash.s
from
src/crypto_hash/sha3-256/amd64/bmi1/hash.jazz
.
Also, this will build a file src/libjade.h
and a file src/libjade.a
,
each with all implementations of all primitives offered by Libjade.
To remove all files produced by this global build process, simply run make distclean
in the src/
directory.
Alternatively, if you are interested in building only a specific implemenation of a specific primitive
contained in Libjade, you can simply run make
in the corresponding leaf directory under src/crypto_*
.
For example, to build just the Kyber768 reference implementation targeting the AMD64 architecture, run
cd src/crypto_kem/kyber/kyber768/amd64/ref/ && make
This will only build
src/crypto_kem/kyber/kyber768/amd64/ref/kem.s
from
src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz
.
The current prerequisites for running tests in Libjade are:
- Jasmin compiler (
jasminc
) in yourPATH
; - C compiler (gcc or clang);
- GNU make;
- Valgrind;
- Bash.
Note 1: our tests are run under Linux-based OS (Debian). We are currently updating them to be macOS-compatible.
Note 2: some Libjade AMD64 implementations require specific CPU extensions, such as BMI1 or AVX2. Whenever such extensions are not available, some tests will fail. As such, and to run all tests successfully, there is the requirement that the CPU must support all extensions used throughout Libjade. Any modern Intel CPU supports those. Some AMD CPUs do not. We plan to integrate run-time detection of CPU extensions in our building system to improve on this. We also plan to make available a list of required CPU extensions for each implementation. This will likely happen when implementations for architectures different than AMD64 are developed/integrated into Libjade.
Running cd test/ && make
performs the following tests, in no particular order, for all
implementations:
checksums
: implements tests that we adopted from SUPERCOP8. These tests, briefly:
- check for out-of-bounds memory writes;
- how the implementation behaves when pointers overlap (e.g., input pointer is equal to output pointer);
- functionality (e.g., decryption after encryption recovers the original plaintext);
- check if the function produces the same outputs given the same inputs; and
~
correctness: computes a checksum of the functions' outputs to be compared with the expected checksum. In these tests, pseudo-random inputs are given to the functions as arguments, andrandombytes
is replaced by a deterministic function. We also consider two checksum values:checksumsmall
andchecksumbig
. The difference is the number of test iterations (checksumbig
has more test iterations and, consequently, takes more CPU time). The original idea is to avoid runningchecksumbig
ifchecksumsmall
fails. On our deployment, there is no dependency betweenchecksumsmall
andchecksumbig
, and both are evaluated (formake all
kind of targets) given that it simplifies day-to-day development tasks and the Makefile design (developer does not need to wait forchecksumsmall
to finish if it only intends to runchecksumbig
. The expected checksum values are on META.yml files under the source (src/) directory. We use values that can be found (or computed, if not available) with the SUPERCOP framework;
-
memory
: the executables produced in the context of these tests are mainly valuable to run with Valgrind, primarily to detect out-of-bounds reads on the argument pointers (and even some out-of-bound writes thatchecksums
is not able to identify given that, for practical reasons, the size of canaries must be kept reasonably small -- in this context, a canary is a small pattern copied before and after a memory region to detect out-of-bound memory writes). For operations which process data of arbitrary length, for instance, a stream cipher whose plaintext length is only known during runtime, we test for lengths from 0 to 4096 (this value is easily adjusted). -
functest
: defines a simple sequence of calls to the functions of a given cryptographic operation to demonstrate how these can be used. Code from these test files is included in the release asexample.c
. For instance, in the case of Kyber, a primitive of the operationcrypto_kem
, first callskeypair
, to create a public and a secret key and thenenc
(apsulate) anddec
(apsulate) to show how to obtain/recover a shared secret; -
printparams
: tests if the expected macros for a given API are well defined in their correspondingapi.h
file.
The source code for each test can be found under libjade/test/crypto_*/
. For example, under
libjade/test/crypto_kem/
, the following files are present: checksums.c
, functest.c
, memory.c
,
and printparams.c
. A deterministic version or randombytes
(necessary for nondeterministic
functions to compute the same checksum on every execution) can be found under libjade/test/common
.
Under this same directory, there are also some files with utility code to, for example, handle
printing and opening files.
As explained above, running cd test/ && make
runs all tests. More precisely, the default
target is equivalent to running the following 4 commands:
make CI=1 -C ../src/ all
make CI=1 all
make CI=1 reporter
make CI=1 err
CI
is a variable that stands for Continuous Integration. When CI
is set to 1, all the
compilation and execution outputs and return errors are recorded for later inspection. Some log
files are under .ci/
(hidden) directories. Additionally, if the compilation or execution of a
given target returns an error (a segmentation fault, for instance), make
continues to execute
until there are no more tasks. On a system with 8 cores available, running make -j8
will use
those cores as well as make -j$(nproc)
. Running make
should take 10 to 13 minutes on a
reasonably recent CPU when using all the available CPU power.
-
make CI=1 -C ../src/ all
builds all assembly files undersrc/
; -
make CI=1 all
follows each*.jazz
file undersrc/
and compiles and runs the tests (for instance,checksumbig
,checksumsmall
, ormemory
) using the same directory structure that exists insrc/
, but undertest/bin
. After runningmake CI=1 all
the binaries and outputs corresponding to, for instance,src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz
will be built undertest/bin/crypto_kem/kyber/kyber768/amd64/ref/
and, under normal conditions,cat test/bin/crypto_kem/kyber/kyber768/amd64/ref/checksumbig.out && echo
should show thechecksumbig
value that is present insrc/crypto_kem/kyber/kyber768/META.yml
; -
make CI=1 reporter
prints information about the tests: compilation and execution. To check if the checksums match with the ones specified inMETA.yml
files, the scriptscripts/checksumsok
is used; -
make CI=1 err
returns an error if there are any*.error
files undertest/bin
. These files contain the output from thestderr
and the return code of the job that failed.
Even though running all the tests might be helpful occasionally, as a developer you will often want to
focus on a specific family of implementations (or just one). For instance, consider the scenario
where the developer wants to produce the checksumsmall
corresponding to the reference AMD64
implementation of Kyber768 (to verify that it passes through all the tests and actually outputs a
checksum):
$ make bin/crypto_kem/kyber/kyber768/amd64/ref/checksumsmall.stdout
456bb24a767160dcca466adde267b87f359de6e827d31b5b23512d227d8bbfaa
While typing the target, the developer can use 'TAB' for completion, given that all targets are declared (not extensively, but instead by using variables to keep the Makefile short and easy to maintain). As another example, to run Valgrind for a specific implementation:
$ make bin/crypto_kem/kyber/kyber768/amd64/ref/memory.stdout
(...)
==XXXXX== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
Another helpful feature is to use the FILTER
variable. For instance, to run all tests (the same 4
rules previously discussed) just for all Kyber768 implementations, run the following:
$ make FILTER=../src/crypto_kem/kyber/kyber768/%
(...)
Checksums status:
OK, 0, crypto_kem/kyber/kyber768/amd64/avx2/.ci/checksumbig.ok.log
OK, 0, crypto_kem/kyber/kyber768/amd64/avx2/.ci/checksumsmall.ok.log
OK, 0, crypto_kem/kyber/kyber768/amd64/ref/.ci/checksumbig.ok.log
OK, 0, crypto_kem/kyber/kyber768/amd64/ref/.ci/checksumsmall.ok.log
Regarding the previous example, the default value for FILTER
is ../src/crypto_%
. The %
is
important and should not be missed: FILTER
is given to the text function filter
(see Text
Functions section in GNU Makefile documentation for more information), and %
corresponds to the
pattern.
To clean artifacts produced under test/
:
$ make clean
And to remove also assembly files under src/
:
$ make distclean
Footnotes
-
Gilles Barthe, Benjamin Gregoire, Vincent Laporte, and Swarn Priya. Structured Leakage and Applications to Cryptographic Constant-Time and Cost. ACM CCS 2020. IACR ePrint 2021/650 ↩
-
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean. Typing High-Speed Cryptography against Spectre v1. IEEE S&P 2023. IACR ePrint 2022/1270. ↩