Secure Satellite Software-Defined Payloads with High-Assurance Post-Quantum Cryptography

Authors: Virgile Robles, Karthikeyan Bhargavan, Franziskus Kiefer and Thomas Gazagnaire

As space missions increasingly rely on software-defined payloads, the need for secure, reliable, and future-proof communication becomes critical. This paper presents the integration of formally verified, post-quantum cryptography into RedactedOS, a unikernel-based operating system for satellite platforms. We leverage libcrux, a high-assurance cryptographic library written in Rust, and Bertie, a verified TLS 1.3 implementation, to enable memory-safe, side-channel resistant, and quantum-secure communication and update mechanisms. This proposed integration enables applications ranging from secure software updates to authenticated channels for quantum key distribution and key establishment for SDLS-based protocols. We demonstrate the viability of this approach with a proof-of-concept implementation for post-quantum signed software updates. This work is a step toward providing robust security foundations for next-generation space systems with minimal developer burden.