系统与数据库2020sel4.systems
SeL4 微内核：介绍
The SeL4 Microkernel: An Introduction
进阶 · 约 40 分钟读完前置知识：操作系统基础、微内核概念、形式化验证基础
导读
这是 seL4 微内核的官方白皮书（介绍性文档），系统介绍 seL4 是什么、它的形式化验证与安全保障体系、面向安全关键/嵌入式与信息物理系统的特性、性能基准，以及在旧系统上进行增量式网络安全改造等典型使用场景。核心主张是：经过形式化验证的微内核可以为安全与安全关键系统提供独特的保证。
HN 关注点：形式化验证微内核的实际价值与落地：验证规模的可扩展性、商业与国防领域的采用难度，以及普通用户何时能买到基于 seL4 的路由器/防火墙。
后来怎么样
seL4 被视为首个通过形式化验证的通用微内核，成为高保障系统领域的标杆，并影响了一系列经过验证的内核与安全关键系统研究；不过其商业大规模采用仍然有限。
HN 评论精选
这几条评论里：支持 1 补充 2 亲历 1
支持验证不必覆盖全部，小 TCB 加上加密即可把驱动/网络栈排除在关键安全边界之外，AMNESIA:33 案例证明了这一点。
关于验证的可扩展性：你不需要验证所有东西就能获得巨大的安全性/可靠性提升。结构良好的系统有很小的可信计算基（TCB），只要把 TCB 做对，即使 TCB 的部分组件未经验证，系统也可以相当安全。例如，如果你对所有数据加密，驱动和网络栈就在 TCB 之外，它们最多只能威胁可用性。AMNESIA:33 就很好地证明了这一点：对基于 seL4 的操作系统来说，它只是个小问题，而不是严重漏洞（链接）。这也印证了我几年前的分析——我研究了 Linux 上的严重漏洞在基于 seL4 的操作系统里会有多严重（提示：基本都不严重）。
microkerneldude查看英文原文
Re scalability of verification: you don't have to verify everything to get a massive security/safety boost. A well-structured system has a small trusted computing base (TCB), and if you get that right, your system can be pretty secure even if parts of the TCB remain unverified. Eg drivers and network stacks are outside the TCB if you encrypt all data, they can only threaten availability. This was just demonstrated pretty well with AMNESIA:33: for an seL4-based OS, it's just a minor issue, not a critical vulnerability: https://hensoldt-cyber.com/2020/12/08/how-amnesia33-does-affect-trentos-not/. This confirms my analysis from a few years ago, looking at critical exploits in Linux and how seriously they'd be in an seL4-based OS (hint: mostly not at all): https://ts.data61.csiro.au/publications/csiro_full_text//Biggs_LH_18.pdf
亲历亲历者：seL4 在国防等领域推销困难，商业采用率低，好在 UNSW 团队提供了面向决策者的商业论证文献。
当年我曾大力推动在某些国防应用中增加对 seL4 的投资。但不能低估其中的微妙之处——根据我的经验，对于本来就不熟悉形式化方法、安全、内核/操作系统等领域的人，这往往很难推销。在我参与的应用之外还有不少更容易摘的果子（比如网络硬件），但商业采用率似乎仍然很低，也许原因就在于此。值得称赞的是，Trustworthy Systems 和 UNSW 团队做了出色的工作，产出了以决策者能接受的方式阐述商业价值的文献。尤其是这篇论文对我多次很有帮助（链接）。
verberant查看英文原文
In a past life, I pushed hard for more investment in seL4 for certain defense applications. The nuance isn't to be underestimated though – I can say from experience that it's often a hard sell to folks that aren't already versed in the ins and outs of formal methods, security, kernels/operating systems, etc. There are plenty of lower hanging fruit (like networking hardware) than the applications I worked on, yet commercial adoption still seems low. Maybe this is due to that nuance. To the credit of the folks at Trustworthy Systems and UNSW, they've done a great job producing literature that outlines the business case in a manner palatable to decision makers. This paper [0] in particular came in handy to me many times. [0] https://ts.data61.csiro.au/publications/csiro_full_text/Klein_AKMHF_18.pdf
补充普通用户的需求：希望有可购买/可自建的 seL4 路由器或防火墙产品。
要怎样才能有一个我能自己构建或购买的 seL4 路由器/防火墙？任何直接连到互联网的东西都需要这类安全保证。
5d749d7da7d5查看英文原文
What will it take for there to be a sel4 router/firewall I can build/buy? Anything directly connected to the internet needs these kind of security guarantees.
补充引用白皮书摘要，概括其内容范围：定义、保证体系、安全特性、性能与使用场景。
“本白皮书介绍并概述 seL4。我们说明 seL4 是什么（以及不是什么），并探讨其决定性特性。我们解释为什么 seL4 能独特地胜任安全与安全关键系统、以及一般嵌入式与信息物理系统的操作系统内核之选。特别是，我们阐述 seL4 的保证体系、其与安全性和安全性相关的特性，以及树立标杆的性能。我们还讨论典型使用场景，包括对遗留系统进行增量式网络改造。”
DyslexicAtheist查看英文原文
> This whitepaper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety-critical systems, and generally embedded and cyber-physical systems. In particular,we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
- 代码
- github.com/apple-oss-distributions/xnu被提到 2 次
- github.com/seL4/l4v被提到 2 次
- github.com/seL4/seL4被提到 2 次
历次讨论
- 2020Hacker News 讨论帖84 分 · 29 评
- 2025Hacker News 讨论帖264 分 · 188 评
同领域还值得读
I/O 比 CPU 更快——让我们划分资源并消除操作系统抽象
I/O Is Faster Than CPU – Let’s Partition Resources and Eliminate OS Abstractions
指出在现代服务器硬件上 I/O 速度已接近甚至超过 CPU，传统操作系统抽象反而成为瓶颈。
系统与数据库2019 · 817 分 · 277 评进阶 · 约 30 分钟编辑精选使用 io_uring 的高效 I/O
Efficient IO with io_uring
由 Linux 内核开发者 Jens Axboe 撰写，介绍 Linux 新的异步 I/O 接口 io_uring。
系统与数据库2019 · 426 分 · 96 评进阶 · 约 45 分钟编辑精选线程对大多数用途而言是个坏主意（1995）
Threads Are a Bad Idea for Most Purposes (1995)
这篇 1995 年的文章由 John Ousterhout 撰写，讨论为什么线程对大多数用途而言是坏主意，并主张事件驱动编程通常更简单、更高效。
系统与数据库2017 · 423 分 · 382 评进阶 · 约 25 分钟编辑精选学习型索引结构之论证
The Case for Learned Index Structures
提出把索引看作一种"模型"：既然 B-tree 等结构本质上是在学习数据的分布，就可以用机器学习模型（如回归模型、神经网络）来近似键到位置的映射，从而替代 B-tree、哈希索引…
系统与数据库2017 · 398 分 · 66 评 · 引用 25进阶 · 约 60 分钟编辑精选FoundationDB：一个分布式、解耦的事务型键值存储
FoundationDB: A distributed, unbundled, transactional key value store
介绍 FoundationDB：一个分布式、解耦设计的事务性键值存储。
系统与数据库2021 · 283 分 · 99 评进阶 · 约 90 分钟编辑精选