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
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 and has been computer-verified to work correctly on all inputs. The sorting software used inside libntruprime comes from djbsort 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.
Version: This is version 2024.08.15 of the "Verification" web page.