Date: Fri, 22 May 1998 08:35:59 -0400 (EDT) From: Robert Watson <robert@cyrus.watson.org> To: Pavol Adamec <palo.adamec@tecton.sk> Cc: "freebsd-security@FreeBSD.ORG" <freebsd-security@FreeBSD.ORG> Subject: Re: Virus on FreeBSD Message-ID: <Pine.BSF.3.96.980522082752.11128A-100000@fledge.watson.org> In-Reply-To: <01BD8571.D24221F0@PCNTWS1>
next in thread | previous in thread | raw e-mail | index | archive | help
On Fri, 22 May 1998, Pavol Adamec wrote: > There's something little close to what you mean. There are some research > OS projects dealing with extensible (micro/nano)kernels. Many of them > use some kind of LKM's, varying from SPIN with in-kernel MODULA compiler > to systems based on run-time proving of the correctness of the code > being loaded. I'm very sorry, that I don't remember the the name, but > there is one, that does in-kernel run-time checking of the object code > based on the formal description of the instructions. I've read it in an > ACM's SIGOPS OSR issue somewhere in 1997 or 1996. I don't have them by > the hand at the present, so that's way my answer is so uncertain. Maybe > there's someone who could look for it. There is work going on at the Fox project at CMU (sorry, URL not available just this moment due to DNS problems) with a proof-generating compiler that guarantees memory/type safety -- I believe that the first intended use was providing a replacement for BPF. The compiler generates machine code + a proof of its safety. The kernel then does a linear-order verification of the proof, and can safely use the machine code. Leaving aside issues of Turing computability and undecidability, this is extremely useful :). I know that they are working on bigger and better things there, and that operating systems with built in proof verification might see dramatic performance increases, as the kernel could effectively host a thread for them that "promises" (by way of a verifiable proof) that it will behave correctly (i.e., not touch other people's memory, etc). I believe they do this by a combination of proven pre/post-conditions, and where a proof is not available, run-time checks that are proven to be safe. I believe one could see a dramatic performance improvement in a number of places if memory safety was guaranteed -- even just as simple as guaranteeing that syscall arguements were correcty and did not need to be verified against memory allocation, etc. There are limits to what the proof system can currently do, but it looks remarkably promising (I had given up on proofs for a while there.. :). With regards to other signatures -- I suppose we could have a digital signature on an lkm -- but this isn't all that useful. Suppose a bug is discovered in an lkm in version 2.2.9. In 2.2.9.1, a fix is released. Both are signed by the FreeBSD Project Magic Key. However, unless you do some weird things with versions, the kernel will accept both of the lkms, including the buggy one. To protect the kernel properly, lkms need to be disabled at a sufficiently high run-level (possibly always), and appropriate file system stuff protected. Personally, I like the idea of using a CD-ROM for a file system, but it's not so very fast. Robert N Watson ---- Carnegie Mellon University http://www.cmu.edu/ Trusted Information Systems http://www.tis.com/ SafePort Network Services http://www.safeport.com/ robert@fledge.watson.org http://www.watson.org/~robert/ To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe security" in the body of the message
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?Pine.BSF.3.96.980522082752.11128A-100000>