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.”