[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: File Share and Sandbox project
From: |
Farid Hajji |
Subject: |
Re: File Share and Sandbox project |
Date: |
Sun, 6 Oct 2002 14:17:19 +0200 (CEST) |
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 | farid.hajji@ob.kamp.net
- - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - -
Due to budget cuts, light at end of tunnel will be out. --Unknown.