Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS)
Abstract
The Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program is creating methods and tools to recover succinct models of domain data abstractions and logic from source code, add enhancements to the models, and convert them to performant new component implementations verified to be compatible and secure. DoD has a critical need for replacing or reworking components of existing software with more secure and more performant code, including cases where a key performance or security benefit comes from moving parts of the software to new hardware, such as utilizing hardware accelerators, isolation enclaves, offload processors, and distributed computation. However, at present, enhancing legacy software components faces high risk that the new software will not be fully compatible with the existing larger environment. Moreover, verified software is currently written from scratch, starting with a formal specification, rather than incrementally added to a system as provably compatible enhancements. V-SPELLS will address these problems by combining novel concepts in verified programming with recent developments in domain specific languages (DSLs) and systems architecture. V-SPELLS aims to enable piecewise, compatible-by-construction improvement of software components in legacy DoD systems, providing to incremental software (re)engineering the benefits of formal software verification currently available only to clean-slate development efforts.
Document Details
- Document Type
- Accomplishment
- Publication Date
- Oct 01, 2023
- Source ID
- 074cfe081d1401bdab17ffeaca0b8b65