Finding meaning in cryptographic verification: Methods in the verification of post-quantum cryptography

The hope of formal verification of the assurance of cryptographic software — both
their designs and their implementations — is that we end up with higher-assurance
and generally better cryptography as a result. How realistic is this? Many different
tools exist for this purpose, and many papers are published every year purporting
to tackle this task better, and yet during even the time of our research NIST has
evaluated candidates for and published new standards for post-quantum cryptogra-
phy with little use of verification tooling in the evaluation or improvement of the
candidates in that process. Moreover, it is not uncommon to tackle verification only
to find partial success, or to derive results that must be heavily caveated.

The question therefore arises: what is the meaning of cryptographic verification?
When different tools are used for the verification of cryptographic designs and im-
plementations, what is the form of the artifacts produced? How can we evaluate
the usefulness, value, and inferential significance of a given piece of verification and
the artifacts it produces? How does the particular verification methodology and
verification tools employed affect the success of a piece of verification and the use
of the artifacts it produces?

We tackle these questions through a series of case studies, primarily targeting
different approaches towards the functional verification of aspects of the Classic
McEliece cryptosystem, though with some forays into correctness verification of its
underlying design and some exploration of the SIKE cryptosystem as a comparator
in one area. Our motivation is to always return to the practical matter of “what
works” — what verification tools are suitable in what circumstances, what do we
learn in practice from them, and what techniques must be employed to get the most
out of them.