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]