Subject: Re: LKM
To: =?iso-8859-1?Q?P=E5l?= Halvorsen <paalh@unik.no>
From: Lennart Augustsson <lennart@augustsson.net>
List: tech-security
Date: 09/14/2001 18:55:28
Pål Halvorsen wrote:

> Hi!
>
> 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.

    -- Lennart