Subject: Re: LKM
To: Hubert Feyrer <hubert.feyrer@informatik.fh-regensburg.de>
From: Lennart Augustsson <lennart@augustsson.net>
List: tech-security
Date: 09/14/2001 21:36:58
Hubert Feyrer wrote:

> [trimmed list of lists this goes to]
>
> On Fri, 14 Sep 2001, Lennart Augustsson wrote:
> > > Is there any mechanisms that verify that the code in "loadable kernel
> > > modules" is safe and does not perform operations compromising system
> > > integrity?
> >
> > 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).

    -- Lennart