dangers of TCPA/palladium
Jeff Cours
cpunk-j at moriarti.org
Wed Aug 14 13:22:11 EDT 2002
Brian A. LaMacchia wrote:
> Seth David Schoen <schoen at loyalty.org> wrote:
>>R. Hirschfeld writes:
>>>
>>>This may be a silly question, but how do you know that the source
>>>code provided really describes the binary?
>>>
>>>It seems too much to hope for that if you compile the source code
>>>then the hash of the resulting binary will be the same, as the
>>>binary would seem to depend somewhat on the compiler and the
>>>hardware you compile on.
>>
>>I heard a suggestion that Microsoft could develop (for this purpose)
>>a provably-correct minimal compiler which always produced identical
>>output for any given input.
>
> We are talking internally about doing exact what is suggested here.
Apologies for what is almost certainly a newbie question, but I've
been thinking about this issue for a few days, and I'm not sure I
understand the idea of a provably correct compiler in this context.
Is it sufficient for the compiler to be simple enough to audit and to
always produce the same binary when given the same source code, say
something along the lines of the Small C compiler?
<http://www.ddjembedded.com/languages/smallc/book/chaps/toc1.htm>
Is something stronger required, where each piece of code in the
compiler includes assertions about its input and output, and it's
possible to construct a formal proof leading from one to the other,
and to link the individual assertions together into a full formal
proof of correctness? How would one go about building something like
that? I think I could see how to write the correctness proofs at the
fairly simple level of turning intermediate code into op-codes, but
I'm having some trouble with how to scale up to higher level language
constructs while still keeping the proof more abstract than the code
it's trying to prove.
Finally, would there need to be restrictions on what the compiler
could accept for input or output, or would a general purpose compiler
do? I'm guessing that restrictions on the output the compiler could
produce, like not linking to external libraries, are not necessary to
help with proving the security of the final product, but I'm not sure.
thanks in advance,
Jeff
---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to majordomo at wasabisystems.com
More information about the cryptography
mailing list