Formal methods progress

[gmaxwell]

So far we have manually checkable proofs for the field mul and square inner loops, and machine verification (via frama-c) of overflow-freeness for 10x26 (5x52 requires hacking on frama-c to get a 128 bit type into it.)

I believe know how to machine check the field and scalar in a reasonable amount of time, but not straight from the C; so the effort would be one-time and rot, and I'm not sure it's worth the time.

There may be other areas of the code that are good targets for formal methods. I'd hoped previously to get some researchers working in this space interested; but so far no luck.

[roconnor-blockstream]

@andres-erbsen I can start.

I've done verification of the int128_struct module using VST. The specification and proofs can be found at https://github.com/BlockstreamResearch/simplicity/blob/139ab8d6f455e8d1cc10ad3693e917d2852e1bf3/Coq/C/secp256k1/verif_int128_impl.v, and there is a interactive log of the proof at https://htmlpreview.github.io/?https://github.com/ElementsProject/simplicity/blob/139ab8d6f455e8d1cc10ad3693e917d2852e1bf3/alectryon/verif_int128_impl.v.html

I'm working my way from the bottom up, and the int128_struct module is one of the main leaves of the development, upon which the field, scalar, and modular inverse operations are built upon.

For licensing reasons, the proof lives in the Simplicity project, and will be limited in scope to those parts of libsecp256k1 that have been imported into the Simplicity project.

Lately I've been working on the correctness of the modular inverse operations. This fits in with our existing proof of the termination of the safeGCD algorithm at https://medium.com/blockstream/a-formal-proof-of-safegcd-bounds-695e1735a348 and is more interesting for vetting the VST tool since it is full of loops and breaks and branches, whereas a lot of the other libsecp256k1 code is straight-line and branchless (for good reason of course) . I don't have a public branch at this time, but I'm at approximately line 265:

https://github.com/BlockstreamResearch/simplicity/blob/139ab8d6f455e8d1cc10ad3693e917d2852e1bf3/C/secp256k1/modinv64_impl.h#L265

(Note however secp256k1_modinv64_divsteps_59 has been excluded from verification as it is not used in Simplicity.)

My current plan is to finish off the proof of secp256k1_modinv64_divsteps_62_var and then turn my attention to the field_inner_mul operations for comparison with fiat-crypto. I had done an early test of verifying these operations in VST a long time ago.

[roconnor-blockstream]

I've finished the correctness proofs in VST of secp256k1_fe_mul_inner and secp256k1_fe_sqr_inner. You can find the rendered proof at https://htmlpreview.github.io/?https://github.com/ElementsProject/simplicity/blob/verif_field_5x52_int128_impl_0/alectryon/verif_field_5x52_int128_impl.v.html.

The more relevant bit is the formal specification of the functions that the proofs relate to. These are secp256k1_fe_mul_inner_spec and secp256k1_fe_sqr_inner_spec which have rendered versions at https://htmlpreview.github.io/?https://github.com/ElementsProject/simplicity/blob/verif_field_5x52_int128_impl_0/alectryon/spec_field_5x52.v.html.

These specifications are written in the formal separation logic language of VST. These specification are made somewhat complicated by needing to support the fact that the r parameter may or may not alias the a parameter. To that end, I've written "sub-specifications" secp256k1_fe_mul_inner_spec_restrict and secp256k1_fe_mul_inner_spec_alias which provided somewhat simpler specification for the specific cases where r does not/does alias a. These sub-specifications can be found in the same file, along with the proofs that these are indeed sub-specifications of the formal specification.

More at https://github.com/bitcoin-core/secp256k1/pull/1319#issuecomment-1821834018.