O(x)Camlの宇宙における応用

2026年5月15日原文(gazagnaire.org)

概要

2024年4月23日、純OCaml製CCSDSプロトコルスタック「Borealis」が地球低軌道で稼働開始
BorealisはDPhi SpaceのClusterGate-2ペイロードモジュール内で運用、全通信はエンドツーエンド暗号化・ポスト量子鍵ローテーション対応
OCaml採用理由は「安全性」と「高性能マルチスレッド対応（OCaml 5）」による宇宙空間での信頼性確保
ホスト衛星は複数テナント環境、Linuxカーネル脆弱性の影響を最小化するため暗号層で防御
今後はJane StreetのOxCaml導入でリアルタイム処理性能・安全性をさらに強化予定

Borealis：純OCaml製CCSDSプロトコルスタックの宇宙実証

Borealis は、 OCaml のみで実装された CCSDSプロトコルスタック の宇宙実証プロジェクト
DPhi Space の ClusterGate-2 ペイロードモジュール上で運用
地上との通信は ファイルシステム経由の遅延耐性ネットワーク として実装
- uplinkディレクトリへのファイル書き込みで地上→衛星通信
- downlinkも同様にファイル転送
BPv7バンドル 形式で全データをシリアライズし、 BPSec で暗号化・認証
- リプレイ攻撃防止のシーケンス番号、 OTARによるポスト量子鍵ローテーション 対応
マルチテナント衛星環境 での「他テナント・運用者からの完全な秘匿性・完全性確保」
- ルーティング経路上のいかなる第三者もデータ内容を解読・改竄・偽造不可

セキュリティ設計とOCaml採用理由

衛星上では カーネル脆弱性（Dirty Pipe, Fragnesia, Copy Fail等） によりコンテナ分離が破られるリスク
- 再起動やパッチ適用が困難な宇宙空間 では、アプリケーション層での暗号化が唯一の防御策
SDLS/BPSec/OTAR などのセキュリティ機能を メモリ安全なOCaml で実装
- C/C++由来の深刻なCVEの約70%が メモリ破壊 によるもの（MSRC/Chromium調査）
- NASA CryptoLibなど従来C実装にもバッファオーバーフロー等の脆弱性事例
型システム や GADT による状態遷移の静的検証、 EverParse/F *による形式手法パーサ生成
地上/衛星/テストオラクル で同一コードを利用し、相互検証・参照実装としても機能

Borealisの運用構成

Daemonプロセス として地上・衛星双方で動作
- テレメトリ取得、コマンド受信・実行、OTAR鍵更新処理
コマンド種別 （Ping, Check, Capture, Halt）はADTとして定義、型安全な分岐実装
- 新コマンド追加時はコンパイラが未対応箇所を検出
OTAR鍵更新 はバイナリペイロードで暗号化、衛星内で復号・ステージング・アクティベート
- マスター鍵は事前書き込みのみ、ローテーション不可（紛失時は回復不能）

OxCaml導入による性能・安全性強化

OxCaml （Jane Street開発）はOCaml上位互換のコンパイラブランチ
- ローカリティ でヒープ未使用のスタック割当明示
- ユニークネス・ケイパビリティ で並列処理時のデータ競合を型システムで検出
CCSDSディスパッチのリアルタイム処理 で、GC圧力ゼロ・ジッター大幅低減
- exclave_ stack_注釈付与でp99.9レイテンシー29ns→9ns、GC回数394→0（2500万パケット処理時）
EU ORCHIDEプロジェクト 等でのリアルタイム宇宙ソフト基盤開発経緯

OCamlの今後とBorealisの意義

OxCaml Labs（ケンブリッジ）・FP Launchpad（IIT Madras）・Tarides がOCaml進化を牽引
宇宙向けソフトウェア開発で 正しさを最優先、多層防御（型検査・形式手法・相互運用テスト）
Borealis は「安全かつ高信頼な宇宙ソフトウェア」の新たな実用モデル
- 今後の ポスト量子OTARの軌道上デモ、 OxCaml適用によるさらなる性能向上 計画

Hackerたちの意見

ここでの大きな勝利は、デフォルトでGC（ガーベジコレクション）があることで、型注釈を追加するだけでヒープの割り当てを減らせることだね。exclave_ stack_ 注釈を使ってOxCamlに切り替えると、ディスパッチのホットパスでのp99.9のレイテンシが29nsから9nsに減って、GCの負荷が完全になくなるんだ（2500万パケット中394回のマイナーGCがゼロに）。スループットも同じくらいだし [...] 数ヶ月前に自分の「httpz」スタックでも似たような結果が出たよ（https://anil.recoil.org/notes/oxcaml-httpz）、それを使ってる自分のウェブサイトも特に問題なく動いてる。OxCamlは最先端の拡張が詰まってる割には驚くほど堅牢なコンパイラだと思う。自分のインフラでのクラッシュはコンパイラのバグによるものは一度もないし（悪いOCamlコードはたくさんあるけど、コンパイルバグではない）。

└

堅牢性は、Jane Streetで使われているプロダクションコンパイラだから助けられてると思うよ。

└

