Collection of classical cryptographic primitives written in portable C90 (with optional GNU extensions also supported by Clang) with no dependencies (including the standard library), optimized for correctness, soundness, portability, and speed in that order.
  • C 94.2%
  • Python 4.8%
  • Nix 0.5%
  • Just 0.5%
Find a file
2026-08-13 21:38:46 -05:00
benchmarks Finished migrating to Unity test framework 2026-08-05 22:34:55 -05:00
machines Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
proofs Reconciled Zig CC and CBMC 2026-08-11 20:45:55 -05:00
tests Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
tinycrypt Made CBMC contracts less hard to look at 2026-08-12 09:02:13 -05:00
.clang-format Added formatting rules for contracts 2026-08-12 09:02:48 -05:00
.gitignore 64-bit Curve25519 is constant time and passes all the Wycheproof vectors! 2026-07-30 20:52:02 -05:00
.gitmodules Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
build.py Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
flake.lock Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
flake.nix Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
justfile Completely overhauled build system, no more Meson 2026-08-13 21:32:39 -05:00
LICENSE License and README updates 2026-08-05 23:08:02 -05:00
README.md License and README updates 2026-08-05 23:08:02 -05:00

TinyCrypT

Drawing of Penelope, After Attic Red Figure

If you are reading this on GitHub, this is a read-only mirror of the original. Submit any issues, pull requests, or whatever there.

Collection of classical cryptographic primitives written in portable C90 (with optional GNU extensions also supported by Clang) with no dependencies (including the standard library), optimized for correctness, soundness, portability, and speed in that order.

Algorithms

  • ChaCha20-Poly1305 for combined encryption and MAC
  • KangarooTwelve128 and TurboSHAKE128 for extendable-output hashing
  • Curve25519 for elliptic-curve Diffie-Hellman key exchange
  • SHA-256 and SHA-512 for hashing, ECDH, and Ed25519
  • Ed25519 for EdDSA

Testing Validations

  • The SHA-2 implementations pass all 586 NIST-provided test cases.
  • The ChaCha20-Poly1305 implementations pass the test vectors provided in the RFC (integrating Wycheproof tests is in progress).
  • The Ed25519 implementation passes all 4096 test cases from libgcrypt and all Wycheproof test cases.
  • The Curve25519 implementation passes all Wycheproof test cases and all test vectors provided in the RFC.

Proof Validations

  • The SHA-2 implementations can be proven to be memory-sound using Frama-C with the WP plugin (provided one follows the contract outlined in the header).
  • The 64-bit Curve25519 implementation can be proven to be constant time and avoid cache timing side channels when compiled for x86-64 (with or without AVX2) using BINSEC/SSE (note that the 32-bit implementation is not yet constant time).
  • The 64-bit and 32-bit SHA-256 implementations can be proven to be constant time (except in the length of the input data, of course) and avoid cache timing side channels for input lengths up to 4KiB when compiled for x86-64 (with or without AVX2) or ARM Cortex-A, again using BINSEC/SSE (proving this for other builds and longer inputs is in progress, the proof takes a long time).

Benchmarking

  • The 64-bit implementation of Ed25519 (automatically compiled against when the target platform supports __uint128_t) is able to generate a signature on 16KiB of data in 0.12ms on an Intel Core i3-1315U processor (single core).
  • The SIMD implementation of ChaCha20-Poly1305 (which requires GNU vector extensions, which are supported in Clang) is able to encrypt, authenticate, decrypt, and verify 1GiB of data in 0.81s on an Intel Core i3-1315U processor (single core).

Current Issues

  • Frama-C/WP memory soundness proofs are still being developed for most of the codebase, and that includes occasionally finding bugs.
  • There is currently no CI pipeline, and all tests and proofs are done ad-hoc during development.
  • The 32-bit Curve25519 implementation is not yet constant time and relies on relatively slow Barrett reductions.