Altran Praxis and AdaCore Release Open Source SPARK Implementation of Skein Algorithm

SPARKSkein reference implementation achieves success ahead of Crypto 2010 conference

NEW YORK, PARIS, and BATH, England, - Crypto 2010 Conference - 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.”

“ Eric Botcazou, GCC expert and consultant at AdaCore provided the optimization and performance analysis for the project. He added, “The results clearly demonstrate that the SPARKSkein code is easy to understand and read, while the performance is at a comparable speed to the C code. This is solid evidence that any ‘formal’ code developed in this way doesn’t have to be slow and impractical.”

About Altran Praxis
Altran Praxis is a specialist systems and software house, focused on the engineering of systems with demanding safety, security or innovation requirements. Altran Praxis leads the world in specific areas of advanced systems engineering and innovation such as: ultra low defect software engineering, Human Machine Interface (HMI), safety engineering for complex or novel systems and tools/methods (such as SPARK) for systems engineering. It offers clients a range of services including turnkey systems development, consultancy, training and R&D. Key market sectors are aerospace and defence, rail, nuclear, air traffic management, automotive, medical and security.

The company operates globally with active projects in the US, Asia and Europe. The headquarters of Altran Praxis are in Bath (UK) with offices in Sophia Antipolis, London, Paris, Loughborough and Bangalore. Altran Praxis is an expertise centre within, and wholly owned by, Altran which is a global leader in innovation engineering and employs 17,000 staff across the world. www.altran-praxis.com

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, the state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore’s flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see www.adacore.com/home/company/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railway systems and medical devices, and in security-sensitive domains such as financial services.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com