From: Alexander Senier <mail@senier.net>
Subject: ANN: libsparkcrypto
Date: Thu, 9 Sep 2010 00:08:53 +0200
Date: 2010-09-09T00:08:53+02:00 [thread overview]
Message-ID: <20100909000853.5ac18f5e@t60> (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
reply other threads:[~2010-09-08 22:08 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox