SPARKSkein - a formal and fast reference implementation of Skein
Rod Chapman ( Praxis )
- 11:30 2nd September 2010 ( Michaelmas Term 2010 )Room 478, Oxford University Computing Laboratory
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.