U.S. military researchers are being seeking help from the private industrial sector in order to upgrade components of mission-critical software for aerospace and defense applications with more secure and higher-performing code.
Officials of the U.S. Defense Advanced Research Projects Agency (DARPA) in Arlington, Va., will brief industry in an online webinar from noon to 4 p.m. eastern time on 29 July 2020 concerning the upcoming Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) project.
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.
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.
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.
The V-SPELLS proposers day on 29 July seeks to familiarize participants with DARPA’s interest in software verification and assurance by enabling piecewise, compatible-by-construction enhancement of software components in legacy military systems.
Companies interested in attending the V-SPELLS webinar should register online at www.schafertmd.com/DARPA/I2O/V-SPELLS/PD/2020/July/ no later than 22 July 2020.