libkeccak

The security of any system can only be as strong as its weakest links. However, cryptographic libraries often require a higher level of scrutiny because of the complexity of their algorithms and implementations. This is why SPARK’s formal verification approach is a very powerful solution for the development and maintenance of such components.

Daniel King delivers a very good example with the libkeccak project. An implementation of the keccak cryptographic hash which has been selected by the National Institute of Standards and Technology (NIST) for the SHA-3 standard. I am not going to delve into details here because Daniel already published on our blog this article about his project a few months ago.

Daniel published the article a couple of weeks after a critical vulnerability in the keccak reference implementation was disclosed: an overflow on integer addition leading to a buffer overflow. This is an example of how memory vulnerabilities are often the result of a computation error beforehand. The vulnerability remained undetected for more than a decade. As mentioned recently in the case study we published with the NVIDIA Security Team, “traditional” means of software validations are not sufficient to ensure security. With SPARK, Daniel was able to prove that none of those run-time errors can occur for any possible input to the library.