In message <3BA2707C.8E191658@augustsson.net>, Lennart Augustsson writes:
>Hubert Feyrer wrote:
>
>> On Fri, 14 Sep 2001, Lennart Augustsson wrote:
>> > No, it's much more powerful.  With a signed driver you have to trust that
>> > whoever signed it is not lying (volontary or involontary).  With a proof t
>hat
>> > YOU check you only have to trust your own proof checking ability.
>> > There is no need to trust anyone else, so it is strictly more powerful
>> > (and also more difficult to implement).
>>
>> Right, but as far as I understand, doing such a check would mean to
>> analyze the whole (machine) code, automatically, and make some assertion
>> if it's "good" or "bad". Sounds tough. :-)
>
>Well, you have to distinguish between who does the tough work and the
>easy work.  Yes, it might tough work coming up with a proof that the code
>is safe (but with the right code it can be much easier than you might think).
>It's easy work to check that the proof is correct.
>So the user of the code does the easy work, the proof checking.

Right.  More precisely, the user verifies two things:  that the proof 
corresponds to the code, and that the semantics described by the proof 
are acceptable.  

References are George Necula's dissertation and papers, and (much 
earlier, and I wasn't a security guy at the time) my dissertation.

		--Steve Bellovin, http://www.research.att.com/~smb
				  http://www.wilyhacker.com