TweetNaCl is a compact reference implementation of the NaCl API. It was initially constructed to show that an entire crypto library could fit into "100 tweets", but has since been re-used in some critical applications, such as the WireGuard VPN. There are no comments in the code at all, and all assurance rests on a single brief academic paper, and the formidable reputation of the authors.

Can we do better? Can we produce a reference implementation which is amenable to automatic verification and yet is competitive with TweetNaCl in terms of performance and code size?

This talk presents SPARKNaCl - a complete re-implementation of TweetNaCl in SPARK, which comes with a fully automated proof of type-safety, memory-safety and a number of key correctness properties. Having established a solid foundation, we went on to compare the performance and code size of SPARKNaCl against the original C implementation. Various transformations and optimizations have been applied that result in SPARKNaCl out-performing TweetNaCl on a bare-metal 32-bit RISC-V machine for a single Ed25519 "Sign" operation, while retaining automation and completeness of the proof. Furthermore, SPARKNaCl is freely available under the 3-clause BSD licence.

This talk will present an overview of the results from both the proof work and performance analysis of SPARKNaCl.