순수 OCaml로 구현한 CCSDS 프로토콜 스택이 저궤도에서 부팅되었고, Borealis는 안전한 OCaml로 종단간 암호화된 명령·제어와 사후양자 키 교체를 수행하며 위성에서 동작하고 있다.
2026년 4월 23일, 우리의 순수 OCaml CCSDS 프로토콜 스택이 저궤도에서 부팅되었습니다! 코드명 Borealis 인 이 프로젝트는 호스트 위성의 DPhi Space ClusterGate-2 payload module 내부에서 실행되고 있으며, 종단간 암호화된 명령 및 제어와 사후양자 키 교체를 모두 안전한 OCaml로 구현했습니다.
왜 여기서 OCaml이 중요할까요? 위성에서 실행되는 신뢰할 수 없는 코드는 거대한 보안 위험 이며, OCaml은 우주에서 실행하기에 이상적인 안전 언어입니다. 그의 ICFP 2022 keynote 에서 KC Sivaramakrishnan 은 안전하고 성능 좋은 멀티스레딩을 OCaml 런타임에 도입한 릴리스인 OCaml 5를 만들어 낸 10년에 걸친 엔지니어링 노력 을 돌아보았습니다.
KC는 고전적인 ML의 수학적 엄밀함을 유지하면서 필요할 때 C/Rust 수준의 성능을 제공하는 언어 기능 덕분에 OCaml 5.0이 달에 가게 될 것이라고 추측하며 발표를 마무리했습니다. Parsimoni의 우리는 그의 말을 조금 너무 문자 그대로 받아들였습니다 :-)
호스트 위성은 대략 90분마다 지구를 한 바퀴 돕니다. Virgile Robles 와 제가 크리스마스 동안 이 작업을 해킹한 지 몇 달 뒤, 우리는 이것을 보고 (가상으로) 펄쩍 뛰었습니다:
2026-04-23 18:48:06 SpaceOS/Borealis (BPv7, BPSec, OTAR) by Parsimoni
2026-04-23 18:48:06 ClusterGate-2 proxy [single iteration]
2026-04-23 18:48:06 Config: scid=100, tm_vcid=0, tc_vcid=4, tm_spi=1, tc_spi=2, tm_frame_len=1115
2026-04-23 18:48:06 Session keys: EK=0x0100 AK=0x0101 active
2026-04-23 18:48:09 Telemetry health: { ... "status": "healthy" }
Borealis는 데몬입니다. 지상과 위성 양쪽에서, 이것은 일반적인 클라이언트-서버 프로토콜(텔레메트리 질의, 명령과 응답, OTAR 재키 요청)을 말하며, 형태만 보면 어떤 프로덕션 서버와도 같습니다. 특이한 점은 그 아래의 전송 계층입니다.
프로토콜 스택은 우주선을 지상과 연결하는 프로토콜 계열인 CCSDS 의 순수 OCaml 구현입니다. 이는 무선 프레이밍부터 Bundle Protocol과 그 위의 보안 확장까지 모든 계층을 포괄하며, 바이너리 형식은 ocaml-wire 코덱으로 기술됩니다.
ClusterGate-2에서는 이 스택의 상위 계층만 사용됩니다. 위성은 외부에서 접근 가능한 네트워크 연결이 없습니다. 유일한 지상 링크는 DPhi의 API를 통한 파일시스템 업로드와 다운로드입니다. 업링크 디렉터리에 기록된 파일은 다음 패스에서 DPhi에 의해 전달되며, 다운링크도 같은 방식으로 동작합니다. Borealis는 그 파일시스템을 지연 허용 네트워크처럼 취급합니다. 모든 명령, 응답, 텔레메트리 샘플, 이미지 청크는 BPv7 번들로 직렬화되어 디스크에 기록되고, DPhi는 그 파일을 불투명한 바이트열로 전달합니다.
BPSec 은 각 번들을 두 개의 확장 블록으로 감쌉니다. 하나는 페이로드를 암호화하고, 다른 하나는 이를 인증합니다. 시퀀스 번호는 재전송 공격을 거부하며, 사전 공유 키(아래에서 설명할 OTAR로 교체됨)는 라우팅 경로를 신뢰 경로에서 분리합니다. 위성 운영자는 불투명한 번들 바이트만 볼 수 있으며, 라우팅 경로의 어떤 요소도 내용을 읽거나 수정하거나 위조하거나 바꿔치기할 수 없습니다.
이것이 중요한 이유는 우리가 다른 누군가의 하드웨어 위에 올라탄 임차인이기 때문입니다. hosted-payload satellite 에서는 여러 임차인이 하나의 버스를 공유하며, 컨테이너 격리만으로는 충분하지 않습니다. 공유 Linux 커널은 커널 수준 CVE로 인해 임차인 경계가 정기적으로 무너지며, 같은 원시 기법들이 새로운 형태로 계속 나타납니다: Dirty Frag (올해 공개된 범용 Linux LPE), Fragnesia (같은 계열의 매우 가까운 변종), 그리고 "Copy Fail", 4월 말 공개되어 주요 배포판 전체에 한꺼번에 영향을 준 Linux 커널 권한 상승 취약점입니다. 그 이전 사례들(Dirty Pipe 는 2022년, nf_tables use-after-free 는 2024년 컨테이너 탈출에 악용됨)을 보면 앞으로도 더 나올 것입니다. 지상 서버에서는 패키지 관리자를 실행하고 재부팅하면 되지만, 궤도에서는 커널 패치 자체가 별도의 전달 문제이며 자체적인 지연을 가지며, 때로는 아예 불가능하기도 합니다. 각 번들을 둘러싼 암호학적 외피만이 유일하게 지속 가능한 보장입니다.
기밀성과 진정성 외에도, 장기 임무의 위협 모델에는 키 교체가 필요합니다. Borealis는 사후양자 서명 키(ML-DSA-65) 를 위한 OTAR(Over-The-Air Rekeying)를 지원합니다. 이 키들은 위성의 수명 전체(10년에서 15년) 동안 사용되기 때문에, NASA의 Space System Protection Standard (NASA-STD-1006A) 는 사후양자 명령 인증을 미래의 선택지가 아니라 요구사항으로 다룹니다. OTAR를 사용하면 위성을 다시 플래시하지 않고도 사후양자 키를 교체할 수 있습니다. 우리가 아는 한 이것은 사후양자 OTAR의 최초 공개 궤도 내 시연 이 될 것이며, 우리는 이후 패스에서 실제 교체를 수행할 계획입니다.
Borealis는 DPhi의 hosted-payload module 위에서 게스트로 실행됩니다. 하드웨어는 Linux를 실행하는 Arm SoC(4개의 Cortex-A53 코어, 4 GB RAM)입니다. 비행용 바이너리는 5-10 MB 크기의 정적 링크 바이너리이며, FROM scratch Docker 이미지로 배포됩니다. 이것은 버스에서 텔레메트리(각도, 속도, 위치)와 온보드 카메라(저품질의 어안 렌즈로, 데모용으로만 적합함)를 폴링합니다. 위성 측 루프의 핵심은 다음과 같습니다:
let send_telemetry t ~prefix payload =
let bundle =
make_bundle t ~source:Eid.sat_telem
~destination:Eid.ground_telem ~payload
in
match protect_bundle t bundle with
| Ok protected ->
ignore (write_bundle t ~dir:(downlink_dir t.config) ~prefix protected)
| Error _ -> log t "Failed to protect telemetry bundle"
protect_bundle 은 SDLS Security Association의 키를 사용해 BPSec를 적용합니다. 이는 지상과 위성이 프로비저닝 시점에 합의한 암호학적 매개변수입니다. 이 중 어느 하나라도 실패하면, 어떤 번들도 위성을 떠나지 않습니다.
업링크 경로는 다운링크 경로를 그대로 반영합니다. 위성은 /data/uplink/ 에서 번들을 읽고, 각 번들의 BPSec 보호를 해제한 뒤, 번들 계층에서 목적지에 따라 라우팅합니다:
if dest = Eid.sat_cmd then handle_command t payload
else if dest = Eid.sat_otar then handle_otar t payload
else log t "Unknown destination"
텍스트 명령은 ADT로 파싱되는 짧은 UTF-8 문자열이며, 타입체커가 완전한 디스패치를 강제합니다:
type cmd = Ping | Check | Capture | Halt
let dispatch t = function
| Ping -> send_response t ~prefix:"pong" "PONG"
| Check -> run_self_check t
| Capture -> capture_and_send t
| Halt -> t.shutdown_requested <- true
새 명령을 추가한다는 것은 생성자를 하나 추가한다는 뜻이며, 그러면 컴파일러가 아직 처리되지 않은 모든 위치를 표시해 줍니다.
OTAR 재키 메시지는 다른 분기로 갑니다. 페이로드는 텍스트가 아니라 바이너리이며, 통합 시점에 위성에 적재되어 모듈의 프로세스 메모리에 존재하는 마스터 키로 암호화됩니다(이 모듈에는 TPM이나 secure element가 없는데, 방사선 내성을 가진 것을 만드는 일은 여전히 미해결 하드웨어 문제이기 때문입니다). 위성은 새 키를 복호화해 staging 슬롯에 보관한 뒤 활성화합니다. 현재 비행 루프는 수신 즉시 활성화합니다. 이 프로토콜은 또한 운영자가 커밋 전에 설치를 검증하는 별도의 지상 주도 활성화 단계도 지원하며, 그 경로로 바꾸는 것은 새 코드가 아니라 비행 루프 변경입니다.
마스터 키 자체에는 교체 경로가 없습니다. 이 키는 위성이 발사체에 결합되기 전에 페이로드에 설치되었고, 우주선이 궤도에 오른 뒤에는 더 신뢰할 수 있는 새 전달 채널이 없습니다. 마스터 키를 잃으면 이 스택에는 접근할 수 없습니다. 하드웨어 기반 키 저장소가 없는 장기 임무에서는 이것이 솔직한 실패 모드입니다.
OxCaml 은 OCaml 위에 올라간 Jane Street의 컴파일러 브랜치입니다. 그 모드 시스템은 위성의 핫패스에서 중요합니다. Locality를 사용하면 할당을 스택에 묶인 것으로 표시할 수 있어, 그것들이 힙에도, GC에도 도달하지 않게 됩니다. Uniqueness와 capability는 공유 가변 상태를 타입 시스템 안에서 추적하여, 스택의 병렬 부분에서 데이터 레이스를 컴파일 타임 오류로 바꿉니다.
hosted-payload module의 핫패스는 CCSDS 디스패치입니다. 모든 CFDP 세그먼트, 모든 COP-1 프레임, 모든 카메라 패킷은 페이로드가 애플리케이션 로직에 도달하기 전에 Space Packet 헤더 디코드와 APID 기반 라우팅 단계를 거칩니다. 모든 패스에서 엄격한 스케줄링 마감시간이 있는 실시간 온보드 디스패치는 바로 EU ORCHIDE Horizon Europe 프로젝트가 다루도록 설계된 작업 부하입니다(이 온보드 작업이 처음 Tarides 내부에서 시작된 컨소시엄이며, 결국 우리가 Parsimoni 를 전용 우주 소프트웨어 회사로 분사하게 된 계기가 되었습니다).
CCSDS 디스패치 핫패스의 패킷당 지연 시간: Space Packet 기본 헤더를 3개 필드 레코드로 디코드하고 APID로 라우팅하는 작업. 일반 OCaml과, 같은 코드에 exclave_ stack_ 주석을 추가한 OxCaml의 비교입니다. 측정은 비행 모듈이 아니라 노트북에서 수행했습니다.
exclave_ stack_ 주석과 함께 OxCaml로 전환하면 디스패치 핫패스에서 p99.9 지연 시간이 패킷당 29 ns에서 9 ns로 감소 하고, GC 압력을 완전히 제거합니다(2500만 패킷 동안 394회의 minor GC에서 0회로). 처리량은 비슷합니다. 이득은 지터에 있으며, 수백 마이크로초의 지터 예산만 가진 hosted-payload module에서는 그것이 전부입니다.
방법은 기계적입니다. 반복마다 발생하는 힙 할당({ apid; seq_count; data_len })을 스택 할당(exclave_ stack_ { apid; seq_count; data_len })으로 바꾸고, 소비자가 이를 @ local 로 받도록 요구하면 됩니다. 타입 시스템은 레코드가 디스패치 범위를 벗어나지 못함을 증명하고, 컴파일러는 힙 트래픽을 생성하지 않으며, GC는 수집할 것이 없어집니다.
설정. Apple M5 Max, macOS 25.4. 일반 OCaml 5.3.0과 5.2.0+ox(Jane Street의 OxCaml 포크)를 비교했습니다. 작업 부하는 각각 256개의 CCSDS Space Packet 헤더 디스패치를 수행하는 100 000개 배치(총 약 25.6 M 패킷)이며, 각 디스패치는 레코드가 실제로 탈출하도록 [@inline never] 핸들러를 거칩니다. 10회 실행의 중앙값을 사용했습니다.
심각한 CVE의 약 70%는 C/C++ 코드베이스의 메모리 손상(버퍼 오버플로, use-after-free, 정수 오버플로)에서 비롯됩니다. 이는 Microsoft의 MSRC 분석 (2019) 과 Chromium의 2020년 연구 에 기반합니다. 우리의 보안 확장(SDLS, BPSec, OTAR)은 모두 암호문과 키 자료를 다루는데, 바로 이런 곳에서 메모리 버그의 피해가 가장 큽니다. 이 분야의 C 기반 기존 구현인 NASA CryptoLib 에도 이런 버그가 있었습니다. 예를 들어 TC 프레임 파서의 힙 버퍼 오버플로 는 조작된 프레임에서 정수 언더플로가 트리거가 되어 발생했습니다. OCaml 구현은 이런 종류의 공격 표면을 애플리케이션 로직에서 구조적으로 제거합니다. 런타임, 그 아래의 커널, 부트로더는 여전히 C이며 여전히 TCB에 속합니다. 메모리 안전성은 도움이 되는 곳에서 도움을 주지만, 신뢰 가능한 계산 기반에 대한 감사를 대체하지는 않습니다.
오늘날 OCaml이 우리에게 제공하는 것 너머로, 언어 자체도 계속 발전하고 있습니다. Jane Street 는 OCaml의 실험적 브랜치인 OxCaml을 유지하고 있습니다. 그 설계 목표는 프로그램의 성능 중요 부분에 대해 안전하고 예측 가능한 제어를 제공하되, 필요한 곳에서만 선택적으로 사용하고, 여전히 OCaml 안에 머무는 것입니다. 모든 유효한 OCaml 프로그램은 유효한 OxCaml 프로그램이기도 합니다. OxCaml Labs (Cambridge의 Anil Madhavapeddy 그룹)와 FP Launchpad (IIT Madras의 KC Sivaramakrishnan 연구실)는 OCaml 을 앞으로 밀고 있으며, Tarides는 준비된 조각들을 메인라인에 업스트림하고 있습니다.
저는 어쩌다 보니 달에만 집중했네요 :-) 먼저 궤도로 가는 것은 성능보다 정확성을 우선하는 것을 의미했습니다. 궤도에서의 프로토콜 버그는 수정 비용이 크기 때문입니다. 방어는 스택의 모든 계층을 관통합니다. 타입 검사, 형식적으로 검증된 암호학 프리미티브(libcrux, fiat-crypto), 상호운용성 테스트, 그리고 의존성 감사 가 그것입니다.
그 계층들 중 세 가지를 구체적인 예로 들어 보겠습니다. wire-format 코덱은 타입이 있는 스키마로부터 생성되며, 디코드 시점에 잘못된 바이트를 거부하고, Microsoft's EverParse 파서 생성기에 입력을 제공합니다. EverParse는 F* 에서 형식적으로 검증된 C 검증기를 생성합니다. 프로토콜 상태 기계는 GADTs 로 인코딩되어, 타입체커가 컴파일 타임에 잘못된 전이를 거부합니다. 상호운용성 파이프라인은 기존 참조 구현과 대조 실행되며, 타입 시스템이 표현할 수 없는 것을 잡아내고 그 과정에서 업스트림 라이브러리의 결함도 드러냅니다.
이 계층들이 잡아내는 것 너머로, 함수형 코어 덕분에 우리는 같은 코드를 비행 소프트웨어, 지상 소프트웨어, 테스트 오라클로 배포할 수 있습니다. 위의 protect_bundle 은 세 역할 모두에서 같은 함수입니다. 우리는 한 역할에서 기록한 트래픽을 다른 역할들에 공급하고, 출력을 바이트 단위로 비교합니다. 이 OCaml 코드는 다른 구현이 검증되는 기준 참조 구현이기도 합니다. 이것은 nqsb-TLS 접근법(Kaloper-Mersinjak, Mehnert, Madhavapeddy and Sewell, USENIX Security 2015)이며, TLS에서 10년 동안 그 효용이 입증되었습니다. Nitrokey's NetHSM 은 오늘날 실제 출하되는 하드웨어 보안 모듈에서 같은 OCaml TLS 스택을 실행합니다.
Borealis도 예외가 아닙니다. 우리가 몇 달 만에 완전한 CCSDS 프로토콜 스택을 0에서부터 궤도 내 시연까지 만든 것처럼 보일 수도 있습니다. 하지만 실제로는 그렇지 않습니다. 핵심 라이브러리는 MirageOS 에서 왔고, 지난 10년 동안 지상에서 프로덕션으로 실행되어 왔습니다. 라이브러리 운영체제는 정의상 필요한 조각을 골라 쓰는 대규모 도구 상자입니다.
ASPLOS 2013 unikernels 논문 은 봉인된 단일 목적 이미지가 클라우드 인프라를 개선할 수 있는지 물었습니다. 10년 뒤, 같은 라이브러리들은 Docker Desktop 안에서 실행되고 수억 대의 노트북에 배포되고 있습니다. 이제 그것들은 우주에서도, ClusterGate-2에서도 실행되며, 우리가 처음 그것들을 설계했을 때는 예상하지 못했던 장소에서 unikernel이 아니라 Linux 프로세스로서 시스템 수준의 배관 작업을 수행합니다.
Borealis는 궤도 위의 하나의 바이너리입니다. 다음 문제는 규모입니다: 지상의 Linux에 Docker가 가져온 것과 같은 한 번의 명령 수준의 용이함으로, 많은 위성에 걸쳐 특화된 페이로드 바이너리의 플릿을 배포하고 관리하는 것입니다. 더 어려운 절반은 그것을 안전하게 하는 일입니다. 지상에서의 서명된 업데이트, 페이로드 간 격리, 실제로 무엇이 실행 중인지에 대한 attestaton이 필요합니다. 하드웨어를 궤도에 올리는 일은 점점 일상적이 되어 가고 있습니다. 흥미로운 문제는 점점 그 위에서 실행되는 소프트웨어 쪽으로 이동하고 있는데, 이는 서버 자체보다 그 위의 스택이 더 중요해졌던 클라우드 컴퓨팅의 익숙한 변화와 닮아 있습니다. 이것이 바로 우리가 Parsimoni 에서 Cambridge 와 그 밖의 협력자들과 함께 다음으로 구축하고 있는 것입니다. 저는 그 더 넓은 질문을 Is Running Untrusted Code on a Satellite a Good Idea? 에서 개괄한 바 있습니다.
페이로드 소프트웨어를 만들고 있거나, 자신의 버스에서 hosted payload를 고려하고 있거나, 비행 환경에서의 OCaml에 대해 의견을 나누고 싶다면, 저에게 연락 하거나 Parsimoni 팀 에게 연락해 주세요.