SPARKSkein – A Formal and Fast Reference Implementation of the Skein Hash Algorithm

Abstract:

This poster describes SPARKSkein – a new reference implementation of the Skein algorithm. Skein is a cryptographic “hash” algorithm – one of the basic building blocks of integrity and authentication in digital communications. Skein is one of the final five candidate algorithms in competition to become the new international standard hash algorithm. The designers of Skein have provided a “reference implementation” written in C. Such reference implementations are supposed to be readable, “obviously correct”, portable, and provide reasonable performance on contemporary hardware.

This poster reports our experience in re-implementing Skein in SPARK – a programming language and verification toolset that is consciously designed for the development of high-assurance software. Unusually, SPARK offers a formal semantics and a verification system based on Hoare-logic and theorem proving, but retains the “low level” features needed to implement real-time code, so it seemed like an interesting idea to see if Skein could be implemented in SPARK without compromise.

The new implementation is readable, completely portable to a wide-variety of machines, and “formal” in that it is subject to a completely automated proof of type safety. This proof also identified a subtle bug in the implementation (an integer overflow which leads to an undefined output hash) that persists in the C version of the code. Performance testing has been carried out using three generations of the GCC compiler. With the latest compiler, the SPARK code offers identical or better performance to the existing C reference implementation at all optimization levels. As a further result of this work, we have identified several opportunities to improve both the SPARK verification tools and GCC.

Finally, in the interests of empirical engineering, the entire SPARKSkein release and the supporting tools have been made freely available.

Biography:

Roderick Chapman is a principle engineer at Altran Praxis, specializing in many aspects of high-integrity systems development. He has made significant contributions to the Correctness by Construction approach, and is currently the technical authority for the SPARK Product Group at Praxis. He is a regular invited speaker at international conferences, and is widely recognized as a leading authority on high-integrity software development, programming language design, and software verification tools.

In 2006, Rod was invited (at the age of just 37) to become a Fellow of the British Computer Society. More recently, Rod has turned his attention to software process, working on merging the discipline of traditional high-integrity process with more agile approaches such as XP, and the philosophy of the Lean Engineering movement. As part of this work, Rod is leading the roll out of PSP within the company. In 2011, Rod was the join recipient of the first Microsoft Research Verified Software Milestone Award for his contribution to the Tokeneer project.