SPARKSkein released

1 view
Skip to first unread message

Rod Chapman

unread,
Aug 16, 2010, 3:37:59 AM8/16/10
to
Altran Praxis and AdaCore have released SPARKSkein - a new reference
implementation of Skein-512 written and verified using the SPARK
language and toolset. In particular, this release includes a complete
proof of type-safety for the implementation, test cases for structural
coverage, performance, and the reference test vectors from the Skein
specification. Performance is very close to that of the C reference
implementation.

Check it out at www.skein-hash.info

There's also a technical paper describing the implementation and
results, available from
the same place.

- Rod Chapman, SPARK Team, Altran Praxis

Peter C. Chapin

unread,
Aug 16, 2010, 7:42:37 AM8/16/10
to
On 2010-08-16 03:37, Rod Chapman wrote:

> Altran Praxis and AdaCore have released SPARKSkein - a new reference
> implementation of Skein-512 written and verified using the SPARK

> language and toolset...

This is great! Thanks for pointing it out.

Peter

Yannick Duchêne (Hibou57)

unread,
Aug 16, 2010, 12:18:02 PM8/16/10
to
Le Mon, 16 Aug 2010 09:37:59 +0200, Rod Chapman
<roderick...@googlemail.com> a écrit:

Was useful:
http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf
says
> [...]
> 4.1.1 Prover says no…a bug is discovered
> The subprogram Skein_512_Final caused someproblems, and led to the
> discovery of a subtle
> corner-case bug.
> [...]

Reply all
Reply to author
Forward
0 new messages