SPARKSkein: A Formal and Fast Reference Implementation of Skein

  • Roderick Chapman
  • Eric Botcazou
  • Angela Wallenburg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)


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.


Skein Hash SHA-3 SPARK Theorem Proving GCC Optimization Verification Security 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Skein project homepage,
  2. 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. 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. 4.
  5. 5.
    SPARK GPL Edition site,
  6. 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),
  7. 7.
    Z3: An efficient theorem prover. Microsoft Research,
  8. 8.
    Alt-Ergo website,
  9. 9.
    Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)CrossRefzbMATHGoogle Scholar
  10. 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. 11.
    VCC: A Verifier for Concurrent C,
  12. 12.
    National Institute of Standards and Technology, Computer Security and Resource Center, Cryptographic Hash Algorithm Competition,
  13. 13.
    The Skein Hash Function Family, Ferguson, N., et al.,

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Roderick Chapman
    • 1
  • Eric Botcazou
    • 2
  • Angela Wallenburg
    • 1
  1. 1.Altran Praxis LimitedBathU.K.
  2. 2.AdaCoreParisFrance

Personalised recommendations