HIPERSPACE

Securing ultra-high speed communication networks in low orbit sounds like technology from a galaxy far, far away. But it is happening now. SDA created a program for increasing the performance of their satellites by several orders of magnitude – moving from around one megabyte per second to hundreds of gigabytes per second – while using approximately the same amount of power, and preparing to support new encryption standards. These new cryptographic modules will need to be certified by the National Security Agency (NSA) and must be able to transmit and receive encrypted data with a throughput of at least 50 gigabits per second, per channel, over six channels.

Galois, in its first project with SDA, is meeting this space-age need in the High Integrity, Performant, Efficient Realization of a SPAceborne Cryptographic Engine (HIPERSPACE) project.

HIPERSPACE focuses on the creation of high-assurance and ultra-high performance implementations of the most performance-intensive cryptographic functions used in low earth orbit. Its platform is low size, weight, and power (SWaP) with platform/client-optimized Power, Performance, Area, and Security (PPAS). Galois is working on this project with its spin-out Niobium Microsystems, as well as Innoflight, a developer of encryption technologies for spaceborne applications. HIPERSPACE’s technical products will also be NSA-certifiable.

Digital Engineering

HIPERSPACE is one of many Galois projects demonstrating Galois’s wide-ranging digital engineering capabilities. Designed to be a product line, the HIPERSPACE platform is an integrated set of hardware, firmware, and software systems engineering artifacts – including documentation, specifications, and source code – that can derive multiple different products from a build / synthesis / fabrication process. The product created and assured in HIPERSPACE is optimized for SDA’s current need: Low SWaP, high performance, and high assurance. But the same product line could be used to create a product with a different optimization function in mind, or simply to explore the trade space of spaceborne high assurance cryptography.

Calculating the Jump to HIPERSPACE

Galois has extensive experience developing side-channel-free, high-assurance cryptographic cores. HIPERSPACE’s AES cores were formally specified using Cryptol, Galois’s flagship tool for simplifying the design, implementation, and verification process for cryptographic implementations. In fact, much of the register transfer-level (RTL) in HIPERSPACE is automatically generated by Cryptol from formal NSA-approved models of cryptographic algorithms.

HIPERSPACE’s cryptographic algorithms and protocols are specified using Cryptol, as well as several other formal languages. Client system requirements are captured as specifications in a semi-formal system specification language called ʟᴀɴᴅᴏ, including a cryptographic module subsystem.

Theorems in the Cryptol specification come directly from theorems stated in source documents, such as NIST standards and academic papers, and are refined from requirements expressed in ʟᴀɴᴅᴏ. Those theorems are used to validate the specification (formally validating that our AES256 specification is, in fact, AES256). The theorems demonstrate (through automated testing) and prove (using SAW) that software and firmware implementations of AES256 are exactly AES256 – no more, no less.

For the hardware implementation generated from Cryptol (which is further refined by Niobium engineers to meet performance goals), Galois uses a combination of in-house and traditional open source and proprietary hardware verification tools and techniques to demonstrate that the implementation conforms to the specification. In fact, our entire formal assurance case is based only on an open source verification flow using SAW, Cryptol, and YosysHQ’s Tabby CAD tool suite.

Results Faster Than Lightspeed

HIPERSPACE finished its second major milestone ahead of schedule. The team delivered the semi-formal and formal system specification, product line specification, architecture specification, and cryptographic algorithm specification. Using digital engineering, 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.

The HIPERSPACE platform is designed to exceed SDA’s baseline program objectives. For example, the SDA proposal request didn’t ask for a full digital engineering project, or for the project to be high-assurance, using formal methods. Galois is overachieving SDA’s goals within available budget not only for this project’s success but to further demonstrate the commercial viability of digital engineering and hardware/software co-design and co-verification product lines.

It’s also worth noting that the HIPERSPACE platform could be used in other contexts, not just for outer space. It is licensable for other demanding areas, including nationally critical infrastructure or national security use cases.

HIPERSPACE isn’t Galois’s first digital engineering application, nor its last. Deploying this methodology multiple times helps build evidence for digital engineering’s exemplary outcomes, saving time and costs, dramatically increasing assurance, and decreasing risk for our clients.

This material is based upon work supported by the Space Development Agency (SDA) under Contract No. HQ085022C0004. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Space Development Agency (SDA).