Từ trái đất lên vũ trụ: Khi ngôn ngữ OCaml chinh phục quỹ đạo thấp

Vào ngày 23 tháng 4 vừa qua, một cột mốc quan trọng đã được đánh dấu trong lĩnh vực công nghệ vũ trụ: ngăn xếp giao thức CCSDS được viết hoàn toàn bằng ngôn ngữ OCaml đã khởi động thành công trên quỹ đạo Trái Đất thấp (LEO). Dự án mang tên mã Borealis đang chạy bên trong mô-đun tải trọng ClusterGate-2 của DPhi Space trên vệ tinh chủ, với khả năng điều khiển và kiểm soát được mã hóa đầu cuối cùng với cơ chế xoay khóa hậu lượng tử (post-quantum key rotation) — tất cả đều được triển khai bằng OCaml an toàn.

Lộ trình phát triển OCaml 5.0 hướng tới Mặt Trăng

Tại sao lại chọn OCaml cho không gian?

Việc chạy mã không đáng tin cậy trên vệ tinh là một rủi ro bảo mật khổng lồ, và OCaml được xem là ngôn ngữ lý tưởng để vận hành trong môi trường này nhờ tính an toàn của nó. Trong bài phát biểu chủ đạo tại ICFP 2022, KC Sivaramakrishnan đã nhìn lại nỗ lực kỹ thuật kéo dài một thập kỷ để tạo ra OCaml 5 — phiên bản đưa ra khả năng đa luồng an toàn và hiệu suất cao vào thời gian chạy của OCaml.

KC đã kết thúc bài nói chuyện của mình bằng sự suy đoán rằng OCaml 5.0 sẽ lên được Mặt Trăng, nhờ các tính năng ngôn ngữ mang lại hiệu suất tương đương C/Rust khi cần thiết trong khi vẫn giữ được sự chặt chẽ về mặt toán học của ML cổ điển. Tại Parsimoni, chúng tôi đã coi những lời đó theo nghĩa đen quite một chút :-)

Nhật ký khởi động lần đầu của Borealis trên bảng điều khiển tác vụ

Borealis thực sự chạy những gì?

Về cơ bản, Borealis là một daemon (quy trình nền). Cả trên mặt đất và trên vệ tinh, nó nói một giao thức client-server bình thường (truy vấn telemetry, lệnh và phản hồi, yêu cầu rekey OTAR), có hình dạng giống như bất kỳ máy chủ sản xuất nào. Điều bất thường nằm ở lớp truyền dẫn bên dưới.

Ngăn xếp giao thức là triển khai thuần OCaml của CCSDS — họ giao thức liên kết tàu vũ trụ với mặt đất. Nó bao phủ mọi lớp từ khung radio lên qua Bundle Protocol và các tiện ích bảo mật ở trên; các định dạng nhị phân được mô tả như các codec ocaml-wire.

Trên ClusterGate-2, chỉ có các lớp trên cùng của ngăn xếp được kích hoạt. Vệ tinh không có kết nối mạng từ bên ngoài. Liên kết mặt đất duy nhất là tải lên và tải xuống tệp qua API của DPhi: một tệp được ghi vào thư mục uplink sẽ được DPhi chuyển tiếp trong lần qua tiếp theo, và downlink hoạt động tương tự. Borealis coi hệ thống tệp đó là một mạng dung sai độ trễ.

Mọi lệnh, phản hồi, mẫu telemetry và đoạn ảnh đều được tuần tự hóa thành một gói BPv7 và ghi vào đĩa; DPhi chuyển tiếp tệp dưới dạng byte mù. BPSec bao bọc mỗi gói trong hai khối mở rộng: một cái mã hóa payload, cái còn lại xác thực nó. Các số thứ tự từ chối việc phát lại (replay), và các khóa được chia sẻ trước (được xoay vòng bởi OTAR) giữ đường dẫn định tuyến ra khỏi đường dẫn tin cậy.

Bảo mật trên môi trường Hosted Payload

Điều này rất quan trọng vì chúng tôi là "khách thuê" trên phần cứng của người khác. Trên một vệ tinh hosted-payload, nhiều khách thuê chia sẻ một bus duy nhất, và sự cô lập của container đơn thuần là không đủ. Một nhân Linux được chia sẻ có nghĩa là các lỗi CVE cấp nhân thường xuyên phá vỡ ranh giới khách thuê.

Biểu đồ độ trễ tail khi sử dụng OxCaml

