seL4实现了一个capability-based的访问控制模型。每一个用户空间的线程有一个相关联的capability space (CSpace)，这个空间包含了这个线程处理的capabilities，也就是说它管理着这个线程访问的资源。
CNode有一些slot，每个slot需要16字节的物理内存，它可以恰恰保存一个capability。同其他对象一样，CNode必须要通过seL4 Untyped Retype()在合适数量的untyped memory上来创建。
seL4用TCB（thread control block）描述一个线程，每一个TCB对一个CSpace和VSpace（它们可与其他线程共享），一个TCB一般有一个IPC buffer。
seL4提供了消息传递机制用于线程间的通信。
seL4采用256个优先级的抢占式轮转调度机制，当一个线程创建或修改了另一个线程，它只能将另一线程的优先级设为比它低或跟它一样，线程优先级用函数seL4 TCB Configure() 和 seL4 TCB SetPriority() 来设置。