Haskell crypto

[Travis H.]

> IMO it is pointless to
> write SHA in a language that ``can have properties of programs
> proved,'' because test vectors are good enough, and there is no real
> assurance that when you write the specification in a machine-readable
> form you do not make the same mistake as in your code.

I think you can prove things about many languages, it just may not be
easy for an arbitrary program in that language.  If you write code
with proof in mind, it probably can work with any language.  If you
don't, and the language is modestly powerful, then you may end up with
the halting problem.

For example, see:
http://raw.cs.berkeley.edu/pcc.html
http://www.cs.princeton.edu/sip/projects/pcc/

It looks like the java bytecode verifier is an example of proving
something about a non-functional language, and they have examples of
checking the safety of hand-coded assembly language.

Even if the proof or specification can be wrong, writing it a
different way may catch some implementation errors.  If the
specification is more terse than the code, then there may be fewer
places to get it wrong, in the same way that handling strings as first
class objects avoids many buffer overflow situations.

None of this will help if the programmer misunderstands the algorithm,
of course.  Test vectors would probably help on that front.

Once I was implementing some crypto, and the AES module was failing
some test vectors, but it worked anyway.  I was told to not worry
about it, but I did.  Later after perusing the code I found that the
author was copying an array of characters to an array of integers,
reducing the keyspace from 128 bits to 32 bits, with 3/4 of the key
being zeroes.

In general testing isn't really a replacement for proof.  It seems
like it would be useful for finding problems in code branches that
aren't taken frequently and thus might be missed by test vectors.  I'm
not sure how many ciphers have this characteristic, I think Schneier
mentioned that IDEA does, among others.
--
http://www.lightconsulting.com/~travis/  -><-
"We already have enough fast, insecure systems." -- Schneier & Ferguson
GPG fingerprint: 50A1 15C5 A9DE 23B9 ED98 C93E 38E9 204A 94C2 641B

---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to majordomo at metzdowd.com