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