# seL4-Programing-Guide-book

**Repository Path**: tjopenlab/seL4-Programing-Guide-book

## Basic Information

- **Project Name**: seL4-Programing-Guide-book
- **Description**: seL4操作系统编程
- **Primary Language**: Unknown
- **License**: Apache-2.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 12
- **Forks**: 3
- **Created**: 2021-01-04
- **Last Updated**: 2025-05-30

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# seL4-Programing-Guide-book

这个仓库是《seL4操作系统编程》一书的素材和成稿。



seL4是一个操作系统微内核，也就是说，seL4本身不是一个完整的操作系统。因为它是微内核，所以它提供很有限的API，没有提供象传统的操作系统Linux那样的内存管理、页内外交换、驱动程序等等。

seL4是一组基于微内核架构的操作系统内核，澳大利亚研究组织NICTA http://nicta.com.au/ 创造了一个新的L4版本，称为Secure Embedded L4（简写为seL4），宣布在世界上率先开发出第一个正规机器检测证明（formal machine-checked proof）通用操作系统。

seL4微内核设计针对实时应用，可潜在应用于强调安全和关键性任务的领域内，如军用和医疗行业。形式证明在较小的内核中已经实现，但这次是首次在执行复杂任务的操作系统内核中实现。研究发现常用的攻击方法对seL4无效，如恶意程序经常采用的缓存溢出漏洞。

seL4是第三代微内核操作系统，它基本是可以说是基于L4的，它提供了虚拟地址空间（virtual address spaces）、线程（threads）、IPC（inter-process communication）

受EROS、KeyKOS、CAP等操作系统设计的影响，seL4的控制机制是基于capabilities的, capabilities机制提供了访问内核对象（kernel objects）的方法，这种机制使得seL4与其它L4比起来，显示出一定的高效率。