Advertisement

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)

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 Security 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Skein project homepage, http://www.skein-hash.info/
  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, http://libre.adacore.com/
  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), http://homepages.inf.ed.ac.uk/pbj/
  7. 7.
    Z3: An efficient theorem prover. Microsoft Research, http://research.microsoft.com/enus/um/redmond/projects/z3/
  8. 8.
    Alt-Ergo website, http://alt-ergo.lri.fr/
  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, http://research.microsoft.com/en-us/projects/vcc/
  12. 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. 13.
    The Skein Hash Function Family, Ferguson, N., et al., http://www.skein-hash.info/sites/default/files/skein1.1.pdf

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