Capability based L4
voelp at os.inf.tu-dresden.de
Mon Oct 8 09:38:58 CEST 2007
Luke A. Guest wrote:
> I'm interested in seeing how capabilities work in a real OS kernel and
> was wondering if there is any source or documents available that I could
> read? Preferably not the Haskell stuff as I just don't get it :(
In previous L4 Kernels you addressed a kernel object by some name (e.g.,
a thread ID) with global validity. In addition you had some permissions
on this kernel object (e.g., exchange_registers only if the thread was
in the same task).
The main difference with capabilities is now that you have a name which
is valid only inside your address space (like previously the virtual
address of a page). At this name the kernel stores a tuple which
consists of the permissions (e.g., read, write) and a reference on the
physical kernel object (e.g., the physical page). This is the capability.
Now everything works like before except that all kernel objects now
behave like virtual memory: capabilities can be mapped / unmapped; any
operation on the kernel object (e.g., read page / write page) requires
the capability as an argument, etc.
The issue within the kernel is now to implement something similar to a
page-table to translate local names to the respective capability. It is
similar to a page-table because a page-table entry is in fact a capability.
> Is there an implementation of L4.sec?
Sorry, no publicly available implementation.
> The spec seems like it's missing
> stuff, is there an update anywhere?
No, what's missing? An ABI you may find in Bernhard Kauer's diploma thesis:
Technische Universität Dresden
Department of Computer Science
Institute for System Architecture
Tel: +49 (351) 463 38350
Fax: +49 (351) 463 38284
Email: voelp at os.inf.tu-dresden.de
More information about the l4-hackers