> Is there any mechanisms that verify that the code in "loadable kernel
> modules" is safe and does not perform operations compromising system
> integrity?

As others have said, the answer with respect to NetBSD is basically
"no".

But I would like to point out that this is not just because of laziness
or anything; it's not really fixable.  In its full generality it is a
hard problem (in the halting-problem sense, ie, provably infeasible).
Some subset of it may be doable in principle, but that would first
require a formalized definition of "system integrity", which is very
difficult and ultimately comes down to a matter of opinion.  (To pick a
simple example, would an LKM that could under some circumstances delete
files be capable of "compromising system integrity"?  One could say
yes, if it torches (say) /bin/sh - but then what about unlink(), which
is just as capable of doing the same?)

Furthermore, I suspect that the subset of LKMs that are provably safe
and the subset of LKMs that are useful enough to be worth caring about
overlap little if at all.  (Apropos of which, ISTR seeing mention of a
system that did do such automated proofs of safety - has anyone
actually done anything useful with such?  I'd love to see how to
reconcile utility and safety.)

/~\ The ASCII				der Mouse
\ / Ribbon Campaign
 X  Against HTML	       mouse@rodents.montreal.qc.ca
/ \ Email!	     7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B