The US National Institute of Standards and Technology (NIST) publishes a number of important cryptographic standards (including upcoming ones for post-quantum cryptography), and runs the cryptographic algorithm and module validation programs that validate and issue certificates to cryptographic libraries.

Last week, at the National CyberSecurity Center of Excellence in Maryland, NIST hosted a workshop on Formal Methods within Certification Programs. The idea behind the workshop was to bring together formal methods researchers and practitioners (like ourselves) with various certification labs and the NIST validation teams, with the goal of investigating how formal methods could be used to improve certification processes.

A key observation by many speakers was that the first step towards the use of formal methods is developing and publishing readable, executable formal specifications of standardized algorithms. In our own talk, titled “Formal Specifications for Certifiable Cryptography”, we and our co-authors surveyed various approaches towards formal specifications and suggested several ways forward on incorporating them within standards and certification processes.

In particular, we pointed out that formal specifications serve three purposes: guiding implementations, enabling security proofs, and providing a target for implementation verification and testing. It is hard for a single language to serve all of these purposes, but tools can help link formal specifications written in different languages. For example, at Cryspen, we help develop hacspec, a language for cryptographic specifications that can be translated to proof-oriented languages like ProVerif, F*, and Coq, using the hax toolchain.

There were many interesting talks and discussions, and the group came up with several concrete next steps towards the eventual goal of integrating formal methods more closely with certification.

The slides for our talk are available here.

If you have any questions about hacspec, hax, and how they can help you to improve the quality of your own software products or the cryptographic libraries you depend upon, drop us an email.