Nimも同じようなことをやってるね。スタックを優先して、動的ヒープ型をデフォルトで値セマンティックなユニークポインタでラップして、できるだけ暗黙のコピーを避けてる。長期的には、コンパイル言語がスタック管理の方向に進むのが見えるかも。

└

GCされたエコシステムがコードのスタック割り当てをもっと許可するようになってきているのを見るのは面白いね。dotnetがCore 2.1以降、またはSpanやMemoryを導入してパフォーマンス向上を図っているのを追うのは楽しい。GCされた言語は、必要なところだけにガーベジを保持すれば遅くならないんだよね（または一度割り当てて二度と収集しないところで）。

└

そうそう、PTCやAicasが埋め込みJavaツールチェーンでリアルタイムGCを提供してるのと同じように、microEJやOberonのAstrobe、マイクロカーネルと.NETのMeadowもやってるよね。人々が「これがいつもそうだった」って抵抗することで、考え方が変わるだけなんだ。OCamlの改善も見れて嬉しい。俺の最初のMLはCaml Lightだったから。

CCSDSはすべてをゼロから再発明させようとするけど、このスタックを実装する時にメモリの安全性が一番の攻撃面になるとは思えないな。大手が衛星のネットワーキングをどう実装してるのかは知らないけど、個人的にはデータ暗号化を再発明するよりも、TLSのような既存で実績のあるものを使う方がいいと思う。あの文書を見てみてよ： https://www.google.com/search?client=firefox-b-lm&q=ccsds+en...

└

ここでのTL;DR（https://ccsds.org/Pubs/350x9g2.pdf）は「AES GCM」みたいだけど、古い衛星のせいでレガシープロトコルがたくさんあるね。最近だとDTLSやHTTP3の方がいい選択肢かも。

└

（投稿者）やあ、dsab！同意するけど、CCSDSは今のところ私たちが持っているものなんだ。もし拡張したり移行したりしたいなら、まずはしっかりサポートする必要がある。特にSDLS部分の全体スタックの良いオープンソース実装がないのも、移行をさらに難しくしてるんだ。型安全の面では、型付きコンビネーターがパースやシリアライズを説明するのにすごく役立った（以前の投稿を見てね[1]）。プロトコルロジックをI/Oから分けて純粋に保つことで、全体がテストや推論しやすくなるんだ。OCamlのファジングサポートも型と相性がいいしね。これは基本的にnqsb-TLSアプローチ[2]で、ocaml-tlsでは10年間持ちこたえてるよ。 [1] https://gazagnaire.org/blog/2026-03-31-ocaml-wire.html [2] https://www.usenix.org/conference/usenixsecurity15/technical...

実は、2016年にGHGSat-Dの低軌道にOCamlを載せた最初の人間かもしれない。ペイロードソフトウェアは、DBusを介して通信するSystemDサービスの集合体として設計したんだ。それにはプラットフォームと話すためのCCSDS-to-DBusブリッジも含まれてた（ペイロードをホストして、衛星を制御・操縦するもの）。ペイロードは、規制に従って結果データの対称鍵暗号化も行ってた。パリのOCamlユーザーグループでペイロードソフトウェアについて講演したこともある。あのアーキテクチャを選んだ理由は、自分一人でペイロードソフトウェアを全部書くとは思ってなかったし、他の開発者が参加した時に、変な言語（OCaml）を使いたがらないだろうから、彼らはC/C++などで自分の部分を書けるだろうと思ったから。もちろん、そんなことは起こらなかったけど。会社がまだOCamlを使ってるとは思えないな、業界標準の問題を解決するために「業界標準」の言語に戻るのが普通だから。全ての処理とシミュレーションツールチェーンもOCamlで書かれてた。今はRustを使わない理由がほとんどないし、処理側とペイロードソフトウェアの両方をカバーできる。だけど、みんなC/C++を使いたがるんだよね。それでも請求書を出せるなら全然OK。追記：スライド見つけたよ https://lambda-diode.com/static/data/GHGSat_OCaml.pdf

└

あなたのトークのリンクはありますか？GHGの測定をしたのか、それともコントロールスタックの一部だったのかも気になります。私たちは2004年にOCamlでXenServerスタックを書いて、2017年にそれが軌道に乗ったと思います（たぶん、そうだったはず：https://www.theregister.com/offbeat/2017/05/12/space-upstart...）。

└

あ、こんにちはBerké。GHGSatコンステレーションのペイロードソフトウェアはまだほとんどOCamlですが、限られた新しいコンポーネントは確かにRustで作られています。今16基の衛星でうまく動いていますが、あなたが言ったように、主な課題は開発者をOCamlに訓練することでした。今新しいコードをOCamlで書くとは思えません。

└

（投稿者）やあ、Berké！君のトークをすごくよく覚えてるよ（その場にいたからね）。めっちゃ面白くて、この分野について考えさせられた！それ以来、調べれば調べるほど、MirageOSのユニカーネル作業と合うなって思うようになった。地上では、セキュリティや専門性を問題にするために、もっとマシン（またはお金）を投げ入れることでごまかせるけど、軌道上ではそうはいかないから、コンパイル時とランタイムの保証がしっかりしてないといけないんだよね！

Hacker Newsで議論の続きを見る

ハクソク