太空中的 O(x)Caml

Thomas Gazagnaire 构建从云到轨道的功能系统。 thomas@gazagnaire.org O(x)Caml 进入太空 2026-05-14 #unikernels #ocaml #space 4 月 23 日，我们的纯 OCaml CCSDS 协议栈在近地轨道启动！该项目代号 Borealis，在主卫星上的 DPhi Space 的 ClusterGate-2 有效载荷模块内运行，具有端到端加密的命令和控制以及后量子密钥轮换，所有这些都在安全的 OCaml 中实现。为什么 OCaml 在这里很重要？在卫星上运行的不受信任的代码存在巨大的安全风险，而 OCaml 是在太空中运行的理想安全语言。在 ICFP 2022 主题演讲中，KC Sivaramakrishnan 回顾了 OCaml 5 长达十年的工程工作，该版本将安全且高性能的多线程引入 OCaml 运行时。 KC 在演讲结束时推测 OCaml 5.0 将登上月球，因为它的语言功能可以按需提供类似 C/Rust 的性能，同时保持经典 ML 的数学严谨性。在 Parsimoni，我们对他的话的理解有点过于字面意思了 :-) KC Sivaramakrishnan 的 ICFP 2022 主题演讲的结束幻灯片：从 OCaml 5.0 到月球的箭头，以及赋予这篇文章标题的隐喻。 Borealis 于 2026 年 4 月 23 日首次在 DPhi Space 的任务操作仪表板上启动。纯 OCaml CCSDS 堆栈首次在太空中运行！主卫星大约每九十分钟绕地球一圈。在 Virgile Robles 和我在圣诞节期间破解这个问题几个月后，当我们看到以下内容时，我们（几乎）跳了起来：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 配置：scid=100、tm_vcid=0、tc_vcid=4、tm_spi=1、tc_spi=2、tm_frame_len=1115 2026-04-23 18:48:06 会话密钥：EK=0x0100 AK=0x0101 active 2026-04-23 18:48:09 Telemetry health: { ... "status": "healthy" } 实际运行的 Borealis 是一个守护进程。在地面和卫星上，它都采用正常的客户端-服务器协议（遥测查询、命令和响应、OTAR 重新密钥请求），与任何生产服务器的形状相同。不寻常的是下面的电线。该协议栈是 CCSDS 的纯 OCaml 实现，CCSDS 是连接航天器与地面的协议族。它涵盖了从无线电成帧到捆绑协议以及顶层安全扩展的每一层；二进制格式被描述为 ocaml-wire 编解码器。在 ClusterGate-2 上，仅使用该堆栈的上层。该卫星没有与外部的网络连接。唯一的地面链接是通过 DPhi 的 API 进行文件系统上传和下载：写入上行链路目录的文件由 DPhi 在下一次传递时转发，下行链路的工作方式相同。 Borealis 将该文件系统视为延迟容忍网络。每个命令、响应、遥测样本和图像块都被序列化为 BPv7 包并写入磁盘； DPhi 将文件作为不透明字节转发。 BPSec 将每个包包装在两个扩展块中：一个对有效负载进行加密，另一个对其进行身份验证。序列号拒绝重播，并且预共享密钥（由 OTAR 轮换，如下）使路由路径远离信任路径。卫星运营商只能看到不透明的捆绑字节；路由路径中的任何内容都无法读取、修改、伪造或替换内容。这很重要，因为我们是别人硬件上的租户。在托管有效负载卫星上，多个租户共享一条总线，仅靠容器隔离是不够的。共享 Linux 内核意味着内核级 CVE 会定期打破租户边界，并且相同的原语不断以新形式重新出现：Dirty Frag（今年发布的通用 Linux LPE）、Fragnesia（同一家族的近亲）和“Copy Fail”，这是 4 月底披露的 Linux 内核权限升级，立即影响了每个主要发行版。早期几轮（2022 年的 Dirty Pipe、2024 年用于容器逃逸的 nf_tables use-after-free）表明还会有更多。在地面服务器上，您可以运行包管理器并重新启动；在轨道上，内核补丁本身就是一个交付问题，有其自身的延迟，有时根本不可能。每个捆绑包周围的加密信封是唯一持久的保证。除了保密性和真实性之外，长期任务威胁模型还需要密钥轮换。 Borealis 支持 OTAR（空中重新加密）的后量子签名密钥 (ML-DSA-65)。这些密钥的有效期与卫星的使用寿命相同（十到十五年），这就是为什么 NASA 的空间系统保护标准 (NASA-STD-1006A) 将后量子命令身份验证视为一项要求，而不是未来的选择。 OTAR 让我们可以轮换后量子密钥，而无需重新刷新卫星。据我们所知，这将是后量子 OTAR 的首次公开在轨演示；我们计划在稍后的过程中进行轮换。 Borealis 作为访客运行在 DPhi 的托管有效负载模块上：运行 Linux 的 Arm SoC（四个 Cortex-A53 内核，4 GB RAM）。飞行箱