The National Institute of Science and Technology (NIST) is looking for a better cryptographic hash function. The body has been considering submitted algorithms for over a year now in an effort to pick one to become SHA-3 (the Secure Hash Algorithm), but at least one developer in the U.K. decided to implement one of the competitors himself before a winner is crowned.

Rod Chapman, principal engineer of software house Altran Praxis, said he decided to implement the Skein algorithm in order to give the SPARK programming language a real workout. His company developed SPARK, which is a subset of Ada and designed for use in real-time, high-security environments and embedded systems. SPARK is built to make provably correct applications, and to limit the possibility of errors hidden in the code.

So when Chapman heard about the Skein algorithm and its submission to NIST as one of 14 potential SHA-3 candidates, he decided to use the algorithm as a test project for SPARK. “Some of our customers are doing high-grade security stuff,” he said. “When I came across Skein and the SHA-3 competition, I wondered if I could implement one of these in SPARK. I wondered if I could do a better implementation.”

Chapman said that the reference implementation was written in C, which facilitated recoding it in SPARK. “I wanted to make the code as readable as possible,” he said. “I wanted to make it portable, so the same code with no modification would theoretically run on any computer with any compiler regardless of word size. I wanted to do a proof of type safety, and finally the most ambitious goal was to see if I could come up with a new implementation that would at least be competitive with the C code.”

Once the code was up and running, Chapman was able to do a deep round of optimization in GCC, the compiler used at Altran Praxis to compile Ada and SPARK code.

“We’ve tried it with various builds of the GCC compiler. We can use the same compiler to compile C and the SPARK code, so hopefully that puts us on even footing to compare with C. We’re now about 5 to 10% slower than the C code. We’re down to 13 clock cycles per byte,” said Chapman. “I’m sure we can get that 10% back. I wrote this up as an example of how this sort of thing can be done.”

Chapman said he was confident that further optimizations would bring the code to performance par with the C implementation.

The creators of the Skein algorithm were impressed with Chapman’s work, he said, and asked him to open-source the project so that others could see what the code looked like behind the curtains. And while Chapman said that he made great effort to keep the code readable, he admits that most developers are unfamiliar with Ada, making it tough for them to read SPARK.

Still, he hopes people will use his implementation, regardless of whether or not the Skein algorithm wins the competition to become the next SHA.