O(x)Caml in Space: Securing the Final Frontier with Memory Safety

Deploying software to low Earth orbit (LEO) presents a unique set of challenges: extreme environments, limited connectivity, and the high cost of failure. When a bug reaches orbit, you cannot simply SSH into a server and restart a process; kernel patching becomes a complex delivery problem, and a total system crash can mean the loss of a multi-million dollar asset.

Recently, the project codenamed Borealis—a pure-OCaml implementation of the CCSDS protocol stack—successfully booted up inside DPhi Space's ClusterGate-2 payload module. This deployment demonstrates that high-level, memory-safe languages are not just viable for space applications but are essential for securing the next generation of hosted-payload satellites.

The Architecture of Borealis

Borealis operates as a daemon that manages the communication between the ground station and the satellite. While it presents a standard client-server interface for telemetry and commands, the underlying transport is a pure-OCaml implementation of the CCSDS (Consultative Committee for Space Data Systems) protocol family.

Delay-Tolerant Networking

Because the satellite lacks constant network connectivity, Borealis treats the filesystem as a delay-tolerant network. Every command, response, and telemetry sample is serialized into a BPv7 (Bundle Protocol version 7) bundle and written to disk. DPhi's API then forwards these opaque bytes during the next available pass.

The Security Envelope

Security is paramount when running as a tenant on shared hardware. Borealis utilizes BPSec to wrap each bundle in encryption and authentication blocks. This ensures that even if the host's Linux kernel is compromised—a real threat given the prevalence of kernel-level CVEs like "Dirty Frag" or "Copy Fail"—the routing path remains outside the trust path. The satellite operator sees only opaque bytes; they cannot read, modify, or forge the contents.

Post-Quantum Readiness

Looking toward long-term missions (10-15 years), Borealis implements Over-The-Air Rekeying (OTAR) for post-quantum signing keys using ML-DSA-65. This is a critical requirement for NASA's Space System Protection Standard (NASA-STD-1006A). By implementing OTAR, Parsimoni can rotate keys without re-flashing the satellite, marking one of the first public in-orbit demonstrations of post-quantum OTAR.

Performance and the OxCaml Advantage

While OCaml 5 provides safe multi-threading and high performance, the "hot path" of satellite dispatch—where every packet must be decoded and routed—demands minimal jitter. This is where OxCaml, Jane Street's experimental compiler branch, becomes transformative.

Eliminating GC Jitter

In standard OCaml, per-packet allocations typically hit the heap, triggering minor Garbage Collection (GC) cycles. In a high-throughput environment, these cycles introduce latency spikes (jitter) that can compromise hard scheduling deadlines.

By using OxCaml's mode system and exclave_ stack_ annotations, developers can mark allocations as stack-bound. This ensures they never reach the heap and never trigger the GC. The results are stark:

• p99.9 Latency: Dropped from 29 ns to 9 ns per packet.
• GC Pressure: Reduced from 394 minor GCs to zero over 25 million packets.

As noted by community members, this allows developers to enjoy the ergonomics of a GC-based language by default, while opting into manual-like memory control only where performance is critical.

Why OCaml for Space?

Historically, space software has been dominated by C and C++, but these languages carry a heavy burden of memory corruption vulnerabilities. Microsoft and Chromium studies suggest that roughly 70% of severe CVEs stem from memory safety issues. In the space domain, this is evidenced by bugs like the heap buffer overflow found in the NASA CryptoLib TC frame parser.

OCaml eliminates this entire class of attack surface by construction. To further ensure correctness, Borealis employs a multi-layered defense:

1. Formal Verification: Using libcrux and fiat-crypto for cryptographic primitives.
2. Typed Schemas: Wire-format codecs are generated from typed schemas and validated via Microsoft's EverParse.
3. Type-Driven State Machines: Protocol states are encoded as GADTs, allowing the compiler to reject invalid transitions at compile time.

The Path Forward: Scaling the Fleet

Borealis is more than a single binary in orbit; it is a proof of concept for a new way of building space software. The project leverages libraries from MirageOS, proving that the same toolset used for cloud unikernels a decade ago is equally potent for satellite payload plumbing.

The next challenge is scale. As hardware becomes routine, the focus shifts to the software stack: managing fleets of specialized payload binaries with the same ease as Docker manages Linux containers on the ground. This involves creating secure, signed update paths and robust isolation between multiple tenants on a single satellite bus.

By combining the mathematical rigor of ML with the performance optimizations of OxCaml, Parsimoni is demonstrating that the "final frontier" can be both safe and performant.