Paper Info
Title
SPARKSkein: a formal and fast reference implementation of skein
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-25032-3_2
SBMF
Keywords
Field
DocType
new reference implementation,existing c reference implementation,c version,new implementation,spark code,gcc compiler,spark language,fast reference implementation,identical performance,spark tool,original reference implementation
Programming language,Spark (mathematics),Software engineering,Computer science,Cryptographic hash function,SHA-3,Compiler,Theoretical computer science,Reference implementation,Skein,Hash function,Type safety
Conference
Volume
ISSN
Citations 
7021
0302-9743
2
PageRank 
References 
Authors
0.43
1
3
Name
Order
Citations
PageRank
Roderick Chapman112010.62
Eric Botcazou220.77
Angela Wallenburg3263.46