L4.Sec Implementation

[Anton Soppelsa]

Hi Bernhard,

>you should perhaps take a look at Fiasco, which is an L4V2 kernel with the
>focus on real time properties.
>
>  
>
Thx for advice. I  will consider that code when we will look for a new 
os for our board.

>
>
>A capability in L4.sec is a references to a kernel object and permissions
>to use it. Kernel objects are for example threads, endpoints or tasks.
>Permissions are whether it is allowed to send to an endpoint or to modify
>the state of a thread.
>
>  
>
>A capability space is a table of capabilities. These capabilities are
>referenced through task local numbers called capability id's. This is
>very similar to file descriptors in unix.
>  
>

So,a capability is a machine word used like a pointer and another 
machine word used for the permissions or it is just a machine word with 
some of the most significant bits used as permission field? I see now 
that the capability space is a table. (So why don't call it capability 
table?) I think my problem is that some terms clash into my mind. I 
think the address space is and underlying hardware structure that 
permits access to structures in memory.  I was probably misled by the 
name. I can imagine now that address space, capability space and io 
space are all structures from ur point of view. Isn't it? Am I correct 
if I think that MMU control is transparent to the concepts of the three 
spaces?

>If you need some pictures to understand this, have a look at my thesis,
>where I give a short introduction into L4.sec. You can find the thesis
>at http://os.inf.tu-dresden.de/papers_ps/kauer-diplom.pdf
>
>  
>
I already have read ur thesis. But probably I lack some knowledge to 
fully understand it. I'm studying the kernel code of L4 for this reason 
as well.
Many thanks for ur answer,
  Anton