Phase II Amount
$1,200,374
Kestrel Technology will develop CLAIM: Corpus- and Logic-based Automated Identification of Malware, which will pioneer a novel approach to malware detection and identification using a Big Code corpus of known malicious programs. CLAIM will work by performing a logical match (based on semantics and functionality, not signatures) between unknown, possibly malicious programs and known malicious programs from the corpus. The match will be performed by applying our technique of lifting-into-logic to both programs (x86 binaries), using a model of the x86 instruction semantics, and then applying our equivalence checking techniques to detect equivalent malicious functionality. When malice is detected, CLAIM will produce a certificate of malicious behavior, showing in detail how the new program's functionality corresponds to known malicious code in the corpus. All of this is enabled by the Big Code corpus of known malware. The corpus allows the difficult problem of malware detection to be reduced to the more tractable problem of equivalence checking. In turn, this equivalence checking problem is made tractable by our advanced techniques, including lifting into logic and the strategies used in the Axe Equivalence Checker (suitably adapted to handle x86 malware).
