Capability based L4

[Marcus Voelp]

Luke A. Guest wrote:
> Hi,
>
> 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:

http://os.inf.tu-dresden.de/L4/L4.Sec/

Regards

    Marcus

-- 
Marcus Völp

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
Web: http://os.inf.tu-dresden.de/~voelp