Trên máy chủ mặt đất, bạn có thể chạy trình quản lý gói và khởi động lại; nhưng trên quỹ đạo, vá lỗi nhân là một vấn đề vận hành riêng với độ trễ của nó, và đôi khi hoàn toàn không thể thực hiện được. Lớp bao bói mật mã xung quanh mỗi gói là sự đảm bảo bền vững duy nhất.

Ngoài tính bảo mật và tính xác thực, mô hình đe dọa của nhiệm vụ dài hạn cần xoay khóa. Borealis hỗ trợ OTAR (Over-The-Air Rekeying) cho các khóa ký hậu lượng tử (ML-DSA-65) của mình. Những khóa này tồn tại trong suốt vòng đời của vệ tinh (mười đến mười lăm năm), đó là lý do Tiêu chuẩn Bảo vệ Hệ thống Không gian của NASA (NASA-STD-1006A) coi việc xác thực lệnh hậu lượng tử là một yêu cầu bắt buộc chứ không phải là một lựa chọn trong tương lai.

Tối ưu hóa hiệu suất với OxCaml

OxCaml là nhánh trình biên dịch của Jane Street trên nền tảng OCaml. Hệ thống chế độ (mode system) của nó quan trọng trên đường dẫn nóng (hot path) của vệ tinh. Locality cho phép chúng tôi đánh dấu các cấp phát là ràng buộc stack, do đó chúng không bao giờ chạm đến heap và không bao giờ chạm đến GC. Uniqueness và capabilities theo dõi trạng thái có thể thay đổi được chia sẻ trong hệ thống kiểu, biến các cuộc đua dữ liệu thành lỗi thời gian biên dịch trên các phần song song của ngăn xếp.

Việc chuyển sang OxCaml với các chú thích exclave_stack làm giảm độ trễ p99.9 từ 29 ns xuống còn 9 ns cho mỗi gói trên đường dẫn phân phối nóng, và loại bỏ hoàn toàn áp lực GC (từ 394 GC nhỏ xuống không một chút nào trên 25 triệu gói). Thông lượng có thể so sánh; lợi ích nằm ở sự dao động (jitter), và trên mô-đun hosted-payload với ngân sách dao động hàng trăm micro giây, đó là toàn bộ cuộc chơi.

Công thức này mang tính cơ học: chuyển một cấp phát heap cho mỗi lần lặp ({ apid; seq_count; data_len }) thành một cấp phát stack (exclave_stack { apid; seq_count; data_len }), và yêu cầu người tiêu dùng lấy nó @local. Hệ thống kiểu chứng minh rằng bản ghi không thể thoát khỏi phạm vi phân phối; trình biên dịch không phát sinh traffic heap nào; GC không có gì để thu gom.

Tương lai của phần mềm vũ trụ

Khoảng 70% các CVE nghiêm trọng trong các cơ sở mã C/C++ bắt nguồn từ hỏng hóc bộ nhớ (tràn bộ đệm, use-after-free, tràn số nguyên), dựa trên phân tích của Microsoft MSRC (2019) và nghiên cứu của Chromium năm 2020. Việc triển khai OCaml loại bỏ lớp bề mặt tấn công đó khỏi logic ứng dụng bằng cấu trúc.

Borealis không phải là ngoại lệ. Nó có thể trông giống như chúng tôi đã viết một ngăn xếp giao thức CCSDS đầy đủ từ số không đến bản demo trên quỹ đạo trong vài tháng. Điều đó không đúng. Các thư viện cốt lõi đến từ MirageOS và đã chạy trong sản xuất trên mặt đất trong thập kỷ qua. Một hệ điều hành thư viện, theo định nghĩa, là một bộ công cụ lớn nơi bạn chọn các mảnh bạn cần.

Borealis là một tệp nhị phân trên quỹ đạo. Vấn đề tiếp theo là quy mô: triển khai và quản lý một đội tàu các tệp nhị phân chuyên biệt trên nhiều vệ tinh với sự dễ dàng như một lệnh duy nhất mà Docker đã mang lại cho Linux trên mặt đất. Việc đưa phần cứng lên quỹ đạo đang trở nên thường xuyên; các vấn đề thú vị ngày càng nằm ở phần mềm chạy trên nó, một sự chuyển dịch quen thuộc từ điện toán đám mây, nơi ngăn xếp trên cùng các máy chủ cuối cùng lại quan trọng hơn chính các máy chủ đó.

Đó là những gì chúng tôi đang xây dựng tiếp theo tại Parsimoni, với sự cộng tác tại Cambridge và hơn thế nữa.