ハクソク

世界を動かす技術を、日本語で。

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

11時間前原文(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のユニカーネル作業と合うなって思うようになった。地上では、セキュリティや専門性を問題にするために、もっとマシン（またはお金）を投げ入れることでごまかせるけど、軌道上ではそうはいかないから、コンパイル時とランタイムの保証がしっかりしてないといけないんだよね！

└

今はRustを使わない理由はほとんどないし、処理側とペイロードソフトウェアの両方をカバーできる。でも、みんなC/C++を使い続けるんだよね。請求書を出せるならそれでもいいけど。OCamlを使い続ける理由は、人気がないこと以外に何かある？人気や認知度が問題じゃなければ、OCamlの開発サイクルは、Pythonが許可されているプラットフォームでRustと比べていくつかの点で良いと思う（限られたメモリのLinuxシステムを「組み込み」とは呼ばないけど）。

└

認証の問題を除けば、文化の問題だと思う。だからこそ、Rustの主要なドメインは、技術的な理由で自動リソース管理ができない環境や（君の言うように）人々の信念を変えるのが無駄だと思うところだと見てる。プレゼンテーションありがとう。

最近驚いたのは、エージェントがOCaml 5+やOxCamlのコードを生成するのがすごく得意なこと。トレーニングデータにはあまりないけどね。OxCamlの強い型とモードは、エージェントを導くための素晴らしいテスト可能なオラクルとして機能してるみたい。OCaml 5とOxCamlに基づいた並行プログラミングのコースを教えたんだけど、教材のほとんどのコードはエージェントが書いたものだった。50人以上の学生に教えてたから、全てのコードをレビューしたけど、正直言ってエージェントが書くO(x)Camlの方が（ほとんど）自分より上手いよ。

└

実は、私もほとんどのOxCamlのアノテーションにエージェントを使っていることを告白します：https://github.com/avsm/ocaml-claude-marketplace/tree/main/p... アノテーションはプログラムのパフォーマンス特性を変えるだけなので、あまりデメリットはないですよ。静的型システムが不整合なアノテーションを拒否しますし。

└

LLMにはHindley-Milnerベースの言語に関する奇妙な機能が組み込まれてるんだよね。新しい言語、例えばGleamやNanolangでも自動的に上手く扱える。俺がどこにも公開してない趣味のMLはLuaにコンパイルできるんだけど、コーディングモデルがそれをうまく書けるんだ。PythonやPHPよりも確実に上手いよ。あっちの方がトレーニングデータには大量にあるのにね。なんでこうなるのか全然わからないけど、今はこの理由で助けてもらいながらコーディングしてる。

HNでは今、Rust対Zigが熱いね。OxCamlはその両方の代替として考えられるべきだと思う。Rustの主張は安全性で、Zigは使いやすさだけど、OxCamlは安全性と使いやすさを両立できることを示してる。自分がちょっといじってみた感じでは[1]、すごく使いやすかったよ。[1]: https://noelwelsh.com/posts/a-quick-introduction-to-oxcaml/

└

OxCamlは、GoやJS/Typescript、Java/.NETエコシステムに対する競争相手って感じだね。この言語たちよりも、むしろそっちの方が近い。しかも、これは一時的な取り組みで、最終的には上流のOCamlにフィードバックされる予定なんだ。

└

ゼロックスはドロドでCedarを使ってそれを証明したし、Interlisp-Dも同様に、多くの他のプロジェクトもそうだったよ。http://toastytech.com/guis/cedar.html https://interlisp.org/ 残念ながら、そういう試みは技術的な理由ではなく、人間的な理由で失敗しちゃうんだよね。

KCは彼のトークを終える際に、OCaml 5.0がその言語機能のおかげでC/Rustのようなパフォーマンスを発揮して月に行くかもしれないと推測しました。 それはかなりの肯定ですね！OCamlがそこに行くのを見てみたいです。

└

OxCamlを見てみないといけませんね。「Cのような」パフォーマンスの主張にはちょっと警戒しています。Javaが30年以上の開発を経ても同じような主張を果たせなかったからです... 実際に達成したのは、巨大なヒープを与えればCの約50%のパフォーマンスです。Rustは深く埋め込まれた作業に非常に適していて、実際にC/C++レベルのパフォーマンスを持っています。AIのコーディングアシスタンスがあれば、Rustはますます手が届きやすくなりますし、もちろんプロセッサの速度向上やコンパイラの改善が時間とともにコンパイル速度の問題を解決してくれるでしょう。とはいえ、ML構文を持つ速くて安全な言語には何の問題もありません！(この中でのダークホースはMojoで、Rustレベルの安全性を持ちながら、より使いやすい言語と、はるかに速いコンパイラを提供するかもしれません...)

多くのガーベジコレクション言語には、クラスを最小限に抑えたり、スタックにもっと多くのものを押し込むことでGCの圧力を減らす方法があることを知っています。Javaのような言語が最初に大量のメモリを割り当てて、その後高頻度取引のシナリオで一日中ガーベジコレクタをオフにするという話も聞いたことがあります。この状況に一度も遭遇したことがないので、ガーベジコレクション言語を非ガーベジコレクション言語のように振る舞わせるのはどれくらい難しいのか気になります。

└

GCオブジェクトと非GCオブジェクトがシームレスに相互作用するのはいつも難しいですね。GCオブジェクトのファイナライザが非GCデータをドロップできるようにしたり、非GCオブジェクトが参照するかもしれないGCオブジェクトを一時的なルートとして登録できるようにしたり、GCトレースパスがそれらが参照しているものを発見できるようにする必要があります。そして、非GCオブジェクトをサイクルに関与させることはできず、きちんと自己完結したリーフ状またはツリー状のセクションである必要があります。

└

その言語が値型とスタック割り当てをサポートしてるかどうかによるね。多くのGC言語はそうしてる。難しいのは、その違いが型システムの一部になってるから、値型と参照型の間でコードを移動させるときにリファクタリングが必要になること。

RustにはOCaml 5のような代数的効果システムが必要だとずっと思っていましたが、両方を使ったことがある人は、さまざまなユースケースでどれだけうまく機能するか比較したことはありますか？RustはもちろんOxCamlよりも成熟していますが、Jane Streetにとって十分なら...

信頼性重視の言語については詳しくないけど、私が知っている限りでは、Ada、Rust、Haskellが一番目立っているね。OCamlがこれらの選択肢よりも良い選択肢になった理由は何なの？

└

（投稿者）やあ、Maksadbek！いい質問だね。これは、書く速さと自分が書いたものへの信頼のトレードオフなんだ。OCaml（特にOxCaml）は、そのカーブ上で本当に良いポイントに位置してる。Ada/SPARKは最強の検証ストーリーと数十年の宇宙の実績があるけど、開発コストが高いんだよね。Rustも使えるけど、私はデフォルトでGCが欲しいし、ホットパスではオフにできるオプションが欲しい。それがまさにOxCamlのモードシステムが提供しているもので、投稿のディスパッチループではマイナーGCがゼロで、他はGC管理されてるんだ。Haskellは型駆動設計には最適だけど、ランタイムコストモデルが低ジッターの作業には難しいんだよね。それに、OCamlエコシステムは両方の面でしっかりした基盤を提供してくれた。プロトコルスタックについては、MirageOSスタイルのクリーンな分離があって、ワイヤーシリアライゼーション、純粋な状態マシン管理、I/Oがあって、MLモジュールやGADTsがプロトコル状態マシンに自然にマッピングされるんだ。暗号については、OCaml向けのプリミティブにはmirage-crypto（楕円曲線の下のfiat-crypto）を使って、ポスト量子署名にはlibcruxを使ってる。CCSDSやBPv7/BPSecのレイヤーは自分でゼロから書かなきゃいけなかった（以前の投稿でその過程を説明してるよ）、20年のOCamlの筋肉記憶が確実に役立った！

クラスタゲート2サーバーがどこにあるか見たい人はここだよ: https://spacebook.com/explorer?scene=8451c006-9e1a-4943-8202...