package curve448

Security policy

Reporting a vulnerability

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.

Audit status

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.

What is verified and what is tested

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.

• C field arithmetic (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.
• OCaml field kernels (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.
• Everything else, in both implementations (scalar arithmetic modulo L, SHAKE256, the X448 ladder, edwards448 formulas and scalar multiplication, Ed448 signing and verification, and the C bindings), is hand-written or generated without proof, and is not formally verified. It is tested against RFC and Wycheproof vectors, an independent Zarith model, OpenSSL 3 and CIRCL, with property tests and fuzzing, and a mutation check confirms the suite detects representative bugs in each implementation. The two implementations share no arithmetic code and agree on every test and differential input. See docs/testing.md.

Side-channel boundary

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:

• Valgrind, C. 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.
• Valgrind, OCaml. The same operations of the OCaml backend, compiled with ocamlopt 4.14.1 on aarch64 and x86-64 Linux and with ocamlopt 5.4.1 and 5.5.1 on x86-64 Linux, each run twice: as is, and with a minor collection forced at every allocation, so that buffers holding secrets are in the major heap whenever later code touches them. This check found, and led to the removal of, a secret-dependent branch inside the runtime: 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.
• Each Valgrind build includes a self-test with a deliberate secret-indexed lookup and secret branch, which must be reported, so the harness cannot pass vacuously; for the OCaml backend, a planted secret branch in the library's table selection and a reinstated 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.
• Compiled kernels, OCaml. 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.
• Timing. 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.
• Not addressed: power and electromagnetic analysis, fault injection, speculative-execution attacks, and microarchitectural effects such as data-dependent multiplier timing.

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.

Secret material

• X448.secret and Ed448.priv hold key bytes in ordinary OCaml strings. The garbage collector may copy them, and they cannot be reliably erased.
• The top-level functions of both implementations overwrite the buffers they create for secrets (the X448 ladder state, expanded keys, nonce prefixes, nonces and digests) before returning. In C, temporaries inside lower-level helpers (point formulas, table selection, Keccak rounds) are not wiped. In OCaml, a buffer may already have been copied by the garbage collector when it is overwritten, and values in registers and stack slots are not wiped. Neither is a zeroisation guarantee.
• Key generation takes randomness from 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.

Protocol-relevant behaviour

• X448 accepts every 56-byte public value, as RFC 7748 requires, and returns `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.
• Ed448 verification rejects non-canonical point encodings and S >= L, so signatures are not malleable, and uses RFC 8032's cofactored equation. CIRCL rejects some signatures that pass the cofactored check (R with a small-order component); honest signers never produce them. See docs/interoperability.md.
• Small-order Ed448 public keys (four encodings, listed in 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.
• Contexts and variants. Ed448 always binds the context (default empty) and distinguishes Ed448 from Ed448ph. A signature is valid only for the context and variant it was made with.

Platform requirements

• 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.