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.