242 points • 4 days ago • Article Link

2026 年 4 月 23 日，一个纯 OCaml 实现的 CCSDS（Consultative Committee for Space Data Systems）协议栈，代号为 Borealis，在 DPhi Space 的 ClusterGate-2 载荷模块中成功在低地球轨道启动。该项目由 Parsimoni 开发，实现了端到端加密的命令与控制以及后量子密钥轮换，全部用安全的 OCaml 编写。这一里程碑是历经十年工程攻关、为 OCaml 5 带来安全且高性能多线程能力的成果；Parsimoni 团队把曾被戏言"会到达月球"的设想字面化，将协议栈部署到一颗每 90 分钟绕地球一圈的卫星上。

Borealis 作为守护进程运行在 Arm SoC（四核 Cortex-A53 、 4 GB RAM）的托管载荷环境中。由于卫星没有直接的网络连接，系统采用延迟容忍网络模型，命令和遥测被序列化为 BPv7（Bundle Protocol version 7）包并写入文件系统，DPhi Space 的 API 在卫星过境时转发这些文件。为保障共享硬件上的安全——以防像 "Dirty Frag" 或 "Copy Fail" 之类的内核级漏洞破坏租户隔离——每个数据包都被封装在 BPSec（Bundle Protocol Security）扩展块中。这个加密信封对有效载荷进行加密和认证，确保即便底层 Linux 内核被攻破，卫星运营方或其他租户也无法读取、篡改或伪造内容。

系统还实现了 OTAR（Over-The-Air Rekeying）用于后量子签名密钥 ML-DSA-65，设计以覆盖卫星的 10 到 15 年寿命，允许运营方在无需物理重刷硬件的情况下进行密钥轮换。当前飞行循环在接收新密钥时即刻激活，但协议也支持更保守的地面驱动激活步骤，允许运营方在提交前验证安装。值得注意的是，一旦卫星在轨，主密钥并无轮换路径——在缺乏硬件安全元件（如 TPM）的长期任务中，这是一种现实存在的失败模式。

为提升性能，团队正在引入 OxCaml（Jane Street 的 OCaml 编译器分支）。通过使用 `exclave_ stack_` 注解将分配标记为栈绑定，开发者可以在热路径上消除垃圾回收压力。在一项涉及 2500 万个 CCSDS 包调度的基准测试中，该方法将单包 p99.9 延迟从 29 ns 降至 9 ns，并完全消除了 394 次次要 GC 。这种抖动的减少对具有严格调度截止的实时机载调度至关重要——这是欧盟 ORCHIDE Horizon Europe 项目的核心负载之一。

选择 OCaml 源于对数学严谨性与内存安全的需求：在该领域，C/C++ 的内存损坏约占严重 CVE 的 70% 。采用 OCaml 可消除一整类攻击面，例如在现有 C 库（如 NASA CryptoLib）中常见的堆缓冲区溢出。开发流程采用"纵深防御"策略：针对传输格式使用类型化 schema 、用 GADTs（Generalized Algebraic Data Types）在编译时强制有效的协议状态转换，并与参考实现做互操作测试。这遵循 nqsb-TLS 的做法：同一段代码既可作为飞行软件、地面软件，又可作为测试判定器，从而实现跨角色的逐字节比对。

Borealis 协议栈建立在为期十年的 MirageOS 生产级库之上，MirageOS 最初为云 unikernel 设计。尽管当前部署以 Linux 进程形式运行，而非 unikernel，但它展示了这些函数式系统的适用性。 Parsimoni 的下一个挑战是将该方案扩展到卫星编队，重点包括安全部署、签名更新、载荷隔离和认证。随着把硬件送入轨道变得常态化，行业中最有趣的问题正逐步转向软件层面，这与云计算的发展轨迹相呼应——最终，堆栈比服务器本身更重要。 On April 23, 2026, a pure-OCaml implementation of the CCSDS (Consultative Committee for Space Data Systems) protocol stack, codenamed Borealis, successfully booted in low Earth orbit aboard DPhi Space's ClusterGate-2 payload module. Developed by Parsimoni, the project features end-to-end encrypted command and control with post-quantum key rotation, all written in safe OCaml. This milestone follows a decade-long engineering effort to bring safe, performant multi-threading to OCaml 5, which its creators speculated would eventually reach the moon. The team at Parsimoni took that vision literally, deploying the stack on a satellite that circles the Earth every ninety minutes.

Borealis functions as a daemon running on an Arm SoC (four Cortex-A53 cores, 4 GB RAM) within a hosted-payload environment. Because the satellite lacks direct network connectivity, the system uses a delay-tolerant network model where commands and telemetry are serialized into BPv7 (Bundle Protocol version 7) bundles and written to a filesystem. DPhi Space's API then forwards these files during orbital passes. To ensure security on shared hardware where kernel-level vulnerabilities like "Dirty Frag" or "Copy Fail" could break tenant boundaries, every bundle is wrapped in BPSec (Bundle Protocol Security) extension blocks. This cryptographic envelope encrypts and authenticates the payload, ensuring that even if the underlying Linux kernel is compromised, the satellite operator or other tenants cannot read, modify, or forge the contents.

The system also implements OTAR (Over-The-Air Rekeying) for post-quantum signing keys (ML-DSA-65), designed to last the 10-to-15-year lifespan of the satellite. This allows operators to rotate keys without physically re-flashing the hardware. While the current flight loop activates new keys upon receipt, the protocol supports a more cautious ground-driven activation step where operators verify the installation before committing. The master key, however, has no rotation path once the satellite is in orbit, representing an honest failure mode for long missions lacking hardware-backed secure elements like TPMs.

Looking toward performance optimization, the team is integrating OxCaml, Jane Street's compiler branch for OCaml. By using `exclave_ stack_` annotations to mark allocations as stack-bound, developers can eliminate garbage collection pressure on the hot path. In benchmarks involving 25 million CCSDS packet dispatches, this approach reduced p99.9 latency from 29 ns to 9 ns per packet and eliminated 394 minor GCs entirely. This reduction in jitter is critical for real-time on-board dispatch with hard scheduling deadlines, a workload central to the EU's ORCHIDE Horizon Europe project.

The choice of OCaml is driven by the need for mathematical rigor and memory safety in a domain where C/C++ memory corruption accounts for roughly 70% of severe CVEs. By using OCaml, the team removes entire classes of attack surfaces, such as the heap buffer overflows found in incumbent C-based libraries like NASA CryptoLib. The development process relies on a "defense in depth" strategy: typed schemas for wire formats, GADTs (Generalized Algebraic Data Types) to enforce valid protocol state transitions at compile time, and interop testing against reference implementations. This follows the nqsb-TLS approach, where the same code serves as flight software, ground software, and a test oracle, allowing for byte-for-byte comparison across roles.

The Borealis stack is built on a decade of production-tested libraries from MirageOS, originally designed for cloud unikernels. While the current deployment runs as a Linux process rather than a unikernel, it demonstrates the versatility of these functional systems. The next challenge for Parsimoni is scaling this to a fleet of satellites, focusing on safe deployment, signed updates, payload isolation, and attestation. As launching hardware into orbit becomes routine, the industry's most interesting problems are shifting to the software layer, mirroring the evolution of cloud computing where the stack eventually mattered more than the servers.