SPARKSkein: A Formal and Fast Reference Implementation of Skein
- 3 Citations
- 290 Downloads
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.
Keywords
Skein Hash SHA-3 SPARK Theorem Proving GCC Optimization Verification SecurityPreview
Unable to display preview. Download preview PDF.
References
- 1.Skein project homepage, http://www.skein-hash.info/
- 2.Carré, B., Bergeretti, F.: Data- and Information-Flow Analysis of While Programs. ACM Transactions on Programming Languages and Systems 7(1), 36–61 (1985)zbMATHGoogle Scholar
- 3.Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley (2003) (reprinted in 2007) ISBN 978-0-321-13616-0Google Scholar
- 4.Tokeneer Discovery: A SPARK Tutorial, http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/
- 5.SPARK GPL Edition site, http://libre.adacore.com/
- 6.Jackson, P.B., Ellis, B.J., Sharp, K.: Using SMT Solvers to Verify High-Integrity Programs. In: 2nd International Workshop on Automated Formal Methods, AFM 2007, Atlanta, Georgia, USA (2007), http://homepages.inf.ed.ac.uk/pbj/
- 7.Z3: An efficient theorem prover. Microsoft Research, http://research.microsoft.com/enus/um/redmond/projects/z3/
- 8.Alt-Ergo website, http://alt-ergo.lri.fr/
- 9.Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)CrossRefzbMATHGoogle Scholar
- 10.Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven, Belgium (August 2008)Google Scholar
- 11.VCC: A Verifier for Concurrent C, http://research.microsoft.com/en-us/projects/vcc/
- 12.National Institute of Standards and Technology, Computer Security and Resource Center, Cryptographic Hash Algorithm Competition, http://csrc.nist.gov/groups/ST/hash/sha-3/index.html
- 13.The Skein Hash Function Family, Ferguson, N., et al., http://www.skein-hash.info/sites/default/files/skein1.1.pdf