Home > Products > Altran Praxis and AdaCore release open source SPARK Implementation of SPARK Algorithm

Design

Altran Praxis and AdaCore release open source SPARK Implementation of SPARK Algorithm

16th August 2010

Altran

ES Admin

0 0

Altran Praxis and AdaCore today announced a new reference implementation of the Skein algorithm, written and verified using the GPL 2010 Edition of the SPARK language and toolset. Skein is a cryptographic hash function and an entrant in the National Institute of Standards and Technology (NIST) hash function competition to design what will become the new Secure Hash Algorithm (SHA-3) standard. Such hash functions are used to compute short “digests” of long messages, and are one of the key building blocks of digital communication and cryptographic systems. Altran Praxis and AdaCore have open sourced the SPARKSkein reference implementation and made it available to the developer community via the Skein website. This is in time for the second SHA-3 candidate conference taking place at the Crypto 2010 conference, Santa Barbara, California, USA, from 23-24 August 2010.

The joint Altran Praxis and AdaCore project began as an informal experiment to demonstrate whether a hash algorithm like Skein could be realistically implemented in SPARK. The goals of the implementation were:

· Readability – to strike a reasonable balance of readability and performance.

· Portability – the team aimed for a single code-base that was portable and correct on all target machines of any word size and endian-ness, with no macros, ‘ifdefs’, or pre-processing of any kind.

· Performance – to ensure that the performance of the SPARK code would be close to or better than the existing C reference implementation.

· Formality – to prove at least type-safety (i.e., no exceptions) on the SPARKSkein code. The team wanted to use the experiment to refute the claim that ‘formal is slow’ in programming languages.

The project concluded with notable success, proving that an algorithm like Skein can be written in a ‘formal’ language like SPARK without sacrificing readability or performance. Furthermore, portability was achieved. A single set of sources yielded identical results on more than fifteen platforms, covering a wide range of microprocessors and operating systems. In addition, SPARK’s type-safe nature allowed the project team to maximize compiler optimization with confidence.

Professor Stefan Lucks, a member of the Skein design team, said, Speaking for the Skein design team, we're very impressed by this work. SPARKSkein isn't just another implementation of Skein - essential properties of this implementation have been formally verified. It is stunning how the formal verification of the SPARK source code actually made us discover a flaw in our own reference C implementation.. Personally, I also find the SPARK code to be more readable than the equivalent C.

Rod Chapman, a Principal Engineer at Altran Praxis, led the SPARKSkein project. He said, “This is an incredibly exciting project for us to be involved in. By open sourcing the code and donating our work, we hope to make a valuable contribution to the scientific community, as well as to showcase the capability of SPARK and its verification tools.”