ARLINGTON, Va. – U.S. military researchers are asking industry for enabling technologies to upgrade legacy military software with secure and high-performance code.
Officials of the U.S. Defense Advanced Research Projects Agency (DARPA) in Arlington, Va., issued a broad agency announcement (HR001120S0058) on 24 July for the Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program. DARPA briefed industry on V-SPELLS last Wednesday.
The V-SPELLS software verification and assurance project seeks to enable piecewise, compatible-by-construction enhancement of software components in legacy military systems, and to create methods and tools to recover succinct models of domain data abstractions and logic from the source code.
The aim is to enhance military software at the level and convert these models to component implementations that are verified to be secure and compatible with the legacy systems to which they belong.
The U.S. military has a critical need for enhancing and replacing components of existing software with more secure and more performant code, DARPA officials explain.p>
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.
Introducing enhancements or replacements into large legacy code, however, carries a high risk that new code will not safely compose with the rest of the system.
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.
The goal of the V-SPELLS program is to create a developer-accessible capability to enhance existing components piece-by-piece and ensure these enhancements are compatible with verified code.
V-SPELLS seeks to create tools for developers to verify re-engineered software components incrementally, rather than only in clean-slate introduction. V-SPELLS aims to radically broaden adoption of software verification by introducing superior technologies into systems that cannot be re-designed from scratch and replaced as a whole.
The program seeks software technology breakthroughs in automated program understanding; matching known and extracted domain abstractions and models with legacy code; and overcoming performance reduction due to added layers of abstraction.
Automated program understanding seeks to infer architectural structure, assumptions, and dependencies in a legacy source code base, and enable its decomposition into components with explicit modular structure, interfaces, dependencies, and constraints.
Related: Trusted computing: an overview
Matching known and extracted domain abstractions and models with legacy code, seeks to lift legacy code to succinct, enhanceable, safely-composable, and inter-operating representations.
Overcoming performance reduction due to added layers of abstraction seeks to create new verified cross-layer optimization and distribution techniques, by developing of non-brittle and granular rules for composable representation, packaging, and transformation of software verification proofs.
V-SPELLS seeks technology breakthroughs in automated program understanding to infer architectural structure, assumptions, and dependencies in a legacy source code base; matching known and extracted domain abstractions and models with legacy code; and overcoming performance reduction from added layers of abstraction.
Software engineers today struggle to understand legacy code, DARPA researchers explain, because it tends to entangle application domain logic and performance optimizations for past hardware that remain in the code despite being no longer useful. Component specifications often aren't available.
Related: Raytheon to provide encryption and cyber security upgrades for Patriot missile system
As a result, critical systems can be locked into obsolete hardware and software components, which makes capability upgrades difficult, if not impossible, and today's software engineering tools and standards offer meager support.
The V-SPELLS program seeks to combine concepts in verified programming with recent developments in domain-specific software languages and composable system architectures in production systems at scale.
The V-SPELLS program will last for four years, and is organized into three phases: 18-month phases one and two, and a 12-month phase three. The project also has four technical areas: automated, iterative interactive program understanding; compositional DSL programming; verified layer flattening and distribution; and demonstration and evaluation.
Automated, iterative, interactive program understanding will develop methods and tools for automated, iterative, interactive program understanding of software components in large code bases, based on extraction, matching, and application of domain-specific structures, expressions, and models.
Compositional DSL programming focuses on enabling regular developers to create new verified component replacements and enhancements quickly that compose with the rest of the system safely.
Verified layer flattening and distribution focuses on processes, designs, standards, and tools for creating safe and high-performance executable artifacts for the composable DSL-based enhancements and replacements.
Demonstration and evaluation will develop evaluations for resulting capabilities, and come up with a testing approach that enables the incremental development, demonstration, evaluation, and eventual DOD use of V-SPELLS capabilities.
Related: BAE Systems to provide software engineering support for U.S. Army intelligence systems
DARPA researchers say they expect to make several contract awards for automated, iterative interactive program understanding; compositional DSL programming; and verified layer flattening and distribution. DARPA will make one contract award for demonstration and evaluation.
Companies interested should upload proposals no later than 9 Sept. 2020 to the DARPA BAA website at https://baa.darpa.mil.
Email questions or concerns to Sergey Bratus, the V-SPELLS program manager, at [email protected]. More information is online at https://beta.sam.gov/opp/7dc5798bf5e74d8aa3df767edd3e0815/view.
