SPARKNaCl: A verified, fast cryptographic library
Rod Chapman
Director, Protean Code
SPARKNaCl https://github.com/rod-chapman/SPARKNaCl is a new, freely-available, verified and fast reference implementation of the NaCl cryptographic API, based on the TweetNaCl distribution. It has a fully automated, complete and sound proof of type-safety and several key correctness properties. In addition, the code is surprisingly fast - out-performing TweetNaCl's C implementation on an Ed25519 Sign operation by a factor of 3 at all optimisation levels on a 32-bit RISC-V bare-metal machine. This talk will concentrate on how "Proof Driven Optimisation" can result in code that is both correct and fast.
About Rod Chapman
Dr Roderick Chapman is an independent consultant software engineer: https://www.proteancode.com/. He specialises in the development of safety and security-critical systems, from requirements engineering, through architectural design and implementation, to verification, audit and assessment. He has particular interest in the software implementation and verification of cryptographic algorithms and protocols. He is a Fellow of both the BCS and IET and holds an honorary visiting chair in computer science at the University of York.Sponsored by
