Summary
The DoD has a critical need for enhancing and replacing components of existing software with more secure and more performant code.
This includes 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, introducing enhancements or replacements into large legacy code bases carries a high risk that new code will not safely compose with the rest of the system. Verified programming methodologies for creating software that is correct-by-construction are currently not effective for lowering this risk, because they focus on clean-slate software construction, assume an existing formal specification that is typically not available for a legacy system, and require formal methods expertise typically not accessible to developers.
The goal of the V-SPELLS program is to create a developer-accessible capability for piece-by-piece enhancement of software components with new verified code that is both correct-by-construction and compatible-by-construction, i.e., safely composable with the rest of the system.
V-SPELLS will create practical tools for developers to gain benefits of formal software verification in incremental software (re)engineering rather than only in clean-slate introduction. V-SPELLS tools will enable developers to deliver assured incremental modernization of legacy systems in a manner that leverages verification technologies and reduces rather than raises risk. V-SPELLS aims to radically broaden adoption of software verification by enabling incremental introduction of superior technologies into systems that cannot be re-designed from scratch and replaced as a whole.
To accomplish these goals, the V-SPELLS program will leverage a combination of novel concepts in program understanding and verification, as well as recent developments in domain specific languages and composable system architectures for production systems at scale. The program seeks breakthroughs in and novel approaches to the following technical challenges, including, but not limited to:
- Automated program understanding to infer architectural structure, assumptions, and dependencies in a legacy source code base, enabling its decomposition into components with explicit modular structure, interfaces, dependencies, and constraints. Recovery of domain abstractions and models from legacy code bases, in succinct and expressive representations suitable for programming functional component enhancements or replacements that are safely composable with the existing systems.
- Matching known and extracted domain abstractions and models with legacy code, lifting of legacy code to succinct, enhanceable, safely composable, and inter-operating representations, and automated specification inference leveraging such representation. Provably safe composition of enhancements with the rest of the system.
- Overcoming performance reduction due to added layers of abstraction with novel verified cross-layer optimization and distribution techniques (“verified stack flattening and distribution”). Development of non-brittle and granular rules for composable representation, packaging, and transformation of software verification proofs that support distribution and orchestration of verified programs.