우주 속의 O(x)Caml

4월 23일, 우리의 순수 OCaml 기반 CCSDS 프로토콜 스택이 저궤도(low Earth orbit)에서 부팅되었습니다! 코드명 Borealis인 이 프로젝트는 호스트 위성에 탑재된 DPhi Space의 ClusterGate-2 페이로드 모듈 내부에서 실행되고 있으며, 종단 간 암호화(end-to-end-encrypted)된 명령 및 제어(command and control)와 양자 내성 키 로테이션(post-quantum key rotation)을 모두 안전한 OCaml로 구현했습니다.

여기서 왜 OCaml이 중요할까요? 위성에서 실행되는 신뢰할 수 없는 코드는 거대한 보안 리스크이며, OCaml은 우주에서 실행하기에 이상적인 안전한 언어(safe language)입니다. KC Sivaramakrishnan는 그의 ICFP 2022 기조연설에서, OCaml 런타임에 안전하고 성능이 뛰어난 멀티스레딩(multi-threading)을 도입한 릴리스인 OCaml 5를 탄생시킨 10년간의 엔지니어링 노력을 회고했습니다.

KC는 그의 강연을 마치며, OCaml 5.0이 고전적인 ML의 수학적 엄밀함을 유지하면서도 필요에 따라 C/Rust와 같은 성능을 제공할 수 있는 언어적 특징 덕분에 달까지 가게 될 것이라고 추측하며 끝을 맺었습니다. 여기 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
...

실제로 실행되고 있는 것

Borealis는 데몬(daemon)입니다. 지상과 위성 모두에서 일반적인 클라이언트-서버 프로토콜(텔레메트리 쿼리, 명령 및 응답, OTAR 키 재설정 요청)을 사용하며, 이는 일반적인 프로덕션 서버와 동일한 형태를 가집니다. 특이한 점은 그 아래에 깔린 와이어(wire)입니다.

이 프로토콜 스택은 우주선과 지상을 연결하는 프로토콜 제품군인 CCSDS를 순수 OCaml로 구현한 것입니다. 이는 라디오 프레이밍(radio framing)부터 번들 프로토콜(Bundle Protocol) 및 그 상위의 보안 확장 기능에 이르기까지 모든 계층을 다룹니다. 바이너리 형식은 ocaml-wire 코덱(codecs)으로 기술되어 있습니다.

ClusterGate-2에서는 해당 스택의 상위 계층만 실행됩니다. 위성은 외부로부터의 네트워크 연결성이 없습니다. 유일한 지상 링크는 DPhi의 API를 통한 파일 시스템 업로드 및 다운로드뿐입니다. 업링크 (uplink) 디렉토리에 기록된 파일은 다음 통과 시점에 DPhi에 의해 전달되며, 다운링크 (downlink)도 동일한 방식으로 작동합니다. Borealis는 해당 파일 시스템을 지연 내성 네트워크 (DTN, Delay-Tolerant Network)로 취급합니다. 모든 명령, 응답, 텔레메트리 (telemetry) 샘플 및 이미지 청크 (chunk)는 BPv7 번들 (bundle)로 직렬화되어 디스크에 기록되며, DPhi는 해당 파일을 불투명한 바이트 (opaque bytes) 형태로 전달합니다.

BPSec은 각 번들을 두 개의 확장 블록 (extension blocks)으로 감쌉니다. 하나는 페이로드 (payload)를 암호화하고, 다른 하나는 이를 인증합니다. 시퀀스 번호 (sequence numbers)는 재전송 공격 (replays)을 차단하며, (아래에서 설명할 OTAR에 의해 교체되는) 사전 공유 키 (PSK, Pre-shared keys)는 라우팅 경로를 신뢰 경로 (trust path)에서 제외합니다. 위성 운영자는 오직 불투명한 번들 바이트만을 보게 되며, 라우팅 경로상의 그 무엇도 내용을 읽거나, 수정하거나, 위조하거나, 대체할 수 없습니다.

