Brian A. LaMacchia wrote:
> Seth David Schoen <[EMAIL PROTECTED]> 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 [EMAIL PROTECTED]

Reply via email to