sel4用户指南：安全可信系统的核心服务与对象

需积分: 10 197 浏览量更新于2024-07-20 收藏 508KB PDF 举报

sel4是一款专注于安全和可靠性的操作系统内核设计，由TrustworthySystems团队在NICTA开发，旨在提供高级别的安全特性，特别是基于能力的访问控制和细粒度资源管理。本文档详细介绍了seL4 v1.3的特性，重点关注其核心概念和功能。 1. **Introduction** (介绍) seL4强调了可信系统的概念，通过严格的最小特权原则和硬件级支持，确保系统的安全性。该文档首先介绍了seL4的背景和目标，以及它在系统安全领域的重要地位。 2. **Kernel Services and Objects** (内核服务和对象) - **Capability-based Access Control** (基于能力的访问控制) seL4采用基于能力的模型，通过分配和撤销特定的安全“票证”（capabilities）来控制对系统资源的访问。这允许系统内核只授权给必要的组件执行特定操作，降低了攻击面。 - **System Calls** (系统调用) 系统调用是进程与内核交互的关键接口，seL4的设计允许高效、安全地执行这些操作，每个系统调用都被设计成原子操作，以防止并发时的数据损坏。 - **Kernel Objects** (内核对象) 内核对象是seL4中用于封装系统资源的抽象，它们代表内存、I/O设备等，通过能力进行管理和控制。 - **Kernel Memory Allocation** (内核内存分配) 内存管理在seL4中尤为重要，包括如何高效地重用内存以及对内存资源的精确控制。 - **Reusing Memory** (内存复用) seL4支持内存的动态分配和回收，以提高资源利用率，同时保持数据的一致性和安全性。 3. **Capability Spaces** (能力空间) - **Capability and CSpace Management** (能力与C空间管理) CSpace是seL4中的一个关键概念，用于表示和组织能力。CNode方法允许对能力和C空间进行创建、删除和管理，确保权限的准确传递和控制。 - **CNode Methods** (C节点方法) 包括创建新的CNode、关联和拆分CNode等操作，这些方法支持复杂的能力架构。 - **Capability Rights** (能力权利) 每个能力都有特定的权利和限制，比如读取、写入或执行，这些权利在CNode和C空间层次结构中被严格定义。 - **Capability Derivation Tree** (能力派生树) 通过能力派生树，seL4维护了能力的来源和权限层次，确保所有操作符合最小特权原则。 4. **Delimiters and Acknowledgements** (分隔符与致谢) 文档最后提供了作者列表和版权信息，展示了seL4开发团队的贡献，强调了团队成员在设计和实现这个高度安全内核系统中的角色。这篇seL4用户文档深入探讨了这个安全内核的核心机制，包括其访问控制、内存管理和能力空间管理，为理解和使用这一先进内核提供了详尽的指南。对于研究安全操作系统或者希望深入了解sel4技术的开发者来说，这是一个不可或缺的参考资料。

4 CHAPTER 2. KERNEL SERVICES AND OBJECTS

seL4 NBSend() performs a non-blocking send. It is similar to seL4 Send() except that

if the message cannot be received immediately, the message is silently dropped.

Like seL4 Send(), no error code or response will be returned by the object.

seL4 Call() is a seL4 Send() that blocks the sending thread until a reply message is

received. When the sent message is delivered to another thread (via an Endpoint),

an additional ‘reply’ capability is added to the message and delivered to the

receiver to give it the right to reply to the sender. The reply capability is stored

in a special purpose slot in the receiver’s TCB. When invoking capabilities to

kernel services, using seL4 Call() allows the kernel to return an error code or

other response within a reply message.

seL4 Wait() is used by a thread to receive messages through endpoints. If no message

is ready to be sent, the thread will block until a message is sent. This system

call works only on endpoint capabilities, raising a fault (see section 5.2) when

attempted with other capability types.

seL4 Reply() is used to respond to a seL4 Call(), using the capability generated by

the seL4 Call() system call and stored in the replying thread’s TCB. It delivers

the message to the calling thread, waking it in the process.

There is space for only one reply capability in each thread’s TCB, so the seL4 -

Reply() syscall can be used to reply to the most recent caller only. The seL4 -

CNode SaveCaller() method that will be described later can be used to save

the reply capability into regular capability space, where it can be used with

seL4 Send().

seL4 ReplyWait() is a combination of seL4 Reply() and seL4 Wait(). It exists for

eﬃciency reasons: the common case of replying to a request and waiting for the

next can be performed in a single kernel system call instead of two.

seL4 Poll() is used by a thread to check for messages waiting to be sent through

an endpoint without blocking on that endpoint. This system call works only

on asynchronous endpoint capabilities, raising a fault (see section 5.2) when

attempted with other capability types.

seL4 Yield() is the only system call that does not require a capability to be used.

It causes the calling thread to give up the remainder of its timeslice to another

runnable thread of the same priority level. If there are no runnable threads with

the same priority, the calling thread is resumed and the system call has no eﬀect.

2.3 Kernel Objects

In this section we give a brief overview of the kernel-implemented object types whose

instances (also simply called objects) can be invoked by applications. The interface

to these objects forms the interface to the kernel itself. The creation and use of the

high-level kernel services is achieved by the creation, manipulation, and combination

of these kernel objects:

2.4. KERNEL MEMORY ALLOCATION 5

CNodes (see Chapter 3) store capabilities, giving threads permission to invoke methods

on particular objects. Each CNode has a ﬁxed number of slots, always a power

of two, determined when the CNode is created. Slots can be empty or contain a

capability.

Thread Control Blocks (TCBs; see Chapter 5) represent a thread of execution in

seL4. Threads are the unit of execution that is scheduled, blocked, unblocked,

