Generating Requirements Evidence with Analysis and System-level Enforcement

The Generating Requirements Evidence with Analysis and System-level Enforcement (GREASE) project will develop a static binary verifier with an optional human-in-the-loop testing facility that generates evidence that COTS software components satisfy their requirements. The GREASE tool will reduce the time required for both (1) the safe and high-assurance integration of COTS components into systems, and (2) the time required to build assurance cases for certification of systems that incorporate COTS components. By analyzing binaries, the verifier will be able to build assurance cases even when manufacturers are unwilling or unable to provide source code. The GREASE tool will statically verify that COTS software binaries satisfy their requirements by lifting them into an intermediate representation suitable for analysis, converting requirements into static assertions, and verifying that the assertions hold on all program executions through under-constrained symbolic execution. This approach provides a strong combination of scalability, precision, and explainability. The project will explore applications of human-in-the-loop testing, where the GREASE tool will generate augmented binaries to (1) build assurance in cases where static verification is not possible, and (2) augment the static verification with additional information to improve its results.