이것이 중요한 이유는 우리가 타인의 하드웨어에 거주하는 테넌트 (tenant)이기 때문입니다. 호스팅 페이로드 (hosted-payload) 위성에서는 여러 테넌트가 단일 버스 (bus)를 공유하며, 컨테이너 격리 (container isolation)만으로는 충분하지 않습니다. 리눅스 커널 (Linux kernel)을 공유한다는 것은 커널 수준의 CVE (Common Vulnerabilities and Exposures)가 정기적으로 테넌트 경계를 허문다는 것을 의미하며, 동일한 원리들이 새로운 형태로 계속해서 다시 나타납니다. 올해 발표된 범용 리눅스 LPE (Local Privilege Escalation)인 Dirty Frag, 같은 계열의 가까운 친척인 Fragnesia, 그리고 4월 말에 공개되어 모든 주요 배포판을 동시에 타격한 리눅스 커널 권한 상승 (privilege escalation) 취약점인 "Copy Fail"이 그 예입니다. 이전 사례들(2022년의 Dirty Pipe, 2024년 컨테이너 탈출에 악용된 nf_tables use-after-free)은 앞으로 더 많은 사례가 발생할 것임을 시사합니다. 지상 서버에서는 패키지 관리자를 실행하고 재부팅할 수 있지만, 궤도 상에서는 커널 패칭 (kernel patching) 자체가 고유한 지연 시간을 가진 전달 문제이며, 때로는 아예 불가능할 수도 있습니다. 각 번들을 감싸는 암호화 봉투 (cryptographic envelope)가 유일하고 지속 가능한 보장책입니다.

기밀성 (confidentiality) 및 인증 (authenticity)을 넘어, 장기 임무의 위협 모델 (threat model)에는 키 로테이션 (key rotation)이 필요합니다. Borealis는 양자 내성 서명 키 (post-quantum signing keys, ML-DSA-65)를 위한 OTAR (Over-The-Air Rekeying, 무선 키 교체)를 지원합니다. 이러한 키들은 위성의 수명(10~15년) 동안 유지되는데, 이것이 바로 NASA의 우주 시스템 보호 표준 (Space System Protection Standard, NASA-STD-1006A)이 양자 내성 명령 인증 (post-quantum command authentication)을 미래의 선택 사항이 아닌 필수 요구 사항으로 취급하는 이유입니다. OTAR를 사용하면 위성의 펌웨어를 다시 플래싱 (re-flashing)하지 않고도 양자 내성 키를 교체할 수 있습니다. 저희가 알기로는 이것이 **양자 내성 OTAR의 첫 번째 공개 궤도 시연 (public in-orbit demonstration)**이 될 것입니다. 저희는 이후의 패스 (pass)에서 로테이션을 실행할 계획입니다.

Borealis는 Linux가 실행되는 Arm SoC (4개의 Cortex-A53 코어, 4 GB RAM) 기반의 DPhi 호스트 페이로드 모듈 (hosted-payload module) 위에서 게스트 (guest)로 실행됩니다. 비행 바이너리 (flight binary)는 5-10 MB 크기의 정적 링크 (statically linked) 형태이며, FROM scratch Docker 이미지로 배포됩니다. 이 시스템은 버스 (bus)를 폴링 (poll)하여 텔레메트리 (telemetry, 각도, 속도, 위치)와 온보드 카메라 (데모용으로만 적합한 저화질 어안 렌즈) 데이터를 수집합니다. 위성 측 루프 (satellite-side loop)의 핵심은 다음과 같습니다:

let send_telemetry t ~prefix payload =
let bundle =
make_bundle t ~source:Eid.sat_telem
...

protect_bundle은 프로비저닝 (provisioning) 시 지상과 위성이 합의한 암호화 파라미터인 SDLS 보안 연관 (Security Association)의 키를 사용하여 BPSec를 적용합니다. 이 과정 중 어느 하나라도 실패하면 어떤 번들 (bundle)도 위성을 떠나지 못합니다.

