Please do not open a public issue for a suspected vulnerability. Use the repository's Security → Report a vulnerability private advisory form, or email the maintainer at ville@vesilehto.fi. Include the affected revision, a reproducer if possible, and your assessment of impact. Receipt should be acknowledged within seven days.
Not independently audited. No release should be described as audited unless the audit and the exact audited revision are linked from this file. Passing test vectors, differential tests and tool-based constant-time checks is evidence of correctness, not a security review.
curve448 has two implementations of the same algorithms: the pure OCaml default, curve448.ocaml (lib/ocaml/), and the optional curve448.c (lib/c/). See docs/design.md.
lib/c/native/p448_64.h) is generated by fiat-crypto, which proves its functional correctness within stated limb bounds. The wrappers use distinct C types for the two bound classes. The proof covers fiat-crypto's model of C; it does not cover the C compiler.lib/ocaml/fe448_kernels.ml) are generated by tools/gen_fe448_ocaml.py, which proves by interval arithmetic that no intermediate overflows the 63-bit integer range and that outputs meet the bound the next operation assumes, and checks every kernel on random and extreme inputs. This is a machine-checked argument about the generated statements, not a formal proof in a proof assistant, and the rest of lib/ocaml/fe448.ml is hand-written.docs/testing.md.Both implementations are written to avoid branches and memory access that depend on secret data (private scalars, seeds, nonce prefixes and nonces). Every scalar multiplication, including those in verification, uses the same constant-time algorithms; verification branches only on public validity checks (lengths, point encodings, S < L). See docs/design.md.
This has been checked, not proven:
tools/ctgrind runs key derivation, X448, Ed448 and Ed448ph signing, and the variable-base scalar multiplication used in verification (with a secret scalar and point) under Valgrind memcheck with secrets marked undefined: with GCC 13.3 and Clang 18.1 at -O1, -O2, -O3 and -Os on aarch64 Linux and x86-64 Linux, and with GCC 16.2 and Clang 22.1 at the same levels on x86-64 Linux.Array.fill on an array in the major heap compares each old element with the new value. The OCaml backend now writes secret arrays only with plain stores, and CI rejects Array.fill and Array.blit in lib/ocaml/. With OCaml 4.14 the runs suppress conditional jumps inside the garbage collector's scanning functions (tools/ctgrind/ocaml/runtime.supp), which test the always-set tag bit of integers that Valgrind's approximation of multiplication marks undefined.Array.fill were also confirmed to be reported. The checks cover the paths those inputs take, under those compilers and architectures; they do not cover other compilers or compiler versions, Apple clang, flambda builds, or OCaml 5 on arm64, where OCaml's code saves return addresses below the stack pointer and Valgrind reports invalid accesses from the first line of the program.compiler/inspect_ocaml_native.sh disassembles the OCaml archive and fails if a generated field kernel contains a conditional branch other than a prologue stack check, or calls into the runtime (which would mean an allocation). It passes with OCaml 4.14.4, 5.2.1 and 5.5.1 on x86-64 Linux, 4.14.1 and 5.4.1 (also with flambda at -O3) on arm64 Linux, and 5.4.1 on arm64 macOS, and CI runs it with OCaml 4.14 and 5.5. The Valgrind harness also checks that the kernels do not allocate, which holds for every compiler above, including flambda at -O2 and -O3. These check control flow and allocation only, and only for those kernels.bench/timing_ocaml.exe and bench/timing_c.exe find no timing difference between fixed and random secrets on an Apple M1 Pro and an AMD Ryzen AI 9 HX PRO 370. Wall-clock measurements can only reveal gross leaks.OCaml gives no constant-time guarantees for its compiler, runtime or garbage collector. The OCaml backend relies on ocamlopt compiling integer arithmetic, shifts and masks to the corresponding machine instructions, on allocation and garbage collection happening at points fixed by the code rather than by data, and on not calling runtime primitives that inspect the contents of arrays holding secrets. The C backend's OCaml layer does not branch on secrets.
X448.secret and Ed448.priv hold key bytes in ordinary OCaml strings. The garbage collector may copy them, and they cannot be reliably erased.Mirage_crypto_rng. The application must initialise a cryptographically secure generator, for example with Mirage_crypto_rng_unix.use_default (), and concurrent key generation is only as safe as that generator: use_default reads getrandom/getentropy per request, while mirage-crypto-rng documents that a Fortuna generator must not be used concurrently. curve448 itself keeps no global mutable state.`Low_order when the shared secret is all zero. TLS 1.3 and HPKE require callers to reject that case; with this API they cannot forget to.docs/interoperability.md.docs/interoperability.md) are accepted by pub_of_octets, as RFC 8032 specifies. Under such a key, some signature verifies for every message. Protocols that rely on a signature binding a message to an honestly generated key must reject those encodings.curve448.ocaml: OCaml 4.14 or later with 63-bit integers (a 64-bit native or bytecode runtime). On a 32-bit runtime or js_of_ocaml the library fails when it is initialised rather than computing wrong results.curve448.c: additionally a 64-bit C compiler with unsigned __int128 (GCC or Clang). Dune does not build curve448.c on other targets, so selecting it there fails at build time rather than falling back to untested code.