Generating Requirements Evidence with Analysis and System-level Enforcement (GREASE)

The Generating Requirements Evidence with Analysis and System-level Enforcement (GREASE) project will develop a static binary verifier that generates evidence that COTS software components satisfy their requirements. The GREASE tool will accelerate both (1) the safe and high-assurance integration of COTS components into systems, and (2) the generation of assurance cases for the 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. Requirements will be described in a constrained natural language, making GREASE suitable for use by auditors without a reverse engineering background. The project will optionally 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.