eeh@netbsd.org wrote:

> | > > 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?

Yes, in the worst case it might be hard to prove something about the program.

But, remember that whoever is producing the code is also supposed to
produce the proof, so you might restrict yourself to things that are easily
provable.

The whole idea about proof carrying code is quite beatuiful and actually
practical.  I advice anyone interested to do a web search and read about it.

The first practical application (to my knowledge) was to BPF filter code
which you can load into a running kernel.  The way it's handled now is that
the code you can load is in a small interpreted language with a number of
limitations.  The PCC example instead loaded machine code; after checking
that the proof of safety that came with the code was correct, of course.

    -- Lennart