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, addressing issues encountered in the Cyber Assured Systems Engineering (CASE) program, budgeted within this PE and Project, will create 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 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, replacing legacy software components with technologically superior ones for improved performance or security faces high risk that the new software, despite being proven correct according to a specification, 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 technology will iteratively and interactively leverage automated program understanding to semi-automatically derive a DSL for the targeted component of a large code base, translate the code for the component into this DSL while concurrently inferring its specification within the larger environment, and then generate, optimize, and distribute executable artifacts across the system, creating and validating relevant proofs. 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, 2022
- Source ID
- 8f8ea50a22be70185c9ef8c8ef353a74