업링크 (uplink) 경로는 다운링크 (downlink) 경로를 미러링합니다. 위성은 /data/uplink/에서 번들을 읽고, BPSec로 각 번들의 보호를 해제한 뒤, 번들 계층 (bundle layer)에서 목적지에 따라 라우팅합니다:

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 (Algebraic Data Type, 대수적 데이터 타입)로 파싱되는 짧은 UTF-8 문자열이며, 타입 체커 (typechecker)가 철저한 디스패치 (exhaustive dispatch)를 강제합니다:

type cmd = Ping | Check | Capture | Halt
let dispatch t = function
| Ping -> send_response t ~prefix:"pong" "PONG"
...

새로운 명령을 추가한다는 것은 생성자 (constructor)를 추가하는 것을 의미하며, 그러면 컴파일러가 해당 명령이 아직 처리되지 않은 모든 곳을 표시해 줍니다.

OTAR 재키(rekey) 메시지는 다른 분기(branch)를 따릅니다. 페이로드(payload)는 텍스트가 아닌 바이너리(binary) 형태이며, 통합(integration) 시점에 위성에 로드되어 모듈의 프로세스 메모리(process memory)에 상주하는 마스터 키(master key)로 암호화됩니다 (모듈에는 TPM이나 보안 요소(secure element)가 없습니다. 방사선 내성(radiation-tolerant)을 갖춘 보안 요소를 제작하는 것은 여전히 해결되지 않은 하드웨어 문제입니다). 위성은 새로운 키를 복호화하여 스테이징 슬롯(staging slot)에 보관한 뒤 활성화합니다. 현재의 비행 루프(flight loop)는 수신 즉시 활성화됩니다. 또한 이 프로토콜은 운영자가 설치를 확인한 후 확정하는, 지상 주도형(ground-driven) 별도 활성화 단계도 지원하며, 해당 경로로 전환하는 것은 비행 루프의 변경일 뿐 새로운 코드를 추가하는 것이 아닙니다.

마스터 키 자체에는 로테이션(rotation) 경로가 없습니다. 마스터 키는 위성이 발사체와 결합되기 전에 페이로드에 설치되었으며, 우주선이 궤도에 진입한 후에는 새로운 키를 전달할 수 있는 더 신뢰할 수 있는 채널(more-trusted channel)이 존재하지 않습니다. 만약 마스터 키를 분실하면 이 스택(stack)에는 접근할 수 없습니다. 이것이 하드웨어 기반 키 저장소가 없는 장기 미션에서 발생할 수 있는 정직한 실패 모드(failure mode)입니다.

다음에 올 것: OxCaml

OxCaml은 OCaml을 기반으로 한 Jane Street의 컴파일러 분기(branch)입니다. OxCaml의 모드 시스템(mode system)은 위성의 핫 패스(hot path)에서 매우 중요합니다. 지역성(Locality)을 통해 할당(allocation)을 스택 바운드(stack-bound)로 표시할 수 있으므로, 이는 힙(heap)에 도달하지 않으며 가비지 컬렉션(GC)에도 도달하지 않습니다. 유일성(Uniqueness)과 기능(capabilities)은 타입 시스템(type system) 내에서 공유 가능한 가변 상태(shared mutable state)를 추적하여, 스택의 병렬 부분에서 데이터 경합(data race)을 컴파일 타임 에러(compile-time error)로 전환합니다.

호스트된 페이로드(hosted-payload) 모듈의 핫 패스는 CCSDS 디스패치(dispatch)입니다. 모든 CFDP 세그먼트(segment), 모든 COP-1 프레임(frame), 모든 카메라 패킷(packet)은 페이로드가 애플리케이션 로직(application logic)에 도달하기 전, 우주 패킷(Space Packet) 헤더 디코드(decode)와 APID 기반 라우팅(routing) 단계를 거칩니다. 매 패스(pass)마다 엄격한 스케줄링 마감 시간(scheduling deadlines)을 갖는 실시간 온보드(on-board) 디스패치는 바로 EU ORCHIDE Horizon Europe 프로젝트가 해결하기 위해 설정된 워크로드(workload)입니다 (이 온보드 작업이 Tarides 내부에서 처음 시작된 컨소시엄이며, 결과적으로 우리가 Parsimoni를 전용 우주 소프트웨어 기업으로 분사하게 된 계기가 되었습니다).

