Re: 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 [EMAIL PROTECTED]

Re: Haskell crypto

[Nathan Loofbourrow]

Haskell is a strongly typed functional language with type inference,
much like ML; its key difference from ML is that is purely functional,
allowing it to use lazy evaluation.

I'm not sure how that illuminates the original message, except to note
that I agree that coding in Haskell is quite fun and addictive.

In addition to traditional crypto conference, he might also consider
submitting to POPL or SIGLANG if the implementation has features unique
to Haskell.

http://en.wikipedia.org/wiki/Haskell_programming_language

nathan


Ian G wrote:

Someone mailed me with this question, anyone know
anything about Haskell?

 Original Message 

I just recently stepped into open source cryptography directly, rather
than just as a user.  I'm writing a SHA-2 library completely in
Haskell, which I recently got a thing for in a bad way.  Seems to me
that nearly all of the message digest implementations out there are
written in C/C++, or maybe Java or in hw as an ASIC, but I can't find
any in a purely functional programming language, let alone in one that
can have properties of programs proved.  Haskell can, and also has a
very good optimizing compiler.  I'm not sure where to submit for
publication when I'm done and have it all written up, though!

-
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to [EMAIL PROTECTED]



-
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to [EMAIL PROTECTED]

Re: Haskell crypto

[Alexander Klimov]

On Sat, 19 Nov 2005, Ian G wrote:

> Someone mailed me with this question, anyone know
> anything about Haskell?

It is a *purely* functional programming language.


>  Original Message 
>
> I just recently stepped into open source cryptography directly, rather
> than just as a user.  I'm writing a SHA-2 library completely in
> Haskell, which I recently got a thing for in a bad way.  Seems to me
> that nearly all of the message digest implementations out there are
> written in C/C++, or maybe Java or in hw as an ASIC, but I can't find
> any in a purely functional programming language, let alone in one that
> can have properties of programs proved.

TTBOMK the main reason why people write low-level crypto in something
other than C is for integration simplification (e.g., there is a lisp
sha1 implementation in the emacs distribution): 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.

BTW, there is low-level crypto in Haskell as well:


-- 
Regards,
ASK

-
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to [EMAIL PROTECTED]