Introducing SPARKNaCl – a verified crypto library

Here’s some new software that I’ve been working on in my spare time over the last few months. I’ve decided to make the code freely available under the simplified BSD licence.

SPARKNaCl is a SPARK 2014 implemenation of the NaCl cryptographic library, based on the minimalistic TweetNaCl code from Daniel J. Bernstein and his colleagues.

SPARKNaCl has been verified “type-safe” (aka “no runtime errors”) by the SPARK toolset, and the proof is fully “auto-active” meaning the standard set of provers discharge every single verification condition, with no interactive proof at all, based solely on the contracts in the code and nothing else. In addition, some interesting correctness properties have been verified en-passant.

This was all something of a challenge – cryptographic code like TweetNaCl sets some particularly difficult challenges for both the human brain and for automated verification tools alike. Read all about it here.