Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

ReSMT: An SMT-Based Tool for Reverse Engineering

Nir Somech, Guy Katz

TL;DR

This paper introduces ReSMT, an automated SMT-based framework for reverse engineering obfuscated binaries. It converts obfuscated assembly to a platform-independent intermediate language (REIL), encodes semantics and a reverse-engineering goal into SMT constraints, and solves them with an SMT backend to recover inputs that reveal intended behavior. The approach targets layered and customized obfuscation, demonstrated through a case study where increasingly complex PELOCK obfuscations are automatically resolved to reveal a hidden key. Results show ReSMT outperforms manual analysis and a contemporary AI model in finding the key within minutes for heavily obfuscated variants, underscoring its potential for malware analysis and automated RE workflows.

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.

ReSMT: An SMT-Based Tool for Reverse Engineering

TL;DR

This paper introduces ReSMT, an automated SMT-based framework for reverse engineering obfuscated binaries. It converts obfuscated assembly to a platform-independent intermediate language (REIL), encodes semantics and a reverse-engineering goal into SMT constraints, and solves them with an SMT backend to recover inputs that reveal intended behavior. The approach targets layered and customized obfuscation, demonstrated through a case study where increasingly complex PELOCK obfuscations are automatically resolved to reveal a hidden key. Results show ReSMT outperforms manual analysis and a contemporary AI model in finding the key within minutes for heavily obfuscated variants, underscoring its potential for malware analysis and automated RE workflows.

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.
Paper Structure (19 sections, 2 equations, 19 figures, 1 table)

This paper contains 19 sections, 2 equations, 19 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Our Approach: An SMT-Based Solution
  4. ReSMT: Features and Design
  5. Main Features
  6. Tool Design
  7. Case Study: Find the Key
  8. Setup
  9. Reverse-Engineering $P_0,\ldots,P_6$
  10. Related Work
  11. Conclusion & Future Work
  12. Applying the ReSMT Pipeline: A Thorough Description
  13. The Naive solution: Brute Force
  14. Solving with ReSMT
  15. Deobfuscation
  16. ...and 4 more sections

Figures (19)

  • Figure 1: Example of java function code obfuscation: original code (left) vs. obfuscated code (right).
  • Figure 2: Original source code, and its obfuscated counterpart, after renaming.
  • Figure 3: Simple bytecode and its corresponding assembly instructions.
  • Figure 4: Assembly code (on the left), and its IL representation on the right.
  • Figure 5: Assembly code.
  • ...and 14 more figures