Proofcraft在最新一期新闻公告里宣布，seL4微内核在AArch64架构上的机密性证明已经完成。加上此前完成的功能正确性和完整性证明，seL4在这颗芯片架构上第一次拼出了完整的安全隔离证明链——用数学方式证明一个应用跑在seL4之上，既不能未经授权修改别人的数据，也不能未经授权窥探别人的信息。这项工作由英国NCSC持续资助，理论上意味着自动驾驶、军用系统这类高保障场景，终于可以在AArch64上找到一个证明完整的信任根。
但把seL4官方文档翻出来对照，会发现一件挺尴尬的事：同一个verified-configurations页面，在检索的不同时间点，一份写着AArch64机密性证明“in progress”，另一份写着已经“complete”。两份文档指向同一个URL，却给出相反的答案。这不是哪家媒体转述出了错，而是seL4项目自己的权威页面存在版本滞后或缓存不一致。对一个把“形式化证明”当作核心卖点的项目来说，证明本身可以做到滴水不漏，证明状态怎么对外传播却出了岔子，这本身就值得记一笔。
证明了什么，没证明什么
机密性证明听起来像是给系统上了一把绝对锁，实际边界要窄得多。seL4的假设条件里明确写着：这个证明不覆盖时序侧信道和微架构侧信道，也就是说，通过缓存命中时间、执行耗时这类旁路推断信息的攻击，不在证明范围内。DMA设备如果没有被信任、禁用或单独验证，同样可以绕过证明直接读写内存。启动代码、底层汇编、缓存和TLB管理，则被列为“假设成立”而不是“被证明成立”的部分——换句话说，这些环节出了问题，整套证明链条一样会失效。
- 风险.TrustZone架构下，seL4只跑在Non-secure EL2，EL3固件和Secure world完全在证明边界之外，理论上可以在seL4看不见的情况下修改系统状态。
这意味着，一个宣称“基于seL4机密性证明”的系统，如果同时用了TrustZone做安全分区，或者外设走DMA直连，光靠这纸证明并不能覆盖整个攻击面。采购方如果把“数学证明”直接等同于“绝对安全”，中间这段落差需要自己补上。
AArch64比RISC-V差在哪
横向看seL4整个证明矩阵，AArch64目前只验证到C代码层面，还缺一个关键环节：二进制级正确性证明（binary correctness），也就是编译器和链接器把C代码翻译成机器码这一步是否被证明忠实。RISC-V64和AArch32的标准配置已经补上了这一层，AArch64还没有。
对芯片选型和系统架构师来说，这条差距是实打实的。AArch64的优势是EL2虚拟化能力更成熟，但如果系统对可信基（TCB）要求严格到连编译工具链都要纳入证明范围，目前RISC-V64反而是更完整的选项。
MCS和调度器：留给汽车与国防的进度表
同一批公告里，MCS（混合关键性调度）配置的功能正确性证明率先在RISC-V上跑通，这是seL4路线图里体量最大的新特性，专门服务汽车这类需要实时性和安全隔离并存的场景。AArch64版本还没做完，按公告说法会作为DARPA PROVERS项目的一部分继续移植。也就是说，想在AArch64上用MCS配置做混合关键性汽车电子或军用实时系统的团队，目前还得等。
- 结论.seL4 15.0.0里新增的动态域调度器API算是这轮公告里最直接的工程价值——它让信息流隔离系统可以在启动阶段和运行阶段切换不同的静态调度表，不用再为整个生命周期焊死一份时间片分配，Microkit这类SDK开发者会最先感受到这个变化。
NCSC在这轮进展里的角色，公开记录显示始终是资助方和seL4基金会的生态成员，并没有对外发布过“认证”AArch64机密性证明的正式声明。这个区别在政府采购的合规表述里很关键——把资助方的名字当成认证机构来引用，是容易踩的一个坑。
证明的数学部分可以无懈可击，证明状态的传播链条却未必同样可靠
依赖seL4做安全合规论证的团队，接下来该盯的不是“证明完不完成”这个二元问题，而是三件更具体的事：官方文档口径是否稳定下来、AArch64二进制级证明和MCS移植有没有时间表、以及自己的系统里有没有TrustZone Secure world或裸DMA外设这类天然在证明边界之外的部分。