ReSMT: An SMT-Based Tool for Reverse Engineering

TL;DR

ReSMT is an automated tool that converts obfuscated assembly code into logical assertions and uses SMT solving to facilitate reverse engineering, making the process more accessible and effective against complex obfuscation.

Contribution

The paper introduces ReSMT, a novel automated approach that leverages SMT solving for reverse engineering obfuscated code, reducing the need for specialized skills.

Findings

Successfully handled complex obfuscated code in case studies

Automated approach reduces manual reverse engineering effort

Demonstrated effectiveness in solving reverse-engineering queries

Abstract

Software obfuscation techniques make code more difficult to understand, without changing its functionality. Such techniques are often used by authors of malicious software to avoid detection. Reverse Engineering of obfuscated code, i.e., the process of overcoming obfuscation and answering questions about the functionality of the code, is notoriously difficult; and while various tools and methods exist for this purpose, the process remains complex and slow, especially when dealing with layered or customized obfuscation techniques. Here, we present a novel, automated tool for addressing some of the challenges in reverse engineering of obfuscated code. Our tool, called ReSMT, converts the obfuscated assembly code into a complex system of logical assertions that represent the code functionality, and then applies SMT solving and simulation tools to inspect the obfuscated code's execution. The approach is mostly automatic, alleviating the need for highly specialized deobfuscation skills. In an elaborate case study that we conducted, ReSMT successfully tackled complex obfuscated code, and was able to solve reverse-engineering queries about it. We believe that these results showcase the potential and usefulness of our proposed approach.