Formal verification of cryptographic software at AWS - Current practices and future trends

It appears that the winds-of-change are blowing for formal verification of cryptographic software and, furthermore, those winds are blowing in the same direction. We perceive progress on several fronts:

- Researchers in the mathematics of cryptography now publish formal specifications and proofs of security properties as a matter of course in their papers using language like EasyCrypt[10].
- Formal (yet executable) specification languages for cryptographic algorithms, such as Cryptol[11], are finally achieving acceptance and wider use within industry and government.
- There has been substantial progress in automated synthesis and verification of cryptographic software, including the work of Fiat Crypto[12], the Jasmin language and toolset[13], Hax[14], our own efforts, and many others.
- Governments are other standard-setting bodies are recognizing the importance of memory- and type-safe programming for critical applications.
- “Evidence-based” or “Principles-based” assurance[8] is gaining ground, following many years of use in the safety-critical domain.
- IETF have recently stood up a new “Usable Formal Methods Research Group”[15] to explore how formal notations and methods can improve IETF’s work in the future.

In light of these trends, the time is right to open discussion on how formal verification can influence the future development, verification and certification of cryptographic software.