libjade

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.

Overview of cryptographic primitives in Libjade

At the moment, libjade only targets the AMD64 (aka x86_64 or x64) architecture. Supporting multiple architectures is on our TODO list. The following primitives are currently supported by Libjade

Symmetric primitives

Cryptographic hash functions (crypto_hash)

• SHA-256
• SHA-512
• SHA3-224
• SHA3-256
• SHA3-384
• SHA3-512

Extendable output functions (XOFs, crypto_xof)

• SHAKE-128
• SHAKE-256

One-time authenticators (crypto_onetimeauth)

• Poly1305

Stream ciphers (crypto_stream)

• ChaCha12
• ChaCha20
• Salsa20
• XSalsa20

Authenticated encryption (crypto_secretbox)

• XSalsa20Poly1305

Asymmetric primitives

Scalar multiplication (crypto_scalarmult)

• Curve25519

Key-encapsulation mechanisms (KEMs, crypto_kem)

• Kyber-512
• Kyber-768

Signatures (crypto_sign)

• Dilithium3

Build instructions

Installing nix

Installation of libjade requires the jasmin compiler; the recommended way to install the jasmin compiler is via nix. If you do not have nix installed on your system, please run

sh <(curl -L https://nixos.org/nix/install) --daemon

Please also see the nix installation guide

Obtaining and building the jasmin compiler

With nix installed, you are ready to obtain and build the jasmin compiler:

git clone https://gitlab.com/jasmin-lang/jasmin-compiler.git
cd jasmin-compiler/compiler
git fetch -a
git checkout main
nix-channel --update
nix-shell 

Then, inside nix-shell, run

make
exit

Now you should have a working compiler binary called jasminc in jasmin-compiler/compiler/. We recommend adding this directory to your $PATH variable; the instructions in the following assume that jasminc is available in a directory that is in $PATH.

API documentation

Future plans

• Add more primitives; currently work in progress are
  • Dilithium,
  • Sike, and
  • SPHINCS+.
• Complete missing EasyCrypt proofs.
• Support for Windows
• Support multiple architectures, most importantly 32-bit and 64-bit Arm and RISCV CPUs.
• Add interfaces to other languages (e.g., Rust and Go).
• Implement a libjade-agent that wraps libjade crypto functionality in a separate process.