<aside> 💬 Takeaway Messages

“操作系统” 的含义随应用而变

• 可以大而全 (Linux/Windows API)
• 可以只有最少的硬件抽象 (Microkernel)
• 可以没有用户态 (Unikernel)

互联网时代

• 从井里走出去：RTFM, RTFSC
• 然后去改变这个世界 </aside>

<aside> 💬 操作系统设计 - 一组对象 + 访问对象的 API

操作系统实现 - 一个 C 程序实现上面的设计

</aside>

The Base Specifications Issue 7

• XBD: Base Definitions
• XSH: System Interfaces
• XCU: Shell & Utilities
• XRAT: Rationale

Microkernel (微内核)

<aside> 💬 Microkernel - 只把 “不能放在用户态” 的东西留在内核里

• 状态机 (拥有寄存器和地址空间的执行流)
• 状态机之间的协作机制 (进程间通信)
• 权限管理 (例如设备访问)

赋予进程最少的权限，就能降低错误带来的影响

</aside>

Minix

不让进程直接进入kernel mode操作，而是利用send和receive让内核完成后交给用户程序

操作系统还是操作系统，但跨模块调用会跨越进程边界

把缺陷isolate到每一个模块中，即使有安全漏洞也不会导致整个内核直接crash

Minix3 Architecture

seL4

seL4

世界上第一个 verified micorkernel

<aside> 💬 怎么证明？

1. 用适合描述行为的语言建立一个模型（如 Python )
2. 再用C语言去实现行为
3. 证明两个数学对象 (状态机) 可观测行为的等价性 </aside>