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

Award Information
Agency: Department of Defense
Branch: Air Force
Contract: FA8650-06-M-8081
Agency Tracking Number: O064-NC5-1006
Amount: $100,000.00
Phase: Phase I
Program: STTR
Awards Year: 2006
Solicitation Year: 2006
Solicitation Topic Code: OSD06-NC5
Solicitation Number: N/A
Small Business Information
6157 N Sheridan Rd, Suite16M, Chicago, IL, 60660
DUNS: 361627933
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Miroslav Velev
 President, CEO
 (773) 856-6633
 miroslav.velev@aries-da.com
Business Contact
 Miroslav Velev
Title: President, CEO
Phone: (773) 856-6633
Email: miroslav.velev@aries-da.com
Research Institution
 UNIV. OF ARIZONA
 Saumya K Debray
 Department of Computer Science, University of Arizona
Tucson, AZ, 85721
 (520) 621-4527
 Nonprofit college or university
Abstract
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.

* Information listed above is at the time of submission. *

Agency Micro-sites

SBA logo
Department of Agriculture logo
Department of Commerce logo
Department of Defense logo
Department of Education logo
Department of Energy logo
Department of Health and Human Services logo
Department of Homeland Security logo
Department of Transportation logo
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government