sel4源码解析（二） - CSpace

Sel4采用基于capability的访问控制模型，进程对系统资源的访问控制权限组成一个capability space，所有的cap存放在CNode里。CSpace是由CNode构成，CNode可以看成一个数组，数组元素称为slot，每一个slot里面可以存放一个cap或者为空。
Sel4提供CDT(capability derive tree)结构保存权能的拷贝、

CNode

CNodes本质是一个结构体数组，该数组的元素是cte（capability table entry），cte中包含一个cap_t结构体和mdb_node_t结构体。CNodes的cte称为slot，下面是slot的结构体：

• cap：包含权限和指向具体cap的指针；
• cteMDBNode：保存cap之间的关系，比如：untyped cap衍生出的其它对象的cap。

struct cte {
    cap_t cap;
    mdb_node_t cteMDBNode;
};

CNodes本身是一个内核对象，也有相应的cap。下面是CNode cap的结构体：

• capCNodeGuard：具体的guard数值；
• capCNodeGuardSize：guard占的位数；
• capCNodeRadix：CNode的最大slot个数；
• capCNodePtr：指向CNode的指针；

block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard, capCNodePtr, capType) {
    field capCNodeGuard 64
    field capType 5
    field capCNodeGuardSize 6
    field capCNodeRadix 6				
    field_high capCNodePtr 47
}

capability

capability的结构体的大小是16字节，它包含两部分，一部分是seL4_CapRights，另一部分是指向具体对象cap的指针。下面是cap的结构体和seL4_CapRights结构体：

struct cap {
    uint64_t words[2];
};

block seL4_CapRights {
    padding 32
    padding 28
    field capAllowGrantReply 1
    field capAllowGrant 1
    field capAllowRead 1
    field capAllowWrite 1
}

sel4定义了如下几类cap（不同的架构可能会不同，本例是arm32架构）：

enum cap_tag {
    cap_null_cap = 0,
    cap_untyped_cap = 2,
    cap_endpoint_cap = 4,
    cap_notification_cap = 6,
    cap_reply_cap = 8,
    cap_cnode_cap = 10,
    cap_thread_cap = 12,
    cap_small_frame_cap = 1,
    cap_frame_cap = 3,
    cap_asid_pool_cap = 5,
    cap_page_table_cap = 7,
    cap_page_directory_cap = 9,
    cap_asid_control_cap = 11,
    cap_irq_control_cap = 14,
    cap_irq_handler_cap = 30,
    cap_zombie_cap = 46,
    cap_domain_cap = 62
};

从上面可以看出每一类cap里面具体包含了一些私有的访问控制规则，以endpoint为例：endpoint cap里面包含了四项权限，分别是：capCanGrantReply（）、capCanGrant（）、capCanReceive（该endpoint能否接受消息）、capCanSend（该endpoint能否发送消息）。

同时cap_t也包含三个通用的规则，分别是 capAllowGrantReply、capAllowGrant、capAllowRead和capAllowWrite。

下面是endpoint cap结构体：

block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend,
                   capCanReceive, capEPPtr, capType) {
    field capEPBadge 64
    field capType 5
    field capCanGrantReply 1
    field capCanGrant 1
    field capCanReceive 1
    field capCanSend 1
    padding 7
    field_high capEPPtr 48
}

用户程序API

seL4_CNode_Copy
seL4_CNode_Delete
seL4_CNode_Mint
seL4_CNode_Move
seL4_CNode_Mutate
seL4_CNode_Revoke
seL4_CNode_Rotate
seL4_CNode_SaveCaller

以seL4_CNode_Mint为例，该函数的参数有：

• seL4_CNode _service：新的cap所在的CNode；
• seL4_Word dest_index：新的cap在CNode的偏移；
• seL4_Uint8 dest_depth：新的cap在CNode中查找过程中guardbits和radixbits之和；
• seL4_CNode src_root：原cap所在的CNode；
• seL4_Word src_index：原cap在CNode的偏移；
• seL4_Uint8 src_depth：原新的cap在CNode中查找过程中guardbits和radixbits之和；
• seL4_CapRights_t rights：新的cap的权限；
• seL4_Word badge：新的cap的标识符；

