[13209] in cryptography@c2.net mail archive
Re: The Pure Crypto Project's Hash Function
daemon@ATHENA.MIT.EDU (Eric Rescorla)
Mon May 5 21:04:26 2003
X-Original-To: cryptography@metzdowd.com
X-Original-To: cryptography@metzdowd.com
To: Bill Frantz <frantz@pwpconsult.com>
Cc: Ralf Senderek <ralf@senderek.de>,
"cryptography@metzdowd.com" <cryptography@metzdowd.com>
Reply-To: EKR <ekr@rtfm.com>
From: Eric Rescorla <ekr@rtfm.com>
Date: 05 May 2003 16:58:57 -0700
In-Reply-To: <v03110709badc9f8bde2c@[192.168.1.5]>
Bill Frantz <frantz@pwpconsult.com> writes:
> At 1:21 PM -0700 5/3/03, Eric Rescorla wrote:
> >Can you explain every single line of the modular exponentiation
> >routine you're using? Every single line of the compiler you're
> >using to compile the code?
>
> The need to show that the object code is a correct implementation of the
> algorithm described by the source code is a general problem for validating
> any kind of code. My approach, and why I have some sympathy for Ralf's
> minimum code approach is:
>
> (1) Code the algorithm in assembler.
>
> (2) Explain each instruction as a comment on the instruction.
>
> (3) Run the code thru the assembler
>
> (4) Show that the output of the assembler matches the input, thereby
> avoiding the need to prove the assembler.
>
> YMMV!
Sure, but this isn't practical for building all but the simplest
applications. In my view, the downsides of having things be
inconvenient in order to make them amenable to this kind of proof far
outweigh the downsides of having usable systems which you cna't prove
to be correct.
-Ekr
--
[Eric Rescorla ekr@rtfm.com]
Web Log: http://www.rtfm.com/movabletype
---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to majordomo@metzdowd.com
