DARPA V-SPELLS to develop automated tools for understanding, Re-engineering and Assurance of legacy software of Defense and Aerospace systems

The complexity of  aerospace and defense software has grown manyfold. For example, the U.S. Air Force F-22 Raptor jet fighter, consists of about 1.7 million lines of software code, while the F-35 joint strike fighter has about 5.7 million lines of code to operate its onboard systems. Boeing’s new 787 Dreamliner requires about 6.5 million lines of software code to operate its avionics. Aerospace, defense, and military organizations use embedded software every day. Making sure that software is safe, secure, and reliable is critical. Large code bases and complex systems make this a challenge. Tough compliance requirements make it even more difficult. Airborne systems developers need the right tools to prove compliance and develop quality systems.

These defense systems are also needs upgradation to enhance the capability of platforms to handle new threats or integrate new technologies. This especially is important in cases where systems designers must move parts of existing software programs to new computer hardware like hardware accelerators, isolation enclaves, offload processors, and distributed computation. Defense and commercial systems alike are riddled with legacy software that is difficult to modernize, enhance, and re-engineer, largely due to a lack of effective understanding of the underlying legacy code, which makes predicting the effect of modifications a challenge. From a defense perspective, there is a growing need to enhance or replace components of existing software in critical platforms and systems with more secure and performant code, as well as a desire to use legacy software on new hardware to improve system performance. U.S. military researchers are asking for industry’s help to upgrade components of mission-critical software for aerospace and defense applications with more secure and higher-performing code

When introducing enhancements or replacements into large legacy code bases however, there is a high risk that the new code will not safely compose with the rest of the system. Existing means of verifying that updated software is correct-by-construction focus on clean-slate software development, essentially limiting their effectiveness to software that is developed from scratch.  Verified programming for creating software that is correct-by-construction cannot mitigate this risk today because current programming focuses on clean-slate software construction, assumes an existing formal specification typically not available for legacy systems, and requires expertise in formal methods not typically accessible to software developers. “Modernizing legacy software components for performance or security faces high risks in that the new software, despite being proven correct according to a specification, will not be fully compatible with the existing infrastructure,” said Dr. Sergey Bratus, program manager in DARPA’s Information Innovation Office (I2O). “System owners fear that they might need years of additional adjustments to new code to reliably interoperate with the actual behaviors of the system.”

To address these challenges, DARPA launched  Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program in July 2020 with  aim to make it possible for developers to incrementally enhance existing legacy software components with new verified code and ensure that the resulting software will safely compose with an existing system. Key to the approach is the ability to make incremental updates that are both correct and compatible-by-construction without requiring clean-slate software development, or replacing the software code base entirely. To accomplish its goals, the V-SPELLS program seeks to leverage a combination of novel concepts in program understanding and verification, as well as recent developments in Domain Specific Languages (DSL) – or computer languages that are specialized for a particular application domain, such as SQL for database queries or P4 for network switches and routers – and composable system architectures for production systems at scale.

To accomplish these goals, the V-SPELLS program will leverage a combination of novel concepts in program understanding and verification, as well as recent developments in domain specific languages and composable system architectures for production systems at scale.

Research efforts under V-SPELLS will focus on three primary areas of exploration.

1. The first will explore the development of methods and tools to create the capability to iteratively and interactively understand software components found in large legacy code bases and how they fit within the context of the larger system. Automated program understanding to infer architectural structure, assumptions, and dependencies in a legacy source code base, enabling its decomposition into components with explicit modular structure, interfaces, dependencies, and constraints. Recovery of domain abstractions and models from legacy code bases, in succinct and expressive representations suitable for programming functional component enhancements or replacements that are safely composable with the existing systems.

To do this, the target V-SPELLS tools will enable developers to semi-automatically derive representations or expressions, such as DSLs, of domain structures and domain logic from the source code. In certain situations, lifting or converting legacy code to DSLs has improved the performance of a system by orders of magnitude. V-SPELLS aims to take the legacy code base of our existing software and expand and abstract it to DSLs where it can be safely and tractably modified. Through this approach, the V-SPELLS program seeks to deliver the power and safety guarantees of formal methods into the hands of domain-expert software developers who are not experts in formal verification of software.

2. The second area of research will focus on creating the capability for regular developers to quickly create new verified component replacements and enhancements to the legacy software that safely compose with the rest of the system. Matching known and extracted domain abstractions and models with legacy code, lifting of legacy code to succinct, enhanceable, safely composable, and inter-operating representations, and automated specification inference leveraging such representation. Provably safe composition of enhancements with the rest of the system.This includes the creation of an integrated environment that enables developers to re-implement, re-engineer, and enhance specific components of a system in a combination of DSLs and models derived from the first area of research on the program.

3. Finally, a third area of research will focus on developing processes, designs, standards, and tools to help overcome any performance reductions and/or security concerns generated by the methods and tools created within the first two research areas. This research area will also explore ways of ensuring the enhancements to the legacy code will operate on modern hardware.

Overcoming performance reduction due to added layers of abstraction with novel verified crosslayer optimization and distribution techniques (“verified stack flattening and distribution”). Development of non-brittle and granular rules for composable representation, packaging, and transformation of software verification proofs that support distribution and orchestration of verified programs.

References and Resources also include:

https://beta.sam.gov/opp/30fda7e00b4f44a3a2aaa49ef26bb512/view