Automated analysis of programs (source/binary) for critical properties


Explanation: Critical properties desired of a binary (or source) program are specified precisely. The subject program is then analyzed against a model embodying the semantics of the (hardware/software) execution environment to verify that the desired properties are present.

Vulnerabilities addressed: Addresses any vulnerability countered by the specified properties.

Developer resources required: Requires developers capable of specifying the properties desired of the implementation in the language accepted by the verification tools involved, or access to experts with this ability.

Evaluator resources required: Requires the ability to generate and review output of verification tools applied to the programs analyzed.