Program aims to enable incremental software repair and enhancement with verified, assured code on existing systems
Jul 30, 2020
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. 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. Further, these methods assume an existing formal specification that is typically not available for a legacy system, and they require a certain level of expertise in formal methods not readily found in most 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’s Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program aims 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.
Research efforts under V-SPELLS will focus on three primary areas of exploration. 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. 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.
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. 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.
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.
A Broad Agency Announcement solicitation with full program details is available here: https://beta.sam.gov/opp/7dc5798bf5e74d8aa3df767edd3e0815/view?keywords=&sort=-modifiedDate&index=&is_active=true&page=1&organization_id=300000412&date_filter_index=0&inactive_filter_values=false.
# # #
Media with inquiries should contact DARPA Public Affairs at outreach@darpa.mil
Associated images posted on www.darpa.mil and video posted at www.youtube.com/darpatv may be reused according to the terms of the DARPA User Agreement, available here: http://go.usa.gov/cuTXR.