Security considerations in light launcher software

Security considerations in light launcher software
by Sophie Jenkins
London, UK (SPX) May 16, 2024

When Latitude began creating their small satellite launcher, Zephyr, they recognized the importance of selecting the correct programming language and development tools to support their efforts. They chose to work with high-integrity software experts AdaCore.

Latitude, who closed a Series B funding round in January of 2024 is currently preparing the first flight of Zephyr that will occur late 2025.

In this article, Jose Ruiz, a Product Manager at AdaCore, explores two essential factors to consider when selecting secure software for your space industry projects: the use of memory-safe languages and formal verification.

In the competitive New Space industry, ingenuity, reliability, and cost-effectiveness are paramount. When developing new projects, the correct choice of programming language is critical.

Selection of Memory-Safe Programming Languages
Memory safety is a crucial concept in software development. It addresses how an application handles memory operations such as reading, writing, allocation, and deallocation. A memory-safe application operates within the bounds of its allocated memory (it doesn't access or modify memory locations that it's not allowed to access).

Improper memory management can result in severe problems in software reliability. Languages that aren't memory-safe also negatively impact stability, developer productivity, and application performance. Organizations can substantially diminish software vulnerabilities by leveraging languages engineered to preempt memory safety issues, such as buffer overflows and use-after-free errors.

Introducing Formal Verification
Formal verification frameworks are instrumental in assessing the correctness of hardware and software design operations by applying formal mathematical proofs. These frameworks ensure the correctness of underlying algorithms within a system.

Despite adopting memory-safe programming languages, vulnerabilities persist in software systems. Testing alone is insufficient to comprehensively address these vulnerabilities due to the inherent complexities of code. Formal methods offer a systematic approach to demonstrating correctness and integrate verification into the development process.

Additionally, formal verification facilitates compliance with regulatory requirements and industry standards by providing concrete evidence of software correctness and security. Whether adhering to data privacy regulations, cybersecurity protocols, or quality assurance benchmarks, formal verification offers a robust framework for meeting and exceeding regulatory expectations.

Latitude and Zephyr
Latitude judged Ada and SPARK to have the best support for sound software engineering practice for their 200kg capacity launcher in LEO, thus reducing life cycle costs while meeting real-time embedded systems performance and predictability requirements.

By prioritizing memory safety and embracing formal verification, organizations can enhance their software's resilience against vulnerabilities and demonstrate compliance with regulatory expectations.