exclave_ stack_

. 비행 모듈이 아닌 노트북에서 측정되었습니다.
exclave_stack_ 어노테이션 (annotations)을 사용하여 OxCaml로 전환하면, 디스패치 핫 패스 (dispatch hot path)에서의 p99.9 지연 시간 (latency)이 패킷당 29 ns에서 9 ns로 감소하며, GC 압박 (GC pressure)을 완전히 제거합니다 (2,500만 개의 패킷 처리 동안 394회의 minor GC가 0회로 감소). 처리량 (Throughput)은 유사한 수준입니다. 핵심적인 이점은 지터 (jitter)이며, 수백 마이크로초의 지터 예산 (jitter budget)을 가진 호스팅 페이로드 모듈 (hosted-payload module)에서는 이것이 승패를 결정짓는 전부입니다.

방법은 기계적입니다. 반복(iteration)당 힙 할당 (heap allocation) ({ apid; seq_count; data_len })을 스택 할당 (stack-allocated) (exclave_stack_{ apid; seq_count; data_len })으로 바꾸고, 소비자 (consumer)가 이를 @local로 받도록 요구하는 것입니다. 타입 시스템 (type system)은 해당 레코드 (record)가 디스패치 스코프 (dispatch scope)를 벗어날 수 없음을 증명하며, 컴파일러는 힙 트래픽 (heap traffic)을 생성하지 않고, GC는 수집할 대상이 없게 됩니다.

설정 (Setup). Apple M5 Max, macOS 25.4. 순정 OCaml 5.3.0 대 5.2.0+ox (Jane Street의 OxCaml 포크). 워크로드 (Workload): 각각 256개의 CCSDS 우주 패킷 헤더 디스패치(dispatch)를 포함하는 100,000개의 배치(batch) (총 약 2,560만 개의 패킷), 각 패킷은 레코드가 실제로 탈출할 수 있도록 [@inline never] 핸들러 (handler)를 통해 라우팅됩니다. 10회 실행의 중앙값 (Median)입니다.

왜 OCaml인가

Microsoft의 MSRC 분석(2019)과 Chromium의 2020년 연구에 따르면, C/C++ 코드베이스에서 발생하는 심각한 CVE의 약 70%가 메모리 오염 (memory corruption: 버퍼 오버플로 (buffer overflows), use-after-free, 정수 오버플로 (integer overflows))에서 기인합니다. 우리의 보안 확장 기능들 (SDLS, BPSec, 그리고 OTAR)은 모두 암호문 (ciphertexts)과 키 자료 (key material)를 다루며, 이는 바로 메모리 버그가 가장 치명적인 지점입니다. 이 분야의 기존 C 기반 라이브러리인 NASA CryptoLib에서도 유사한 버그들이 있었습니다. 예를 들어, 조작된 프레임에 의한 정수 언더플로 (integer underflow)로 인해 발생하는 TC 프레임 파서 (TC frame parser)의 힙 버퍼 오버플로 (heap buffer overflow)가 그러합니다. OCaml 구현은 구조적으로 (by construction) 애플리케이션 로직에서 이러한 유형의 공격 표면 (attack surface)을 제거합니다. 런타임 (runtime), 하단의 커널 (kernel), 그리고 부트로더 (bootloader)는 여전히 C이며 여전히 TCB (Trusted Computing Base)에 속해 있습니다. 메모리 안전성 (memory safety)은 도움이 되는 곳에서 도움을 줄 뿐, 신뢰할 수 있는 컴퓨팅 기반 (trusted compute base)에 대한 감사를 대체할 수는 없습니다.

