SPARKSkein - a formal and fast reference implementation of Skein

Rod Chapman (Praxis)

Info

Date	2nd September 2010 (week , Michaelmas Term 2010)
Time	11:30
Place	Room 478, Oxford University Computing Laboratory

Abstract

This talk describes SPARKSkein - a new reference implementation of the Skein algorithm, written and verified using the SPARK language and toolset. The new implementation is readable, completely portable to a wide-variety of machines of differing word-sizes and endian-ness, and "formal" in that it is subject to a proof of type safety. This proof also identified a subtle bug in the implementation which persists in the C version of the code. The new code offers similar performance to the existing reference implementation. As a further result of this work, we have identified several opportunities to improve both the SPARK tools and GCC.