系统与数据库2020cs.rochester.edu
用 Checked C 重构 FreeBSD 内核
Refactoring the FreeBSD Kernel with Checked C
进阶 · 约 60 分钟读完前置知识：C 语言、操作系统内核基础、内存安全概念
导读
这篇论文探讨了用微软推出的 C 语言扩展 Checked C 重构 FreeBSD 内核的可行性。Checked C 通过新增源语言构造（静态分析与运行时检查插入）来防止空指针解引用和空间内存安全错误，且对现有 C 代码保持较高的向后兼容性，允许渐进式迁移。论文报告其在选定基准测试上仅有约 8.6% 的性能开销。
HN 关注点：“更安全的 C”这一老话题的新尝试，讨论焦点是 Checked C 相比 Rust、VeriFast 等方案是否值得，以及 8.6% 的性能开销对内核来说是否可接受。
HN 评论精选
这几条评论里：质疑 2 补充 2
补充推荐 VeriFast 作为替代方案，称其兼容性更好且验证能力更强，可防住 FreeBSD 部分 CVE。
Checked C 有意思，但我觉得 VeriFast 是更有前景的方向。VeriFast 与现有 C 代码库完全兼容（可以继续用现有 C 编译器），并且能验证比 Checked C 更复杂的行为。有研究发现它本可以防止 FreeBSD 近期 50 个 CVE 中的 5 个，这些漏洞的成因包括未加锁的内存访问、资源泄漏和错误的引用计数。
moonchild查看英文原文
Checked c is interesting, but I think a more fruitful avenue would be verifast[0]. Verifast is completely compatible with existing c codebases (so you can keep using your existing c compiler), and is able to verify more interesting behaviour than checked c. [1] finds that it would have prevented 5 of 50 recent CVEs in FreeBSD, whose causes include unlocked memory accesses, resource leaks, and bad reference counts. 0. https://github.com/verifast/verifast 1. https://metasepi.org/en/posts/2020-10-14-avoid-freebsd-security-issue.html
质疑指出 Checked C 的主要卖点只是向后兼容性，可渐进迁移，但 FreeBSD 社区未必买账。
Checked C 是微软较新的研究项目，我不确定 FreeBSD 是否会热衷于围绕它做重构。此前已有许多“更安全的 C”语言，这篇论文唯一的优势似乎是 Checked C 具有更高的向后兼容性——这或许能让重构随时间逐步进行，而不需要一开始就付出巨大的工程量。
AdmiralAsshat查看英文原文
Checked C appears to be a relatively recent research project from Microsoft[0][1], so I'm not sure that FreeBSD would be terribly keen on refactoring around it. There have also been many "safer C" languages before, so the only advantage that the paper offers is that Checked C seems to have a higher degree of backwards compatibility. I suppose that would allow the implementation/refactoring to gradually occur over time, rather than requiring a herculean initial effort. [0] https://www.microsoft.com/en-us/research/project/checked-c/ [1]https://github.com/Microsoft/checkedc
质疑质疑 8.6% 的性能开销对内核而言其实并不算低。
“Checked C 性能开销很低（在选定基准上仅 8.6%）”——这难道不算相当显著吗？
ornxka查看英文原文
>Checked C has low performance overhead (only 8.6% on selected benchmarks [25]) Isn't that actually kind of significant?
补充补充论文的代码来源，指出公开代码很少，暗示工作可能不够扎实。
这似乎是一篇学士论文的演化版本，其中提供了一些代码片段（第一作者）：https://github.com/Duaiden/bachelor-thesis/tree/master/code。另外这里有一些测试代码和结果，可能还有他们的内核镜像（另一位第一作者）：https://github.com/2000jedi/checkedc-tests/blob/master/kernel。我没有找到与论文相关的其他代码。
loeg查看英文原文
This seems to be an evolution of a bachelor’s thesis, which provides some snippets: https://github.com/Duaiden/bachelor-thesis/tree/master/code (first author). And this looks to be some test code and results, as well as possibly their kernel image: https://github.com/2000jedi/checkedc-tests/blob/master/kernel (2nd first author). I have not found any other code related to the paper.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2020Hacker News 讨论帖85 分 · 13 评
- 2021Hacker News 讨论帖163 分 · 41 评
同领域还值得读
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 分钟编辑精选