LoupVaillant
commented
1 year ago Done for Poly1305.
After a bit of investigation, Curve25519 looks like it will require more effort. And since that code is pulled from SUPERCOP Ref10, which shows signs of having been formally verified itself, pushing any further doesn't seem worth it.
So let's close this and push the remaining work way down the priority list.
Bignum arithmetic is the most error prone part of Monocypher. Especially difficult to test for are limb overflows, which when coupled with delayed carry propagation tend not to be caught by random tests. Thus only way to be sure is to prove the impossibility of overflow, given invariants, and then make sure those invariants are respected.
So far Monocypher has relied on hand-written proofs. They do give confidence, machine checked proofs give even more confidence, and are easier to audit. It is especially important when some tool give cause to doubt the correctness of the code.
Thus, bignum arithmetic should be subjected to formal proofs. At the algorithmic level at least, but ideally by directly parsing the C code. The priority here is to prove the absence of limb overflow. Full correctness can probably rely on regular tests.