seL4安全证明在AArch64上完成

# Proofcraft 新闻 - 2026 来源：https://proofcraft.systems/news-2026/ ## seL4 在 AArch64 上的安全性证明现已完成 继完成**功能正确性**（https://proofcraft.systems/news-2024/#2024-04-01）和**完整性**（https://proofcraft.systems/news-2025/#2025-04-29）证明之后，Proofcraft 现已建立 seL4 在 AArch64 上强制执行**机密性**（https://sel4.systems/Verification/proofs.html）的证明，提供了形式化的数学证明，表明该内核可防止运行在 seL4 之上的应用程序在未获授权的情况下获取信息。 感谢 **NCSC**（https://www.ncsc.gov.uk/）的持续支持，这一里程碑完成了证明 seL4 在 AArch64 上的实现代码强制执行运行在其上的应用程序之间安全隔离的正式证明（基于此处列出的假设 https://sel4.systems/Verification/assumptions.html）。这种隔离可以防止针对非关键应用程序的攻击传播并危及关键应用程序。 seL4 在 AArch64 上的证明现状图，机密性已完成，系统初始化已启动 ## 在 LICS'26 上的证明工程与理论 论文《迭代构造的代数》（https://proofcraft.systems/lics26-preprint.pdf）的封面 由 Kevin Batz、Benjamin Lucien Kaminski、Lucas Kehrer、Gerwin Klein、Henning Urbat 和 Todd Schmid 撰写的论文**《迭代构造的代数》**（https://proofcraft.systems/lics26-preprint.pdf）本周在里斯本举行的第 41 届计算机科学逻辑年度研讨会（**LICS** (https://lics.siglog.org/lics26/)）上发表。这篇理论计算机科学论文讨论了一种用于迭代构造不动点的代数抽象和推理原则。不动点是计算机科学中一个反复出现的主题，有许多著名的结果，例如 Kleene 不动点定理。本文展示的代数允许简洁地表达这些定理，并能够以抽象和简化的方式进行推理，这种方式可以在 Isabelle/HOL 等证明助手中高效实现，而 Proofcraft 正在使用它来验证 seL4 微内核。 本文中高度自动化的 Isabelle/HOL 迭代代数实现源于 Proofcraft 首席科学家 Gerwin Klein 与 Benjamin Kaminski 在 2025 年雅典 IFIP 工作组 2.3（编程方法）会议上的一次自发合作。这表明证明工程的范围从实际应用一直到深层理论。 ## MCS seL4 现已验证完成！（针对 RISC-V） Proofcraft 在 **L4**（https://sel4.systems/）验证路线图上实现了一个多年规划的重要里程碑：seL4 的 MCS 配置——为混合关键性系统提供支持——现在已在 RISC-V 上被证明是正确的。 该配置是 seL4 最大的新特性，对于汽车用例等混合关键性实时应用不可或缺。它包含了对内核实现和 API 的广泛更改。因此，其验证需要付出巨大努力，并且长期以来一直是 seL4 路线图的优先事项。 Proofcraft 现已首次完成了支持 MCS 的 seL4 功能正确性验证。功能正确性是 **seL4 验证栈**（https://sel4.systems/Verification/proofs.html）中最大和最核心的证明。该证明针对 RISC-V 架构，现在将作为 **DARPA PROVERS 计划**（https://proofcraft.systems/news-2024/#2024-12-02）的一部分移植到 Arm 64 位架构。 MCS 验证状态图 ## 用于 seL4 的动态域调度器 Proofcraft 交付了在 **seL4**（https://sel4.systems/）中实现更灵活域调度的实现和形式化证明。 在更改之前，seL4 安全性证明，特别是信息流强制执行的证明，要求一个完全静态的调度表编译到内核中。这意味着，当使用 seL4 来强制执行应用程序之间的信息流边界时，开发者必须为整个运行系统生命周期内的每个域提供固定、预定的时间量。这种严格的策略使得在实践中应用信息流控制以及在 SDK 风格的开发（如 **Microkit**（https://docs.sel4.systems/projects/microkit/））中支持该功能变得困难。 Proofcraft 提出了一种新的 seL4 运行时 API（应用程序编程接口），允许加载半静态域调度表。这意味着具有信息流保护的系统可以在运行时经历不同的阶段，以满足不同的域定时要求。例如，系统的引导阶段可以有更长的时间片，以允许虚拟机启动而不会超出其域时间分配；而系统的运行阶段可以提供更短的时间片，以便每个域能够及时响应外部交互。此外，像 Microkit 这样基于 SDK 的系统可以使用新 API 在引导时设置域调度表。 这个新的 seL4 API 已在 seL4 15.0.0 中实现、验证并可用。 示意图展示了一个调度表（之前的状态）与多个静态调度表（当前状态）的对比 ## June Andronick 在斯德哥尔摩 CDIS 春季会议上发表主题演讲 2026年5月21日，**CDIS** (https://www.kth.se/cdis)——瑞典网络防御与信息安全研究中心——在斯德哥尔摩 KTH 理工学院举行了其**春季会议**（https://www.kth.se/cdis/konferens/cdis-spring-conference-2026-1.1465243）。 Proofcraft 首席执行官 June Andronick 与来自 Mistral AI 的 August Martens 一起担任两位主题演讲嘉宾之一。June 概述了用于网络安全的形式化验证，并参与了一个关于数字主权的讨论小组。 June 演讲和参加讨论小组的照片 ## Proofcraft 在 Cyberagentur 里程碑研究峰会上进行展示 峰会上两次演讲的两个标题页表示图 2026年4月，德国 **Cyberagentur** 举办了一个里程碑研究峰会，展示其资助项目的进展和成果，包括 **ÖvIT**（受信任的 IT 生态系统研究计划）(https://www.cyberagentur.de/en/press/a-milestone-for-it-security-in-germany/)，Proofcraft 是该计划的**接受者**（https://proofcraft.systems/news-2025/#2025-01-20），并与 **Kry10** (https://www.kry10.com/) 合作。 Proofcraft 首席科学家 Gerwin 和 Kry10 首席科学家 Martin Dehnel-Wild 展示了 Dyvercon 项目的进展，该项目旨在为复杂的网络物理系统提供动态性、性能和证明。具体而言，Gerwin 报告了 Proofcraft 在扩展 **seL4**（https://sel4.systems/）证明以支持静态多核配置方面的工作，在该配置中，应用程序可以利用多个 CPU 核心来提高性能，同时在内核级别，每个核心上运行一个独立的 seL4 实例。 Gerwin 还对形式化验证进行了总体介绍，并概述了其在现实世界中的应用。 ## Proofcraft 是 seL4 峰会 2026 的骄傲赞助商 seL4 峰会 (https://sel4.systems/Foundation/Summit/2026/) 的标志 Proofcraft 很高兴能作为银牌赞助商支持 **2026 seL4 峰会** (https://sel4.systems/Foundation/Summit/2026/)。 seL4 峰会是一年一度的国际聚会，汇聚了来自工业界、政府和大学的、对世界上最高保证程度的操作系统内核感兴趣的参与者。与会者和演讲者包括 seL4 技术的创造者和维护者，例如 Proofcraft 团队。 今年的 seL4 峰会将于 2026 年 9 月 1-3 日在加拿大温哥华举行。 温哥华天际线图标 ## Proofcraft 五年了。距离验证化的未来又近了一步。 带有5个烟花的Proofcraft标志 2021年4月14日，我们创建了 Proofcraft。五年后，我们正忙于为验证化的未来工作，以至于有一段时间没有发布新闻了。 发生了很多事情，未来还有更多。现在，这里是我们积压的一些新闻帖子，包含了 Proofcraft 一直交付的技术亮点。 首先，seL4 的证明现在**支持内核可以运行的所有 Arm 平台** (https://proofcraft.systems/news-2025/#2025-09-02)。在减少对专家依赖这一重大进展之后，seL4 用户现在可以在支持的 Arm 平台之间自由选择，并始终确保他们使用的是经过验证的代码库。这项工作是 DARPA PROVERS 计划的一部分。 其次，AArch64 上的 seL4 现已可证明地强制执行**完整性** (https://proofcraft.systems/news-2025/#2025-04-29)：我们有形式化的数学证明，表明该内核可防止运行在 seL4 之上的应用程序在未获授权的情况下修改数据。安全性定理的工作仍在继续：感谢 NCSC 的持续支持，我们即将完成机密性属性的证明，至此，64 位 Arm 架构的整个安全性证明栈就完成了。 还有更多进展，三个大型项目正在并行推进，分别由 **DARPA** (https://proofcraft.systems/news-2024/#2024-12-02)、**Cyberagentur** (https://proofcraft.systems/news-2025/#2025-01-20) 和 **NCSC** (https://www.ncsc.gov.uk/) 资助。敬请关注更多信息！ LinkedIn 主页 (https://www.linkedin.com/company/proofcraft/) seL4 是 LF Projects, LLC 的注册商标。