etc., depending on the application’s interaction with other threads.

IPC Endpoints (see Chapter 4) may be used to facilitate interprocess communica-

tion between threads. The seL4 microkernel supports two types of endpoints:

• Synchronous endpoints (Endpoint), which cause the sending thread to block

until its message is received; and

• Asynchronous endpoints (AsyncEP), which only allow short messages to be

sent, but do not cause the sender to block.

A capability to an endpoint can be restricted to be send-only or receive-only. Ad-

ditionally, capabilities to Endpoint objects may be conﬁgured to allow capabilities

to be transferred across to other threads.

Virtual Address Space Objects (see Chapter 6) are used to construct a virtual

address space (or VSpace) for one or more threads. These objects largely directly

correspond to those of the hardware; that is, a page directory pointing to page

tables, which in turn map physical frames. The kernel also includes ASID Pool

and ASID Control objects for tracking the status of address spaces.

Interrupt Objects (see Chapter 7) give applications the ability to receive and ac-

knowledge interrupts from hardware devices. Initially, there is a capability to

IRQControl, which allows for the creation of IRQHandler capabilities. An IRQHandler

capability permits the management of a speciﬁc interrupt source associated with

a speciﬁc device. It is delegated to a device driver to access an interrupt source.

The IRQHandler object allows threads to wait for and acknowledge individual

interrupts.

Untyped Memory (see Section 2.4) is the foundation of memory allocation in the

seL4 kernel. Untyped memory capabilities have a single method which allows

the creation of new kernel objects. If the method succeeds, the calling thread

gains access to capabilities to the newly-created objects. Additionally, untyped

memory objects can be divided into a group of smaller untyped memory objects

allowing delegation of part (or all) of the system’s memory. We discuss memory

management in general in the following sections.

2.4 Kernel Memory Allocation

The seL4 microkernel does not dynamically allocate memory for kernel objects. Ker-

nel objects must be explicitly created from application-controlled memory regions via

Untyped Memory capabilities. Applications must have explicit authority to memory

(through these Untyped Memory capabilities) in order to create new objects, and all

6 CHAPTER 2. KERNEL SERVICES AND OBJECTS

objects consume constant memory once created. These mechanisms can be used to

precisely control the speciﬁc amount of physical memory available to applications, in-

cluding being able to enforce isolation of physical memory access between applications

or a device. There are no arbitrary resource limits in the kernel apart from those dic-

tated by the hardware

, and so many denial-of-service attacks via resource exhaustion

are avoided.

At boot time, seL4 pre-allocates the memory required for the kernel itself, including

the code, data, and stack sections (seL4 is a single kernel-stack operating system). The

remainder of the memory is given to the initial thread in the form of capabilities to

Untyped Memory, and some additional capabilities to kernel objects that were required

to bootstrap the initial thread. These Untyped Memory regions can then be split into

smaller regions or other kernel objects using the seL4 Untyped Retype() method; the

created objects are termed children of the original untyped memory object.

The user-level application that creates an object using seL4 Untyped Retype() re-

ceives full authority over the resulting object. It can then delegate all or part of the

authority it possesses over this object to one or more of its clients.

2.4.1 Reusing Memory

The model described thus far is suﬃcient for applications to allocate kernel objects,

distribute authority among client applications, and obtain various kernel services pro-

vided by these objects. This alone is suﬃcient for a simple static system conﬁguration.

The seL4 kernel also allows Untyped Memory regions to be reused. Reusing a region

of memory is allowed only when there are no dangling references (i.e., capabilities)

left to the objects inside that memory. The kernel tracks capability derivations, i.e.,

the children generated by the methods seL4 Untyped Retype(), seL4 CNode Mint(),

seL4 CNode Copy(), and seL4 CNode Mutate().

The tree structure so generated is termed the capability derivation tree (CDT).

For

example, when a user creates new kernel objects by retyping untyped memory, the

newly created capabilities would be inserted into the CDT as children of the untyped

memory capability.

For each Untyped Memory region, the kernel keeps a watermark recording how much of

region has previously been allocated. Whenever a user requests the kernel to create

new objects in an untyped memory region, the kernel will carry out one of two actions:

if there are already existing objects allocated in the region, the kernel will allocate

the new objects at the current watermark level, and increase the watermark. If all

objects previously allocated in the region have been deleted, the kernel will reset the

watermark and start allocating new objects from the beginning of the region again.

Finally, the seL4 CNode Revoke() method provided by CNode objects destroys all ca-

pabilities derived from the argument capability. Revoking the last capability to a

kernel object triggers the destroy operation on the now unreferenced object. This

The treatment of virtual ASIDs imposes a ﬁxed number of address spaces. This limitation is to

be removed in future versions of seL4.

Although the CDT conceptually is a separate data structure, it is implemented as part of the

CNode object and so requires no additional kernel meta-data.

剩余93页未读，继续阅读

yu.sang

粉丝: 11
资源: 11

sel4用户指南：安全可信系统的核心服务与对象

seL4 操作系统编程手册 （中文版）

sel4源码解析（一） – sel4内核对象

Unix sel4 微内核源码

linux 环境配置sel4

sel4 cpu schedule policy free

error = seL4_X86_PageDirectory_Map(pd, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes); assert(error == seL4_NoError);代码解释

java的sel4j

OPTEE/trusty/seL4

解释代码dis_sel <= {dis_sel[4:0],dis_sel[5]};

cs_dig <= ch_dig[cs_sel[4:0]] ; sclk_dig <= ch_dig[sclk_sel[4:0]] ; mosi_dig <= ch_dig[mosi_sel[4:0]] ; miso_dig <= ch_dig[miso_sel[4:0]] ; 在SPI中怎么理解

最新资源

seL4 操作系统编程手册（中文版）