| > > Yes, but none of these are available in NetBSD (or any other wide spread
| > > OS, AFAIK).  One such technique is called proof carrying code.  Each piece
| > > of code loaded into the kernel is accompanied by a (formal) proof that it
| > > does no damage.  Before loading the code the proof+code is run through
| > > a proof checker.
| >
| > Isn't that similar to the "driver signing" WinXP does?
|
| 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 that
| 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).

How do you verify that the machine code actually does what the proof code 
associated with it asserts?  Doesn't that directly map to the halting problem?

Eduardo