오늘날 OCaml이 우리에게 제공하는 것 이상으로, 언어 자체는 계속해서 발전하고 있습니다. Jane Street는 OCaml의 실험적인 브랜치인 OxCaml을 유지 관리하고 있습니다. OxCaml의 설계 목표는 프로그램의 성능이 중요한 (performance-critical) 부분에 대해 안전하고 예측 가능한 제어를 제공하는 것이며, 필요한 경우에만 선택적으로 (opt-in) 적용할 수 있고, 여전히 OCaml 내에 머무는 것입니다. 즉, 모든 유효한 OCaml 프로그램은 유효한 OxCaml 프로그램이기도 합니다. OxCaml Labs (Cambridge의 Anil Madhavapeddy 그룹)와 FP Launchpad (IIT Madras의 KC Sivaramakrishnan 연구실)가 OCaml을 앞으로 밀어붙이고 있으며, Tarides는 준비된 부분들을 메인라인 (mainline)으로 업스트림 (upstream) 합니다.

어쩌다 보니 달에 집중하게 되었네요 :-) 궤도에 먼저 진입한다는 것은 성능보다 정확성 (correctness)을 우선시해야 함을 의미했습니다. 궤도상의 프로토콜 버그는 수정 비용이 매우 크기 때문입니다. 방어 체계는 스택의 모든 계층에 걸쳐 작동합니다: 타입 검사 (type checking), 형식적으로 검증된 암호화 프리미티브 (formally verified cryptographic primitives; libcrux, fiat-crypto), 상호 운용성 테스트 (interop testing), 그리고 의존성 감사 (dependency audits)가 그것입니다.

이 계층들 중 세 가지를 구체적인 예로 들어보겠습니다. 와이어 포맷 코덱 (wire-format codecs)은 타입이 지정된 스키마 (typed schema)로부터 생성되며, 디코딩 시점에 잘못된 바이트를 거부하고, F*에서 형식적으로 검증된 C 검증기 (C validators)를 생성하는 Microsoft의 EverParse 파서 생성기 (parser generator)에 데이터를 공급합니다. 프로토콜 상태 머신 (protocol state machines)은 GADT (Generalized Algebraic Data Types)로 인코딩되어 있어, 타입 검사기 (typechecker)가 컴파일 타임에 유효하지 않은 전이 (invalid transitions)를 거부합니다. 상호 운용성 파이프라인 (interop pipeline)은 기존의 참조 구현체 (reference implementations)를 대상으로 실행되어, 타입 시스템이 표현할 수 없는 것을 포착하고 그 과정에서 업스트림 라이브러리의 결함을 드러냅니다.

이러한 계층들이 포착하는 것 이상으로, 함수형 코어 (functional core) 덕분에 우리는 동일한 코드를 비행 소프트웨어 (flight software), 지상 소프트웨어 (ground software), 그리고 테스트 오라클 (test oracle)로 배포할 수 있습니다. protect_bundle

위의 함수는 세 가지 역할 모두에서 동일합니다. 우리는 한 역할에서 기록된 트래픽을 다른 역할들에 입력하고, 출력을 바이트 단위로 비교합니다. 이 OCaml 코드는 다른 구현체들이 검증을 받는 기준 구현체 (reference implementation) 역할도 수행합니다. 이것이 nqsb-TLS 방식 (Kaloper-Mersinjak, Mehnert, Madhavapeddy and Sewell, USENIX Security 2015)이며, 지난 10년 동안 TLS 분야에서 그 유효성이 입증되었습니다. Nitrokey의 NetHSM은 오늘날 출시되는 하드웨어 보안 모듈 (HSM)에서 동일한 OCaml TLS 스택을 실행하고 있습니다.

Borealis도 예외는 아닙니다. 마치 우리가 단 몇 달 만에 처음부터 끝까지 전체 CCSDS 프로토콜 스택을 작성하여 궤도 시연 (in-orbit demonstration)까지 마친 것처럼 보일 수도 있습니다. 하지만 실제로는 그렇지 않았습니다. 핵심 라이브러리들은 MirageOS에서 가져온 것이며, 지난 10년 동안 지상 환경의 프로덕션 (production)에서 실행되어 왔습니다. 라이브러리 운영체제 (library operating system)란 정의상, 필요한 조각들을 선택하여 사용하는 거대한 도구 모음입니다.