Verified Garbage

Verified Garbage is an experimental cryptography library, implemented entirely by LLMs. All of the cryptography primitives are formally verified using Lean.

Its aims are, in order:

1. Security
2. Correctness
3. Performance

The library is implemented in Lean, assembly, and Rust.

It targets: x86 (i686 with SSE2), x86-64, ARMv7, ARM64, and PPC64le.

Algorithms

Hashes

Algorithm	Spec landed	x86-64	ARM64	ARMv7	x86
MD5	✅	✅	✅	✅	❌
SHA-1	✅	✅	✅	✅	❌
SHA-256	✅	✅ SHA extensions	✅	✅	✅
SHA3-224, SHA3-256, SHA3-384, SHA3-512, SHAKE128, SHAKE256	✅	✅	✅	✅	✅
SHA-384, SHA-512, SHA-512/224, SHA-512/256	✅	✅	✅	✅	✅

MACs

Algorithm	Spec landed	x86-64	ARM64	ARMv7	x86
HMAC-MD5	✅	✅	✅	✅	❌
HMAC-SHA-1	✅	✅	✅	✅	❌
HMAC-SHA-256	✅	✅ SHA extensions	✅	✅	✅
HMAC-SHA-384	✅	✅	✅	✅	❌
HMAC-SHA-512/224	✅	✅	✅	✅	❌
HMAC-SHA-512/256	✅	✅	✅	✅	❌
HMAC-SHA-512	✅	✅	✅	✅	❌
Poly1305	✅	✅	✅	✅	✅

Ciphers

Algorithm	Spec landed	x86-64	ARM64	ARMv7	x86
ChaCha20	✅	✅ AVX2	✅	✅	✅

AEADs

Algorithm	Spec landed	x86-64	ARM64	ARMv7	x86
AES-GCM (128-, 192- and 256-bit keys)	✅	✅ AES-NI, PCLMULQDQ; GHASH with mul	✅	❌	❌
ChaCha20-Poly1305	✅	✅	✅	✅	✅

KDFs

Algorithm	Spec landed	x86-64	ARM64	ARMv7	x86
PBKDF2-HMAC-MD5	✅	✅	✅	✅	❌
PBKDF2-HMAC-SHA-1	✅	✅	✅	✅	❌
PBKDF2-HMAC-SHA-256	✅	✅ SHA extensions	✅	✅	❌
PBKDF2-HMAC-SHA-384	✅	✅	✅	✅	❌
PBKDF2-HMAC-SHA-512/224	✅	✅	✅	✅	❌
PBKDF2-HMAC-SHA-512/256	✅	✅	✅	✅	❌
PBKDF2-HMAC-SHA-512	✅	✅	✅	✅	❌
scrypt	✅	✅	✅	✅	❌

KEMs

Algorithm	Spec landed	x86-64	ARM64	ARMv7	x86
ML-KEM-768	✅	❌	❌	❌	❌

The tables are generated from the code by ci/algorithms_table.py.

• Spec landed: the algorithm's specification, transcribed from its standard, is in lean/VerifiedGarbage/Spec/.
• x86-64, ARM64, ARMv7, x86: ✅ when verified assembly and a public Rust API exist on that architecture (PPC64le is not started yet), followed by how it has been optimized, if it has (e.g. with SHA-NI or NEON). Where an optimization needs CPU features beyond the architecture's baseline, the features are detected at run time, and CPUs without them run the straightforward scalar code that every other implementation is.

Our goal is to implement all the cryptographic algorithms that are used by the Python pyca/cryptography library.

How it works

• Each primitive is written in assembly, as a program over a Lean model of the target ISA, and proven in Lean to be correct against a specification, memory safe, and constant time (scrypt's ROMix is the exception its standard makes: it reads memory at indices derived from the password, and its contract declares that it leaks them and nothing else secret). See lean/README.md for the layout, the pipeline, and exactly what has to be trusted.
• The proven assembly is emitted into src/asm/ (one directory per architecture) as Rust naked functions (naked_asm!); there is no build script and no separate assembler step.
• The public APIs are Rust that composes these verified primitives.
• The public APIs are tested against the Wycheproof test vectors (tests/wycheproof/).

Development

git clone https://github.com/C2SP/wycheproof
WYCHEPROOF_ROOT=$PWD/wycheproof cargo test   # without it, the Wycheproof tests are skipped

cd lean
lake exe cache get                   # prebuilt Mathlib
lake build                           # check all proofs
lake env lean --run Emit.lean        # regenerate src/asm/ after changing lean/VerifiedGarbage/Artifacts/

To benchmark against OpenSSL (through rust-openssl; needs its headers), and to compare a branch with a checkout of main, as CI does for every pull request that changes the library:

(cd bench && cargo bench)
python3 ci/bench_compare.py path/to/main-checkout .

CI checks every proof, that src/asm/ is exactly what Lean generates, and the import discipline of the Lean directories (ci/check_lean_imports.py); it builds and runs the Rust tests natively on each target architecture, and requires 100% line coverage of the Rust code, merged across all of them.

Credits

This project is inspired by:

• Graviola
• s2n-bignum
• Bobby Powers
• HACS Workshop