seL4操作系统基础01：seL4 whitepaper概览
目录
Chapter 1：What Is SeL4
Chapter 2：SeL4 Is a Microkernel and Hypervisor, It Is Not an OS
2.1 微内核结构
2.1.1 TCB（Trusted Computing Base）的概念
2.1.2 微内核提供的机制
2.1.3 seL4的"IPC"
2.1.4 How to (and how not to) use seL4 IPC
2.1.5 seL4提供服务的方式
2.1.6 component framework
2.2 seL4作为hypervisor
2.2.1 借用Guest Linux的网络设备驱动
2.2.2 借用Guest Linux的文件系统
Chapter 3：seL4's Verification Story
3.1 CAmkES抽象视图
3.2 CAmkES如何参与构建系统
Chapter 4：About Capabilities
Chapter 5：Support for Hard Real-Time Systems
Chapter 6：Security is No Excuse for Poor Performance
Chapter 7：Real-World Deployment and Incremental Cyber Retrofit
说明：seL4 whitepaper对seL4操作系统进行了概要性介绍，本概览是阅读该文档时的总结与扩展，但是只涉及框架和与本人使用相关的内容
链接：https://sel4.systems/About/seL4-whitepaper.pdf
Chapter 1：What Is SeL4
1. seL4是一个操作系统微内核，仅包括操作系统核心部分的最小集合
2. seL4也是一个hypervisor，可以在其上运行完整的Linux Guest OS。通过seL4的通信机制（IPC），Guest OS可以与native application通信
3. seL4通过capability（能力）机制提供细粒度的访问控制。capability可以理解为一种access token，用于控制对特定资源的访问权限
说明：seL4支持Linux Guest OS，且支持Guest OS与native application通信，在很大程度上是因为seL4作为一个极其精简的微内核，几乎没有提供系统服务。除了引入开源或已开发的lib，借用Guest Linux OS中的服务，是一种简单快捷的方式（后文会提及）
Chapter 2：SeL4 Is a Microkernel and Hypervisor, It Is Not an OS
2.1 微内核结构
微内核结构的相关基础概念就不再赘述了，下图充分说明了微内核与常用的单内核结构的不同之处
根据文档，我们着重说明如下几点
2.1.1 TCB（Trusted Computing Base）的概念
1. seL4在描述内核安全性时引入了TCB的概念，表示整个系统中，必须被认为是运行正确的部分。简单来说，就是内核组织越庞大，越容易引入错误并受到攻击
2. 使用单内核结构的Linux，由于内核态代码组织庞大（已超过2000W行），bug自然更多，也更容易遭到攻击
3. seL4内核态代码仅1W行，显然TCB更小。这也是seL4衡量安全性的一个重要指标
2.1.2 微内核提供的机制
seL4作为一个极简的OS内核，几乎不提供任何系统服务，但是提供如下3种能力，
1. 提供安全的对硬件资源的复用机制
2. 程序之间的隔离机制
3. 提供安全的程序间调用机制（出于历史原因，称作IPC）
2.1.3 seL4的"IPC"
1. 使得A程序可以调用B程序中的函数（注意本例中A call B的调用方向）
2. 微内核负责在AB程序间传递参数与返回值
3. A程序调用B程序中函数的方式受到严格限制
① B程序中开发的函数只能通过exported entrypoin调用（可以理解为一种对外部模块提供接口的机制）
② A程序必须明确获得相应的capability
说明：对于A call B的场景，提供调用的进程B称作server，调用函数的进程A称作client
2.1.4 How to (and how not to) use seL4 IPC
Link: How to (and how not to) use seL4 IPC
1. seL4中的IPC并不是一种进程间的数据传送机制，也不是进程间的同步机制
2. seL4中的IPC是一种用户控制的进程上下文切换机制，由于是由用户控制的，具有如下特点，
① 不涉及调度器
② 在用户触发切换时，可以携带一些数据（也就是IPC的参数和返回值）
因此，seL4的IPC是一种跨地址空间的函数调用机制
3. 理解了IPC的本质是函数调用，那么IPC的API就应该只有如下2类，
4. 理解了seL4 IPC的本质，就需要注意如下IPC使用的禁忌
① 不要在IPC中传递大量数据
因为IPC message就是函数调用参数，你也不会在调用函数时传递大量数据吧
② 除了协议初始化或者异常处理，不要使用send-only或receive-only的IPC
③ 不要使用IPC作为同步手段
需要同步时，使用Notification机制
④ 不要使用跨CPU核（cross-core）的IPC
2.1.5 seL4提供服务的方式
1. 在微内核系统中，系统服务和应用程序一样，都是运行在用户态的进程
2. 提供系统服务的程序具备IPC接口，供应用程序调用
3. seL4目前支持的系统服务如下（目前能提供的组件不多，这是seL4的一个不足之处）
Available userlevel components | seL4 docs
说明：seL4提供的组件包括Native component libraries / Camkes reusable components / Device drivers三类，如何将他们结合起来组成一个提供服务的进程，还需要其他学习内容的支持
2.1.6 component framework
从上面的说明可以看出，将各个组件结合成一个系统服务还是很复杂的，在seL4中提供了component framework，帮助开发人员完成大部分系统整合工作，使得我们可以将注意力集中在如何实现系统服务的逻辑
seL4主要支持2种component framework，
1. CAmkES（Component Architecture for microkernel based Embedded Systems）
CAmkES是一种静态架构，预先定义好一系列component，当系统启动后不再改变
2. Genode
更强大的component architecture，但是手册的话里话外就是告诉你不要用它（比如没有过安全认证），所以我们就不再关注了
说明：总结一下上面零散知识点想说明的问题
① 在微内核系统中，除了最核心的IPC、Thread等内容，其他都是运行在用户态的进程（可以看作一个component）
② seL4为component之间提供了IPC手段，供他们之间进行交互
③ 可以使用component framework帮助构建component，我们使用静态的CAmkES框架
2.2 seL4作为hypervisor
如上文所述，seL4目前能提供的组件数量还不太多，尤其缺乏网络协议栈、文件系统和设备驱动，一种解决问题的方式就是在seL4上运行一个Linux虚拟机，借用其中成熟的组件
下面以网络设备和文件系统为例，说明这种使用场景
说明：手册中并不是说这是标准的实现方式，这里只是为了展现seL4与Guest Linux协同工作的使用框架
2.2.1 借用Guest Linux的网络设备驱动
1. Native app需要使用网络服务
2. 网络协议栈运行在native（seL目前支持LwIP和PicoTCP协议）
3. 使用Guest Linux中的网卡驱动，而不是将其porting到native
4. Native运行的协议栈通过IPC与Guest Linux交互；Native app通过IPC和Native运行的协议栈交互，获得网络服务
说明1：从上图中可以看出seL4中严格限定的IPC关系
说明2：对于被借用网络设备驱动的Guest Linux，一般裁剪到"仅包含网络设备驱动"的水平
2.2.2 借用Guest Linux的文件系统
1. Native app需要使用文件系统服务
2. 使用Guest Linux中的文件系统
3. 存储设备的flash驱动运行在native
4. Native运行的flash driver通过IPC与Guest Linux交互；Native app通过IPC和Guest Linux交互
Chapter 3：seL4's Verification Story
说明1：本章中有关于CAmkES component framework的介绍
说明2：个人觉得理解CAmkES的使用方法是实现一个系统服务的关键，一个系统服务就是在CAmkES的帮助下，首先构成一个component（并实现其中的功能），然后定义该component的外部接口
3.1 CAmkES抽象视图
seL4中的系统视图，就是一系列作为黑盒的组件，在组件之间定义了IPC通路。下面说明抽象视图中的3个部分
1. Component
component就是一个程序（进程），其中封装代码和数据
2. Interface
① interface定义了一个component如何调用其他component，或者被其他component调用（在图中就是component框框上的修饰图形，不同的图形表示不同的interface种类）
② shared-memory类型的interface是对称的
③ 其他类型的interface有明确的方向，且只有一个方向。要么是调用别人，要么是被别人调用
3. Connectors
① connectors将interface连接起来
② CAmkES中的connectors都是一对一的，如果要实现广播或多播，可以通过将一个input拷贝到多个output实现
3.2 CAmkES如何参与构建系统
1. CAmkES使用CAmkES ADL语言来描述component以及component的interface与connector
2. 在编译过程中，ADL语言描述的对象（component / interface / connector）会被映射为seL4中的对象以及对这些对象的访问权限（也就是上面提到的capability能力）
3. 这个就是引入CAmkES框架的原因，他大大简化了系统的构建，用户只需要做2件事，
① 使用ADL语言描述component的结构
② 使用C语言实现component的逻辑
说明1：虽然CAmkES ADL语法还没学习，但是不展示个实例的话实在是没有直观的认识，下面是vm_virtio_net模块的.camkes文件
可见connection中包含了类型和指定的调用方向
说明2：引入CAmkES的动机
首先得知道，为什么要有CAmkES这么个东西，从上文的描述中可以看出CAmkES框架对构建系统，以及实现系统服务、设备驱动和网络协议的重要性
① CAmkES用于抽象seL4系统的底层机制（从上文可以看出，这些底层机制琐碎且复杂，个人觉得这是最重要的一点）
② CAmkES帮助将系统拆分为功能模块，同时提供了IPC机制，这样既简化系统设计，也简化了系统实现
Chapter 4：About Capabilities
说明：后续的4个章节和直接上手编程的关系相对较小，因此只是记录了阅读过程中的note
1. seL4中的capability封装了对一个对象的引用和对该对象的访问权限
2. 以我们关心的CAmkES层面为例，一个connector被表示为一个endpoint对象，要调用该connector的client component就需要相应的capability，其中既包含该对象的引用也包含访问权限
如上文所述，CAmkES框架会实现这种对象的映射
3. seL4共有10种对象，均需要通过capability来引用
由此也可以看出，没有CAmkES框架的协助，构建seL4系统会非常复杂
Chapter 5：Support for Hard Real-Time Systems
1. seL4是启用保护模式下的实时操作系统，这里的保护模式，指的是使能了内存保护功能（即引入了MMU）
2. seL4在内核态处理中断时是关中断的，这可以简化内核的设计与实现（比如不用考虑中断嵌套）
3. 在内核态处理中断时都关中断，在seL4中不会影响中断处理的延迟变大，原因如下，
在使能了MMU的系统中，进出内核态的上下文切换耗时巨大。因此尽早开中断导致上下文切换的开销，还不如在关中断的情况下尽快把中断处理完
Chapter 6：Security is No Excuse for Poor Performance
简单一句话就是seL4在实现很高安全性的同时，没有牺牲性能
Chapter 7：Real-World Deployment and Incremental Cyber Retrofit
本章值得说一下的，就是seL4的增量化部署方式，该过程描述了HACMS项目引入seL4的过程
Step 0：原系统运行在Linux中，目标是迁移到seL4
Step 1：将整个原有的Linux作为Guest OS运行在seL4之上（这步先保证原有系统的功能可运行）
Step 2：使用native运行的网络协议栈，同时将Linux中的一些untrusted software剥离到另一个Guest Linux中。这样包括原来的Guest Linux，系统中共有3个部分，他们通过CAmkES channel交互
Step 3：将关键模块均在native运行，Guest OS中仅运行和camera相关的软件
seL4操作系统基础01：seL4 whitepaper概览相关推荐
- seL4操作系统基础02：从Hello World开始
目录 1 实验环境部署 1.1 Ubuntu环境搭建 1.2 实验代码下载 1.3 实验代码使用方法 1.3.1 提取实验代码 1.3.2 编译实验代码 1.3.3 运行实验代码 2 Hello Wo ...
- seL4操作系统基础05：event interface与seL4Notification connector
目录 1 示例程序分析 1.1 示例程序结构 1.2 CMakeLists.txt文件分析 1.3 component类型定义 1.3.1 event interface概述 1.3.2 event ...
- seL4操作系统基础06：dataport interface与seL4SharedData connector
目录 1 示例程序分析 1.1 示例程序结构 1.2 CMakeList.txt文件分析 1.3 component类型定义 1.3.1 dataport interface概述 1.3.2 data ...
- 《Scikit-Learn与TensorFlow机器学习实用指南》 第01章 机器学习概览
本书翻译已加入ApachCN的开源协作项目,见 https://github.com/apachecn/hands_on_Ml_with_Sklearn_and_TF/tree/dev/docs. 我 ...
- 干货！操作系统基础知识汇总！转给要面试的同学吧
作者:Guide哥 来源:公众号 JavaGuide 很多读者抱怨计算操作系统的知识点比较繁杂,自己也没有多少耐心去看,但是面试的时候又经常会遇到.所以,我带着我整理好的操作系统的常见问题来啦!这篇文 ...
- 电大计算机应用技术基础视频,电大形成性测评-计算机应用技术基础01
电大形成性测评-计算机应用技术基础01 (7页) 本资源提供全文预览,点击全文预览即可全文预览,如果喜欢文档就下载吧,查找使用更方便哦! 15.9 积分 01任务-在线作业试卷总分:100 ...
- 日拱一卒.操作系统基础知识点梳理
课程知识概述部分 磁盘管理体系结构 磁盘创建文件系统 磁盘挂载操作 (mount 参数信息) ! 磁盘应用环境 (作为交换分区) ! 系统启动流程 基础节点知识梳理 课程知识回顾说明 操作系统磁盘分区 ...
- linux操作系统基础命令-2
CentOS7 linux操作系统基础命令-2 1.在linux 操作系统中 有内部命令和外部命令之分,使用type命令可以查看该命令是外部命令还是内部命令 . [root@000000 ~]# ty ...
- Java 基础-01 Java语言入门
文章目录 Java 基础-01 Java语言入门 1.计算机基本概念 1.1 计算机概述 1.2 计算机组成 1.3 CPU.内存与硬盘 2.软件基本概念 2.1 软件概述 2.2 人机交互方式 2. ...
最新文章
- Oracle基本操作（二）
- 【java】在分页查询结果中对最后的结果集List进行操作add()或remove()操作，报错：java.lang.UnsupportedOperationException...
- 第三章 用户界面设计
- 微服务可靠性设计--转
- linux脚本重启进程,linux下通过脚本实现自动重启程序
- Python学习——K近邻算法
- 计算机基础知识真题模拟7,计算机一级考试计算机基础及Photoshop应用模拟试题（7）...
- 5月8号－－华为正式推出新企业标识
- Jquery ThickBox的使用
- mac 配置mysql odbc_如何在Mac上装载ODBC驱动程序?
- 5G协议演进（包括3GPP协议版本）
- 云课堂智慧职教自动签到
- Centos7.X安装mariadb及卸载mariadb安装mysql方法
- [WINDOWS]多个文本文件内容合并到一个文本文件中
- FileHelpers Library
- Python实现公众号每日自动发早/晚安消息（详细教程）
- LLVM 之父 Chris Lattner：模块化设计决定 AI 前途，不服来辩
- 2023 年 10 大最佳技术职业 ，十大 IT 职业是什么？
- 基于MFC平台实现SOCKET通信
- [CloudXNS经验分享]修改NS，域名接管状态为×时不着急