O(x)Caml in Space: メモリ安全性で最終フロンティアを保護

Borealis のアーキテクチャ

Borealis はデーモンとして動作し、地上局と衛星間の通信を管理します。テレメトリやコマンド用の標準的なクライアント‑サーバーインターフェースを提供する一方で、基盤となるトランスポートは純粋な OCaml 実装の CCSDS（Consultative Committee for Space Data Systems）プロトコルファミリです。

遅延耐性ネットワーキング

衛星は常時ネットワーク接続がないため、Borealis はファイルシステムを遅延耐性ネットワークとして扱います。すべてのコマンド、レスポンス、テレメトリサンプルは BPv7（Bundle Protocol version 7）バンドルにシリアライズされ、ディスクに書き込まれます。DPhi の API が次に利用可能なパス時にこれらの不透明なバイトを転送します。

セキュリティエンベロープ

共有ハードウェア上でテナントとして実行する場合、セキュリティは最重要です。Borealis は BPSec を利用して各バンドルを暗号化および認証ブロックでラップします。これにより、ホストの Linux カーネルが侵害された場合でも（「Dirty Frag」や「Copy Fail」などのカーネルレベル CVE が多発していることから現実的な脅威です）、ルーティング経路は信頼経路の外側に保たれます。衛星オペレーターは不透明なバイトしか見えず、内容を読み取ったり、変更したり、偽造したりできません。

ポスト量子対応

10〜15 年の長期ミッションを見据えて、Borealis は ML-DSA-65 を用いたポスト量子署名鍵の Over-The-Air Rekeying（OTAR）を実装しています。これは NASA の Space System Protection Standard（NASA-STD-1006A）の重要な要件です。OTAR を実装することで、Parsimoni は衛星を再フラッシュせずに鍵をローテーションでき、ポスト量子 OTAR の最初の公開軌道実証の一つとなります。

パフォーマンスと OxCaml の利点

OCaml 5 が安全なマルチスレッドと高性能を提供する一方で、衛星ディスパッチの「ホットパス」――すべてのパケットをデコードしルーティングしなければならない部分――は最小限のジッターを要求します。ここで OxCaml（Jane Street の実験的コンパイラブランチ）が変革的な役割を果たします。

GC ジッターの除去

標準的な OCaml では、パケットごとの割り当ては通常ヒープに行き、マイナー ガーベジコレクション（GC）サイクルをトリガーします。高スループット環境では、これらのサイクルがレイテンシスパイク（ジッター）を引き起こし、ハードなスケジューリング期限を危うくします。

OxCaml のモードシステムと exclave_ stack_ アノテーションを使用することで、開発者は割り当てをスタックバウンドとしてマークできます。これによりヒープに到達せず、GC をトリガーしません。その結果は顕著です：

  • p99.9 レイテンシ: パケットあたり 29 ns から 9 ns に低下。
  • GC プレッシャー: 2,500 万パケットで 394 回のマイナー GC からゼロに削減。

コミュニティメンバーが指摘するように、これにより開発者はデフォルトで GC ベース言語の使いやすさを享受しつつ、パフォーマンスが重要な箇所だけで手動に近いメモリ制御を選択できます。

なぜ宇宙に OCaml を使うのか？

歴史的に、宇宙ソフトウェアは C と C++ が支配してきましたが、これらの言語はメモリ破壊脆弱性という重い負担を抱えています。Microsoft と Chromium の調査によると、深刻な CVE の約 70% がメモリ安全性の問題に起因しています。宇宙分野でも、NASA CryptoLib の TC フレームパーサで見つかったヒープバッファオーバーフローなどのバグがその証拠です。

OCaml は構造上この全ての攻撃面を排除します。正確性をさらに保証するために、Borealis は多層防御を採用しています：

  1. 形式的検証: 暗号プリミティブに libcrux と fiat-crypto を使用。
  2. 型付きスキーマ: ワイヤフォーマットコーデックは型付きスキーマから生成され、Microsoft の EverParse で検証されます。
  3. 型駆動状態機械: プロトコル状態は GADT としてエンコードされ、コンパイラがコンパイル時に無効な遷移を拒否できるようにします。

今後の道筋：フリートのスケーリング

Borealis は軌道上の単一バイナリにとどまらず、宇宙ソフトウェアを構築する新たな方法の概念実証です。このプロジェクトは MirageOS のライブラリを活用し、10 年前にクラウドユニカーネルで使用されたツールセットが衛星ペイロードの配管にも同様に有効であることを示しています。

次の課題はスケールです。ハードウェアが日常化するにつれ、焦点はソフトウェアスタックへ移ります：Docker が地上で Linux コンテナを管理するのと同様の容易さで、専門化されたペイロードバイナリのフリートを管理することです。これには安全で署名された更新パスの作成と、単一衛星バス上の複数テナント間の堅牢な分離が含まれます。

ML の数学的厳密性と OxCaml のパフォーマンス最適化を組み合わせることで、Parsimoni は「最終フロンティア」が安全でありながら高性能であることを示しています。

Sources