Formal-Verification-Based Tool for Deobfuscation of Tamper-Proofed Software

The rapid increase in the use of the Internet in many aspects of our lives has led to an explosive growth in the spread of malware such as computer worms, viruses, and trojans. Security tools typically examine software for the presence of malware either by looking for specific byte signatures, or (more recently) by analyzing the candidate binary’s internal logic. However, it is surprisingly easy to use binary obfuscation to fool current binary analysis tools into making errors that can hide malicious content. Furthermore, tamper-proofing techniques can be used to hinder or prevent dynamic monitoring of such software. The combination of code obfuscation and tamper-proofing can, therefore, make software opaque to security analysis tools. This project aims to address this situation by developing sophisticated techniques for deobfuscating binaries as well as identifying and working around tamper-proofing and anti-monitoring code intended to prevent dynamic monitoring. In order to do this efficiently without affecting program semantics, we will extend and combine SAT-based formal verification procedures developed by one of the co-PIs (Velev) with low-level binary analysis and deobfuscation techniques developed by the other co-PI (Debray). We will leverage and extend existing binary manipulation software developed by Debray to achieve this.