Technical Papers

SPARKSkein: A Formal and Fast Reference Implementation of Skein

This paper describes SPARKSkein - a new reference implementation of the Skein cryptographic hash 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 original reference implementation which 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 performance to the existing C reference implementation. As a further result of this work, we have identified several opportunities to improve both the SPARK tools and GCC.

The final publication is available at Springer

Attached Files

posted in GNAT Pro, SPARK Pro, SPARK Pro, Certification, Formal Methods, High Security Development, Open Source