太空中的O(x)Caml

# Thomas Gazagnaire :: O(x)Caml 在太空 来源：https://gazagnaire.org/blog/2026-05-14-borealis.html 4月23日，我们纯OCaml实现的CCSDS (https://ccsds.org/)协议栈在近地轨道启动运行！代号*Borealis*的项目，运行于DPhi Space (https://dphi.space/)的ClusterGate\-2 (https://software.dphispace.com/)有效载荷模块上，作为主卫星的托管载荷，实现了端到端加密的指挥控制以及后量子密钥轮换，全部代码均用安全的OCaml编写。 为什么OCaml在这里如此重要？在卫星上运行不可信代码存在巨大的安全风险 (https://gazagnaire.org/blog/2026-02-25-satellite-software.html)，而OCaml是在太空运行理想的的安全语言。在ICFP 2022主题演讲 (https://kcsrk.info/slides/icfp22_keynote.pdf)中，KC Sivaramakrishnan (https://kcsrk.info/)回顾了长达十年的工程努力 (https://tarides.com/blog/2023-03-02-the-journey-to-ocaml-multicore-bringing-big-ideas-to-life/)，最终诞生了OCaml 5，这个版本为OCaml运行时带来了安全且高性能的多线程支持。 KC在演讲最后推测，OCaml 5.0将会登月，因为它的语言特性能够在提供C/Rust级别的按需性能的同时，保持经典ML的数学严谨性。而在Parsimoni，我们有点字面理解了他的话 :-) 主卫星大约每九十分钟绕地球一圈。几个月前，Virgile Robles (https://firobe.fr/)和我在圣诞节期间捣鼓了这个项目，当我们看到以下日志时，我们（虚拟地）跳了起来： `` 2026-04-23 18:48:06 SpaceOS/Borealis (BPv7, BPSec, OTAR) by Parsimoni 2026-04-23 18:48:06 ClusterGate-2 proxy [single iteration] 2026-04-23 18:48:06 Config: scid=100, tm_vcid=0, tc_vcid=4, tm_spi=1, tc_spi=2, tm_frame_len=1115 2026-04-23 18:48:06 Session keys: EK=0x0100 AK=0x0101 active 2026-04-23 18:48:09 Telemetry health: { ... "status": "healthy" } `` ## 实际运行的是什么 Borealis是一个守护进程。在地面和卫星上，它都使用普通的客户端-服务器协议（遥测查询、命令和响应、OTAR密钥更新请求），与任何生产服务器相同。不同之处在于底层的传输线路。 协议栈是CCSDS (https://gazagnaire.org/blog/2026-04-15-ccsds-protocol-stack.html)的纯OCaml实现，CCSDS是连接航天器与地面的协议族。它涵盖从无线电帧到底层Bundle协议及其上层安全扩展的每一层；二进制格式使用`ocaml-wire` (https://gazagnaire.org/blog/2026-03-31-ocaml-wire.html)编解码器描述。 在ClusterGate-2上，仅使用了该协议栈的上层。卫星没有外部网络连接。唯一的地面链路是通过DPhi的API进行文件系统上传和下载：写入上行目录的文件会在下一次过境时由DPhi转发，下行同理。Borealis将该文件系统视为一个延迟容忍网络。每条命令、响应、遥测样本和图像块都被序列化为BPv7 (https://datatracker.ietf.org/doc/html/rfc9171)数据包并写入磁盘；DPhi将文件作为不透明字节转发。 BPSec (https://datatracker.ietf.org/doc/html/rfc9172)为每个数据包包裹两个扩展块：一个加密有效载荷，另一个进行身份验证。序列号防止重放，预共享密钥（通过下方OTAR轮换）将路由路径排除在信任路径之外。卫星操作员只能看到不透明的数据包字节；路由路径中的任何节点都无法读取、修改、伪造或替换内容。 这一点很重要，因为我们是他人硬件上的租户。在托管载荷卫星 (https://gazagnaire.org/blog/2026-02-25-satellite-software.html)上，多个租户共享一个总线，仅靠容器隔离是不够的。共享的Linux内核意味着内核级别的CVE会定期突破租户边界，同样的原语不断以新形式出现：Dirty Frag (https://dirtyfrag.io/)（今年发布的一个通用Linux本地提权漏洞）、Fragnesia (https://github.com/v12-security/pocs/tree/main/fragnesia)（同族近亲），以及"Copy Fail" (https://cert.europa.eu/publications/security-advisories/2026-005/)（2026年4月底披露的Linux内核提权漏洞，同时影响所有主要发行版）。更早的案例（2022年的Dirty Pipe (https://dirtypipe.cm4all.com/)、2024年被用于容器逃逸的f_tables use-after-free (https://nvd.nist.gov/vuln/detail/CVE-2024-1086)）表明未来还会有更多。在地面服务器上，你可以运行包管理器并重启；在轨道上，内核修补本身就是一个有其自身延迟的交付问题，有时甚至完全不可能。每个数据包周围的加密信封是唯一的持久性保证。 除了机密性和真实性之外，长期任务威胁模型还需要密钥轮换。Borealis支持对其后量子签名密钥（ML-DSA-65 (https://csrc.nist.gov/pubs/fips/204/final)）进行OTAR（空中密钥更新）。这些密钥的寿命与卫星相同（十到十五年），这就是为什么NASA的空间系统保护标准 (NASA-STD-1006A) (https://standards.nasa.gov/standard/NASA/NASA-STD-1006)将后量子命令认证视为一项要求，而非未来选项。OTAR使我们能够轮换后量子密钥，而无需重新刷写卫星。据我们所知，这将是**首次公开的轨道后量子OTAR演示**；我们计划在后续过境中执行轮换。 Borealis作为客户程序运行在DPhi的托管载荷模块上：一个Arm SoC（四个Cortex-A53核心，4 GB RAM）运行Linux。飞行二进制文件大小为5-10 MB，静态链接，以`FROM scratch` Docker镜像形式交付。它轮询总线获取遥测数据（角度、速度、位置）以及一个板载摄像头（低质量鱼眼，仅用于演示）。卫星端循环的核心代码如下： `` let send_telemetry t ~prefix payload = let bundle = make_bundle t ~source:Eid.sat_telem ~destination:Eid.ground_telem ~payload in match protect_bundle t bundle with | Ok protected -> ignore (write_bundle t ~dir:(downlink_dir t.config) ~prefix protected) | Error _ -> log t "Failed to protect telemetry bundle" `` `protect_bundle`使用来自SDLS安全关联（地面和卫星在预配时商定的加密参数）的密钥应用BPSec。如果其中任何一步失败，数据包就不会离开卫星。 上行路径与下行路径镜像。卫星从`/data/uplink/`读取数据包，使用BPSec解除保护每个数据包，并根据目的地路由到数据包层： `` if dest = Eid.sat_cmd then handle_command t payload else if dest = Eid.sat_otar then handle_otar t payload else log t "Unknown destination" `` 文本命令是解析为ADT的短UTF-8字符串；类型检查器强制执行穷尽分发： `` type cmd = Ping | Check | Capture | Halt let dispatch t = function | Ping -> send_response t ~prefix:"pong" "PONG" | Check -> run_self_check t | Capture -> capture_and_send t | Halt -> t.shutdown_requested <- true `` 添加新命令意味着添加一个构造函数；编译器会标记所有尚未处理该构造函数的位置。 OTAR密钥更新消息走另一个分支。有效载荷是二进制而非文本，使用主密钥加密，该主密钥在集成时加载到卫星上，并驻留在模块的进程内存中（模块没有TPM或安全元件，因为构建耐辐射的安全元件仍然是一个开放的硬件问题）。卫星解密新密钥，将其保存在暂存槽中，然后激活。当前的飞行循环在接收到时立即激活；该协议还支持单独的地面驱动激活步骤，操作员可以在提交前验证安装，切换到该路径只需更改飞行循环，无需编写新代码。 主密钥本身没有轮换路径。它在卫星与运载火箭对接之前就安装在有效载荷上，一旦航天器进入轨道，就没有更可信的通道来传递新密钥。如果主密钥丢失，这个协议栈将无法访问。对于没有硬件支持的密钥存储的长期任务来说，这就是诚实的失败模式。 ## 下一步：OxCaml OxCaml (https://oxcaml.org/)是Jane Street基于OCaml的编译器分支。其模式系统在卫星热路径上至关重要。Locality使我们能够将分配标记为栈绑定，这样它们永远不会到达堆，也永远不会到达GC。Uniqueness和capabilities在类型系统中跟踪共享的可变状态，将栈中并行部分的数据竞争转化为编译时错误。 托管载荷模块上的热路径是CCSDS分发：每个CFDP段、每个COP-1帧、每个摄像头数据包在有效载荷到达应用逻辑之前，都会经过空间数据包头部解码和基于APID的路由步骤。每次过境时具有硬调度截止期限的实时板载分发正是EU ORCHIDE (https://orchide-project.eu/) Horizon Europe项目旨在解决的问题（这个联合体中的板载工作最初在Tarides (https://tarides.com/)内部开始，最终导致我们分拆出Parsimoni (https://parsimoni.co/)作为专门的太空软件公司）。 显示CCSDS数据包分发延迟平均、p99、p99.9和最大值的柱状图，对比标准OCaml 5.3.0和OxCaml 5.2.0+ox（使用栈绑定分配）。在p99.9处：标准OCaml 29 ns，OxCaml栈9 ns。标准OCaml在2500万个数据包上触发了394次minor GC；OxCaml栈触发了零次。每数据包延迟在CCSDS分发热路径上：将空间数据包头解码为一个3字段记录并按APID路由。标准OCaml与使用`exclave_stack_`注解的相同代码的OxCaml对比。在笔记本电脑上测量，而非飞行模块。 切换到使用`exclave_stack_`注解的OxCaml，将分发热路径上的p99.9延迟从**29 ns降至9 ns每数据包**，并完全消除了GC压力（**2500万个数据包上从394次minor GC降至零次**）。吞吐量相当；优势在于抖动，而在一个抖动预算仅为数百微秒的托管载荷模块上，这关乎全局。 方法是机械性的：将每次迭代的堆分配（`{ apid; seq_count; data_len }`）改为栈分配（`exclave_stack_ { apid; seq_count; data_len }`），并要求消费者使用`@ local`接受。类型系统证明该记录无法逃逸分发作用域；编译器不发出堆流量；GC无需回收任何东西。 **设置。** Apple M5 Max，macOS 25.4。标准OCaml 5.3.0对比5.2.0+ox（Jane Street的OxCaml分支）。工作负载：100,000批，每批256次CCSDS空间数据包头分发（总计约2560万个数据包），每次通过一个`[@inline never]`处理程序路由，以便记录真正逃逸。10次运行的中位数。 ## 为什么选择OCaml 大约70%的C/C++代码库中的严重CVE可追溯到内存损坏（缓冲区溢出、释放后使用、整数溢出），基于Microsoft的MSRC分析 (2019) (https://github.com/microsoft/MSRC-Security-Research/blob/master/presentations/2019_02_BlueHatIL/2019_01%20-%20BlueHatIL%20-%20Trends%2C%20challenge%2C%20and%20shifts%20in%20software%20vulnerability%20mitigation.pdf) 和Chromium的2020年研究 (https://www.chromium.org/Home/chromium-security/memory-safety/)。我们的安全扩展（SDLS、BPSec和OTAR）都处理密文和密钥材料，这正是内存错误危害最大的地方。该领域中基于C的既有实现，NASA CryptoLib (https://github.com/nasa/CryptoLib)，也有过自身这样的错误：例如，TC帧解析器中的堆缓冲区溢出 (https://github.com/nasa/CryptoLib/security/advisories/GHSA-q2pc-c3jx-3852)，由精心构造的帧上的整数下溢触发。OCaml实现从应用逻辑中通过构造消除了此类攻击面。运行时、底层内核和引导加载程序仍然是C，仍然在TCB中：内存安全在其发挥作用的地方提供帮助，但不能替代可信计算基审计。 除了OCaml目前提供给我们的，语言本身也在不断进步。Jane Street (https://oxcaml.org/)维护着OxCaml，这是一个OCaml的实验性分支。其设计目标是对程序中性能关键部分进行安全、可预测的控制，仅在需要时选择性加入，并且仍然是OCaml：每个有效的OCaml程序也是有效的OxCaml程序。OxCaml Labs (https://anil.recoil.org/projects/oxcaml)（Anil Madhavapeddy在剑桥的团队）和FP Launchpad (https://fplaunchpad.org/)（KC Sivaramakrishnan在IIT Madras的实验室）正在推动**OCaml**向前发展；Tarides (https://tarides.com/blog/2025-07-09-introducing-jane-street-s-oxcaml-branch/)将准备就绪的部分上游合并到主线。 我不知怎么就专注于登月了 :-) 先进入轨道意味着将正确性优先于性能，因为轨道上的协议错误修复成本高昂。防御贯穿协议栈的每一层：类型检查、形式验证的加密原语（libcrux (https://github.com/cryspen/libcrux)、fiat-crypto (https://github.com/mit-plv/fiat-crypto)）、互操作性测试和依赖审计 (https://hacksat.dev/)。 以其中三层作为具体例子。线格式编解码器从类型化模式生成，在解码时拒绝格式错误的字节，并馈送给Microsoft的EverParse (https://project-everest.github.io/everparse/)解析器生成器，该生成器生成用F\* (https://fstar-lang.org/)形式验证过的C验证器。协议状态机编码为GADT (https://ocaml.org/manual/5.3/gadts.html)，因此类型检查器在编译时拒绝无效转换。互操作性管道针对现有参考实现运行，捕获类型系统无法表达的问题，并在此过程中暴露上游库中的缺陷。 除了这些层捕获的问题外，函数式核心使我们能够将相同的代码作为飞行软件、地面软件和测试预言机交付。上面的`protect_bundle`在三种角色中都是同一个函数。我们将记录的一个角色的流量馈送到其他角色，并逐字节比较输出。OCaml代码也是其他实现验证的参考实现。这是nqsb-TLS (https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak)方法（Kaloper-Mersinjak, Mehnert, Madhavapeddy and Sewell, USENIX Security 2015），并且在TLS中已经保持了十年。Nitrokey的NetHSM (https://www.nitrokey.com/products/nethsm)今天在其发货的硬件安全模块中运行着相同的OCaml TLS栈。 Borealis也不例外。看起来我们好像用几个月时间从零开始编写了一个完整的CCSDS协议栈并进行了轨道演示。但事实并非如此。核心库来自MirageOS (https://mirageos.org/)，并且已经在地面生产环境中运行了十年。库操作系统，顾名思义，是一个大型工具集，你可以从中挑选所需的组件。 ASPLOS 2013的unikernel论文 (https://gazagnaire.org/blog/2026-02-23-asplos-unikernels.html)曾询问，密封的、单一用途的镜像能否改善云基础设施。十年后，相同的库在Docker Desktop (https://gazagnaire.org/blog/2026-04-23-docker-story.html)上运行于数亿台笔记本电脑中。现在它们运行在太空中，在ClusterGate-2上，作为Linux进程而非unikernel进行系统级管道操作，这在我最初设计它们时未曾预料。 Borealis是在轨道上的一个二进制文件。**下一个问题是规模：** 部署和管理横跨多颗卫星的专用有效载荷二进制文件舰队，要像当初Docker在Linux上带来的一键式便捷那样。更困难的一半是安全地做到这一点：签名更新、滚动升级以及跨故障域的隔离，所有这些都受到延迟和带宽的限制，没有人为干预。