Space-BACN

There will be numerous satellite constellations in low-earth orbit within the next few years, but only a few will be able to communicate with each other using current technology. A satellite constellation using custom-made components can only communicate with satellites made of the same components.

Today, satellite constellations are competing fiefdoms that do not play well with each other. Old satellite constellations cannot use the capabilities of new constellations. Military satellites cannot communicate with commercial satellites, even in instances where there is no classified data to transmit. In general, this friction decreases the overall effectiveness of all capabilities that are put in orbit, and enormous amounts of resources are spent on redundant capabilities.

DARPA’s Space-Based Adaptive Communications Node (Space-BACN) program aims to advance satellite communications by developing low-cost, high-speed reconfigurable optical datalinks to connect various low-earth orbit (LEO) constellations.

Specifically, Space-BACN focuses on the development of a modular optical aperture and a reconfigurable communications terminal for a low size, weight, power, and cost (SWaP) platform that aims to consume, for high-speed communication, less than 100 watts of power, and a low cost (under $100K) for each unit. This terminal must switch between multiple laser waveforms, and be remotely upgradable.

Galois’s prime partner for Space-BACN concentrated on building the optical modem for a terminal that promotes satellite interoperability. Galois focused entirely on building out the modem’s cybersecurity, utilizing our rigorous digital engineering (RDE) methodology.

Sizzling Security by Design

Galois’s tasks included hardening the Space-BACN operating system, the terminal’s hardware, firmware, and software, and the Command & Control (C2) channel. Defining and demonstrating automatically formally verifiable security requirements, and showing the benefits of using cyber-hardening technologies early during system design, were central to the project.

Next, Galois defined, refined, and realized a security-by-design process and methodology that was used by the team in the design, development, and assurance of the Space-BACN platform.

After that, Galois crafted a formal specification of the Space-BACN platform fit for tool-assisted cybersecurity analysis, and then performed the analysis.

The team then performed an objective cybersecurity architecture trade study analysis of the Space-BACN Security Subsystem. This analysis included a full feature model of the platform which included its system, hardware, and software components as well as the program’s threat model, explored using a multi-dimensional optimization function that included both estimated and computed platform SWaP, cost, and risk measures.

In order to put RDE in practice, and to demonstrate the Security-by-Design process and methodology, Galois created a high-assurance, secure First Stage BootLoader (FSBL) for the Space-BACN platform.

Finally, near the end of the project, Galois also offered to demonstrate how we might take the Government’s informal Interface Control Document (ICD) for Space-BACN and turn it into a Digital ICD—a Literate ICD (in the tradition of Knuth’s Literate Programming) that looks and feels like a normal, human-readable ICD, but also contains machine-interpretable models and specifications that automatically enable model-based reasoning, code generation, and assurance of the platform.

Thus, Galois’s final contribution to the program in this phase was a Space-BACN Digital ICD which contained, for example, a demonstration of the reuse of a formal specification of the Space Packet Protocol developed by NASA in order to specify Space-BACN’s flavor of Space Packet, and then automatically generate an implementation of that communication layer in Rust.

 BACN Bytes

A future phase will focus on an analysis (or demonstration) of Galois’s hardening techniques, benefits, overheads,  and residual vulnerabilities. The goal would be to deliver a design for a space-qualifiable system, and demonstrate fieldability by cyber-hardening essential functions.

A Crisp Conclusion

Space-BACN used several aspects of Galois’s RDE methodology – applied formal methods-centric, model-based, high-assurance software, firmware, hardware, and systems engineering. It had an assurance case suitable for NSA certification by the end of the project.

Galois believes that hardening vital systems should never be an afterthought. Building security into the design is a major pillar of the RDE methodology and one that contributes to a project’s overall success.

This research was, in part, funded by the U.S. Government. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.

Distribution Statement “A” (Approved for Public Release, Distribution Unlimited.) If you have any questions, please contact the Public Release Center.