seL4_CNode_Mint函数具体工作流程如下：

1. 通过系统调用执行到decodeCNodeInvocation函数，该函数的具体功能如下：
   a. 从ipc buffer里面取出上述的参数信息；
   b. 通过_service、dest_index、dest_depth参数可以找到目的slot；
   c. 通过src_root、src_index、src_depth参数可以找到源slot；
   d. 通过rights和源slot参数，调用maskCapRights函数，得到带有新的rights的cap；
   e. 更新cap的badge信息；
   f. 根据label调用invokeCNodeInsert函数。
2. invokeCNodeInsert函数调用cteInsert函数将新cap插入到目的slot中；
3. 完成。

Capability查找流程

resolveAddressBits根据CNode（nodeCap）、index（capptr）和depth（n_bits）找到slot。具体流程如下：

1. 从CNode cap取出radixBits和guardBits，将它们相加得到当前级别的CNode的比特数（比如一级的CNode对应的radixBits是12）；
2. 从capptr取出guardBits对应的guard，同CNode的guard作比较；
3. 从capptr取出cap在CNode中的偏移量；
4. 找到对应的slot，判断该slot中的cap是否位CNode，如果是则到第一步，否则进入第五步；
5. 完成；

index和n_bits位数是一致的。

resolveAddressBits_ret_t resolveAddressBits(cap_t nodeCap, cptr_t capptr, word_t n_bits)
{
	......
    while (1) {
        radixBits = cap_cnode_cap_get_capCNodeRadix(nodeCap);
        guardBits = cap_cnode_cap_get_capCNodeGuardSize(nodeCap);
        levelBits = radixBits + guardBits;
        capGuard = cap_cnode_cap_get_capCNodeGuard(nodeCap);
        guard = (capptr >> ((n_bits - guardBits) & MASK(wordRadix))) & MASK(guardBits);
        if (unlikely(guardBits > n_bits || guard != capGuard)) {
            current_lookup_fault =
                lookup_fault_guard_mismatch_new(capGuard, n_bits, guardBits);
            ret.status = EXCEPTION_LOOKUP_FAULT;
            return ret;
        }

        if (unlikely(levelBits > n_bits)) {
            current_lookup_fault =
                lookup_fault_depth_mismatch_new(levelBits, n_bits);
            ret.status = EXCEPTION_LOOKUP_FAULT;
            return ret;
        }

        offset = (capptr >> (n_bits - levelBits)) & MASK(radixBits);
        slot = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)) + offset;

        if (likely(n_bits <= levelBits)) {
            ret.status = EXCEPTION_NONE;
            ret.slot = slot;
            ret.bitsRemaining = 0;
            return ret;
        }

        /** GHOSTUPD: "(\<acute>levelBits > 0, id)" */

        n_bits -= levelBits;
        nodeCap = slot->cap;

        if (unlikely(cap_get_capType(nodeCap) != cap_cnode_cap)) {
            ret.status = EXCEPTION_NONE;
            ret.slot = slot;
            ret.bitsRemaining = n_bits;
            return ret;
        }
    }

    ret.status = EXCEPTION_NONE;
    return ret;
}

Capability derive tree

sel4提供cdt来保存cap的变化过程，其本质是一个双向链表。比如：在删除某一个cap时，如果有其他的cap是通过该cap mint创建的，则也需要删除。

//mapping database
block mdb_node {
    padding 16
    field_high mdbNext 46
    field mdbRevocable 1
    field mdbFirstBadged 1
    field mdbPrev 64
}

相关阅读

sel4源码解析（一） - sel4内核对象
sel4源码解析（二） - CSpace
sel4源码解析（三） - sel4系统调用处理流程
sel4源码解析（四） - ipc
sel4源码解析（五） - Notification
sel4源码解析（六） - 进程
sel4源码解析（七） - vspace