Hi David, > I am developing a thesis topic using the GNU/Hurd OS as the > implementation platform. the topic is very interesting from a theoretical, but also from a practical point of view.
> 2. The GNU/Hurd OS is a _better_ mouse trap. There are security > solutions which are cleaner to implement using it. Where by cleaner, I > mean that there is substantial motivation to code/utility reuse. please elaborate more on this. Just because some stuff runs in user space (e.g. network translator) doesn't necessarily mean that it is more secure for the whole system. One example: If a user application that uses sockets has a security flaw, attackers could get at it via pfinet (Hurd) or the traditional kernel-based IP implementation. Traditional systems have security mechanisms as well, like e.g. chroot(2), jail(8) etc... So the only _obvious_ advantage of the Hurd w.r.t. security would be to reduce the compromise of kernel bugs. Hmmm..., doesn't this apply to _every_ microkernel-based design? In what respect would the Hurd be different here? > 3. Verifiability: The GNU/Hurd OS's security can be verified more > easily than traditional monolithic kernels because of the use of > translators and a micro kernels and the reduction of sharing of kernel > memory. > > One of the problems with monolithic kernels and verifiability is that > the address space of the kernel includes many of the devices and > shared data structures used by the kernel to share information with > the drivers. > > This leads to potential side effects which are difficult to find, as > unrelated sections of the kernel can affect / modify other unrelated > locations. > > Loadable modules share these same problems. > > GNU/Hurd has the potential to reduce these problems through separation > of drivers from the kernel as well as ability to compartmentalize > functionality that traditionally would have been a kernel component. Not so sure. In microkernel-based systems, you must still share data structures between the microkernel, the (userland?) drivers and the applications that use them. Just because the boundaries now cross address spaces doesn't mean that verification is easier. [at least, it would depend on a lot of implementation factors] Consider the scenario of a userland device driver (as of today, we still don't have that in gnumach; but we'll need it in Hurd/L4). That driver will communicate with the kernel via IPC for notifications _and_ probably through mapped [I/O] pages to access physical devices. If you want to mathematically verify the driver, you'll need to prove that the IPC protocols (not the messages alone, but the whole protocol state diagram) are correct. Moreover, you'll need to verify that the microkernel doesn't interfere with the mapped pages [the driver would be the sole user of them; which is realistic]. You also need to prove that memory management w.r.t. the shared pages doesn't get in the way, that scheduling issues won't interfere with the driver task's operation (they always do), etc... Because the drivers now run asynchroneously, you open up a whole new class of issues that are extremly hard to deal with, at least as far as formal verification is concerned. You also need to verify the protocol and the data flow between the driver and users of that driver (e.g. translators), possibly in a multithreaded context. For example: you (still) need to make sure that pages shared between the driver and the userapp are not reclaimed by the VM subsystem (e.g. while DMA with mapped userland receiver buffer is in progress...). The same situation arises in monolithic kernels, but becomes much more difficult to prove correct in kernelized architectures. Of course you're right that monolithic drivers can corrupt the whole address space of their hosting kernel, whereas user space drivers would not. But verifying the correctness of a driver implementation, even for the most simple driver that controls a physical device, would still remain a formidable task. I have seen a verification of a pseudo-device (a loopback interface) and _that_ was approx. 60 DIN-A4 pages densely written. And that was the easiest case ;-) To summarize: you trade off one issue (separation of address spaces) for a whole lot of other issues (scheduling/timing, handshaking, ...), which are probably harder to formally verify. > II. User Configurable File Share Translator > > While looking at the problem of file sharing in user space, the > administration problems have been traditionally a poison pill in the > ubiquitous adoption of file sharing in secure environments. > > The work that an administrator has to do in a traditional *nix (POSIX) > environment requires the maintenance of users and groups, and the > granularity of access control is limited to the compositions of users > in groups. A user belonging to a group has access privileges You should read the papers of the L4 people who had to struggle with exactly the same kind of authorization and authentication issues. They developed L4 with security in mind and are still refining their security model, even redoing it from scratch in some parts (they dropped the clans and chiefs model for instance). > Goal one: enable simple user configurable file sharing with > granularity, in a user space implementation. Yes, "fileshare" is indeed a very good example. > III. Process Rights Management: Sample application: Confined Email > > Goal two: Implement a secure 'virtual sandbox' for potentially rogue > processes whose authenticity or unverifiability make them a threat to > the user. What would be the fundamental difference between traditional chroot(2) or jail(8) environments and this scenario? Basically, they're the same, aren't they? > V. Related discussions. > > If I have overlooked places where there is or was prior ideas that you > are aware of, I will appreciate being made aware of them. Is the discussion taking place offline or on #hurd? I didn't see anything on bug-hurd as yet. > Time line: My goal is to complete a workable version of the first run > of this translator prior to Jan 1 2003. Good luck! -Farid. -- Farid Hajji -- Unix Systems and Network Admin | Phone: +49-2131-67-555 Broicherdorfstr. 83, D-41564 Kaarst, Germany | [EMAIL PROTECTED] - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - Due to budget cuts, light at end of tunnel will be out. --Unknown. _______________________________________________ Bug-hurd mailing list [EMAIL PROTECTED] http://mail.gnu.org/mailman/listinfo/bug-hurd
