seL4 Level-1 Tutorials - Exercise #2: Capabilities

Objectives

Understand CSpace, CNode and capability pointers.
Copy, move, delete capabilities.
Perform operations on capabilities.

Background

Capabilities are the building blocks in seL4. Everything works through capabilities. A capability is a pointer to a kernel object. Capabilities provide fine-grained access control to these objects. They provide a high degree of isolation and privilege-based access control. Capabilities reside in CSpace, which is a capability space. The rootserver program gets its CSpace from the kernel after dropping into a usermode execution environment. From there, other CSpaces can be created within to contain different types of capabilities.

The model ensures that no child capability in an inheritance chain could ever have more privileges than its parent. The most it gets is as many privileges as the parent but never more. 

There are many different types of operations done on capabilities. The basics include: copy, move, mint, ..., etc. 

Disclaimer: this exercise was directly ported from seL4 capabilities tutorial. 

Steps

Initialize build environment:

          The output should be:

    2.  Copy a capability. In application/core/exercise-2/src/main.c, find “TODO #1”, make a copy of the seL4_CapInitThreadTCB capability, and put it into the last available slot (last_slot). The copy function is: 

seL4_CNode_Copy(seL4_CNode dest_cspace_root,
                                     seL4_Word dest_index, seL4_Uint8 dest_depth,
                                     seL4_CNode src_cspace_root,
                                     seL4_Word src_index, seL4 Uint8 src_depth,
                                     seL4_CapRights_t copied_rights);

- dest_cspace_root:      the destination cspace pointer. This is a CNode that points to the first capability in the destination cspace.
- dest_index:                   how many "slots" to count from dest_cspace_root to reach the exact place in the destination cspace where we want the capability to be copied.
- dest_depth:                  how many bits per capability pointer are needed . This works with index to find the exact destination pointer.
- src_cspace_root:        similar to dest_cspace_root, but for the source capability
- src_index:                     same as dest_index, but for the source capability
- src_depth:                    same as dest_depth, but for the source capability
- copied_rights:             a word specifying the privileges of the newly created capability by the copy function.

        Recompile and simulate. The output should be: 

    3.  Now delete a capability (find “TODO #2” in main.c). It can be done using delete or revoke. If you choose to use seL4_CNode_Delete, you will need to manually delete every node that was copied (first_free_slot and last_slot). If you choose to use seL4_CNode_Revoke, you can call it once on the node that was copied (seL4_CapInitThreadTCB) and all copies will be deleted, while the original capability will not be altered.

seL4_CNode_Delete(seL4_CPtr cnode_root, seL4_CPtr index, seL4_Word depth)

- cnode_root:        initial node in the cspace to delete from.
- index:                   offset from cnode_root to find the node to delete (pointer to the node you want deleted)
- depth:                  size bits of each capability pointer along the way
                                                        ---- OR ----
seL4_CNode_Revoke(seL4_CPtr cnode_root, seL4_CPtr index, seL4_Word depth)

- cnode_root:        initial node in the cspace to delete from.
- index:                   offset from cnode_root to find the node whose copies are to be deleted (the original one)
- depth:                  size bits of each capability pointer along the way

        Recompile and simulate. The output should be: 

   4.  Suspend main thread TCB capability (find “TODO #3” in main.c): The default behavior of seL4 runtime is to let the developer determine how the program terminates. If you just return zero, the kernel attempts to call a destructor that was never set which will cause the program to crash. Therefore, we can suspend the main thread and never return 0:

        Recompile and simulate. The output should be: 

Instead of forcing thread suspension in every rootserver program, we included the functionality in the 'common' library which is linked into every exercise. 

Learned APIs

seL4_CNode_Copy
seL4_CNode_Delete
seL4_CNode_Revoke
seL4_CNode_Move
seL4_TCB_Suspend

⟵ Exercise-1

table of contents

Exercise-3 ⟶