Re: File Share and Sandbox project

[Farid Hajji]

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.