The project, Galois’s first for the U.S. Space Development Agency (SDA), focuses on the creation of high-assurance, high-performance implementations of cryptographic functions for deployment in LEO.
Working alongside Galois spinout Niobium Microsystems and partner Innoflight, the company’s digital engineering team aims to create a platform that effectively secures the SDA’s ultra-high speed, satellite communication network, enabling the safe transmission and receipt of encrypted data and preparing to support new encryption standards, all on a low size, weight, and power (SWaP) platform.
HIPERSPACE’s cryptographic algorithms and protocols are formally specified using Cryptol, Galois’s flagship cryptography tool, as well as several other formal languages.
The team delivered the semi-formal and formal system specification, product line specification, architecture specification, and cryptographic algorithm specification. Using digital engineering methodologies, the Galois team proved, for all possible inputs, that software and firmware implementations (hand-written, automatically generated, or a combination) behave identically to the specification.