* ANN: libsparkcrypto
@ 2010-09-08 22:08 Alexander Senier
0 siblings, 0 replies; only message in thread
From: Alexander Senier @ 2010-09-08 22:08 UTC (permalink / raw)
Hello,
I'm happy to announce the first release of libsparkcrypto.
Further information, license and source code is available here:
http://senier.net/libsparkcrypto/
Version 0.1.0 of libsparkcrypto can be downloaded here:
http://senier.net/libsparkcrypto/libsparkcrypto-0.1.0.tgz
libsparkcrypto is a formally verified implementation of several widely
used symmetric cryptographic algorithms using the SPARK programming
language and toolset. For the complete library proofs of the absence of
run-time errors like type range violations, division by zero and
numerical overflows are available. Some of its subprograms include
proofs of partial correctness.
The distribution contains test cases for all implemented algorithms and
a benchmark to compare its performance with the OpenSSL library. The
achieved speed has been found to be very close to the optimized C and
Assembler implementations of OpenSSL.
Have fun!
Regards,
Alex
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2010-09-08 22:08 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-09-08 22:08 ANN: libsparkcrypto Alexander Senier
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox