-rw-r--r-- 2260 libntruprime-20240825/doc/verification.md raw
libntruprime is intended to become
a central target for verification of
full functional correctness of implementations of `sntrup`.
Full functional correctness of an `sntrup` implementation
means that the implementation computes the same
output as the
[NTRU Prime Sage package](https://ntruprime.cr.yp.to/software.html)
for all possible inputs.
This document tracks what has been verified so far and what has not.

Changes in C compilers and in assemblers often change the behavior of
software and might introduce bugs where no bugs existed before.
Some tools address this
by verifying correctness at the machine-language level.
It is important to re-run these tools whenever new binaries are produced.

Changes in CPUs can also introduce bugs where no bugs existed before.
Verification is always relative to a model of CPU behavior,
and physical CPUs often deviate from these models,
sometimes in problematic ways.

There is also a risk that current or future versions of Sage
do not correctly compute the documented Sage functions
used by the Sage package.
This can interfere with falsifiability:
even if the CPU matches the model,
a bug in an `sntrup` implementation could be hidden by a bug in Sage.

The `supercop/crypto_kem/sntrup*` checksums
match the checksums produced by libntruprime
and checksums produced by the Sage package.
These checksums are hashes of outputs
for various pseudorandomly generated inputs
(with randomness treated as another input).
However, there could be bugs for other inputs.

Various runs under `valgrind` and `asan`
have not detected any abnormal use of RAM.
However, `valgrind` will not notice overflows from a C variable into an adjacent C variable;
`asan` will not notice overflows in assembly language;
and neither tool addresses the risk of bugs for rare inputs.

The NTT software used inside libntruprime comes from
[nttcompiler](https://pqsrc.cr.yp.to/nttcompiler.html)
and has been computer-verified to work correctly on all inputs.
The sorting software used inside libntruprime
comes from
[djbsort](https://sorting.cr.yp.to)
and has also been computer-verified to work correctly on all inputs.
However,
there could be bugs in the verification tools,
and there are other computations happening inside libntruprime.