文章摘要
Proofcraft完成了seL4在AArch64架构上的机密性形式化证明，标志着该内核实现了应用间安全隔离的完整数学验证，防止非授权信息泄露。相关成果将在LICS'26发表。
文章总结
好的，这是根据您的要求，对原文进行中文重述和精简后的版本：
Proofcraft 2026年新闻摘要
1. seL4 在 AArch64 架构上完成机密性证明 在完成功能正确性和完整性证明后，Proofcraft 现已完成 seL4 微内核在 AArch64 架构上强制实施机密性的正式数学证明。该证明确认内核能防止未经授权的应用程序获取信息。在英国国家网络安全中心（NCSC）的持续支持下，这一里程碑标志着 seL4 在 AArch64 上实现了对上层应用的安全隔离的完整形式化证明。
2. 证明工程与理论：LICS'26 会议论文 一篇题为《迭代构造代数》的论文在第41届逻辑与计算机科学年度研讨会（LICS'26）上发表。该论文提出了用于迭代构造不动点的代数抽象与推理原则，其成果可在 Isabelle/HOL 等证明助手中高效实现。该合作始于 Proofcraft 首席科学家与 Benjamin Kaminski 在 IFIP 工作组会议上的交流，展示了证明工程从实际应用延伸至深层理论的能力。
3. MCS 配置的 seL4 在 RISC-V 上完成验证 Proofcraft 实现了 seL4 验证路线图上的一个重要里程碑：支持混合关键性系统的 MCS 配置，现已在 RISC-V 架构上被证明功能正确。这是 seL4 最大的新特性，对汽车等混合关键性实时应用至关重要。该验证工作耗时巨大，是 seL4 长期以来的优先事项。下一步，该证明将被移植到 Arm 64位架构。
4. 为 seL4 实现动态域调度器 Proofcraft 为 seL4 交付了更灵活的域调度实现及其形式化证明。此前，seL4 的安全证明要求一个完全静态的调度表。新方案提出了一个运行时 API，允许加载半静态的域调度，使系统可在不同阶段满足不同的域定时需求（例如，启动阶段使用更长的时隙，运行阶段使用更短的时隙）。该新 API 已在 seL4 15.0.0 版本中实现、验证并可用。
5. June Andronick 在斯德哥尔摩 CDIS 春季会议上发表主题演讲 Proofcraft CEO June Andronick 在瑞典皇家理工学院举办的 CDIS 春季会议上担任主题演讲嘉宾，概述了形式化验证在网络安全中的应用，并参与了关于数字主权的专题讨论。
6. Proofcraft 在德国 Cyberagentur 里程碑研究峰会上发表演讲 Proofcraft 首席科学家在德国 Cyberagentur 的峰会上，介绍了“Dyvercon”项目的进展，该项目旨在为复杂的网络物理系统提供动态性、性能和形式化证明。报告重点包括扩展 seL4 证明以支持静态多内核配置，使应用能利用多核 CPU 提升性能。
7. Proofcraft 赞助 2026 年 seL4 峰会 Proofcraft 作为银牌赞助商支持 2026 年 seL4 峰会。该峰会将于 2026 年 9 月 1 日至 3 日在加拿大温哥华举行。
8. Proofcraft 成立五周年 自 2021 年 4 月 14 日成立以来，Proofcraft 已走过五年。期间，团队取得了多项技术进展：seL4 证明现已支持内核可运行的全部 Arm 平台；seL4 在 AArch64 上已可证明强制实施完整性。目前，由 DARPA、Cyberagentur 和 NCSC 资助的三个大型项目正在并行推进。
评论总结
根据评论内容，总结如下：
主要观点与论据：
seL4的应用场景（评论1，评分None）：用户询问seL4的操作系统支持情况，列举了GenodeOS、LionsOS，并提到中国汽车制造商将其用作车载虚拟机监控器。关键引用："What operating systems use SeL4? I know of the following: GenodeOS, LionsOS, A chinese car maker was using it as a hypervisor in their cars."
安全性质疑（评论2，评分None）：用户预测侧信道时序攻击将完全否定seL4的安全性结论。关键引用："Coming soon: a side-channel timing attack which completely invalidates this result."
技术限制（评论3，评分None）：用户指出seL4的验证结果仅适用于非混合关键性系统（non-MCS）和单核（unicore）环境。关键引用："Read the fine print, 'non-MCS (mixed criticality systems), unicore'."
市场与改进需求（评论4，评分None）：用户认为嵌入式与军事市场可能继续资助seL4，但若想真正提升系统安全，需开发原生seL4/Linux方案，因为安全启动虚拟化平台已很常见。关键引用："The embedded and military markets may keep funding them... but they need a native seL4/Linux if they want to honestly claim they are improving systems' security."
平衡性总结： - 支持方：seL4已在多个操作系统和实际场景（如汽车）中应用。 - 反对方：存在侧信道攻击风险、验证范围有限（仅限非MCS单核）、需与Linux整合才能提升安全性，且当前安全启动方案已普及。