JAIST Logic@JAIST

Malware techniques and its pushdown model checking

  • Nguyen Minh Hai
  • VNU-HCMC/HCMUT
Date: 2014/08/22 (Fri) 13:30 to 15:00
Place: JAIST IS school Seminar room (6F)
Group: Research Center for Software Verification

Malware is distributed as binary, and its slickering techniques and the difficulty of its detection come from "data = code" nature on memory.

The first half of the talk overviews typical malware techniques, consisting of 3 steps: intrusion, infection, and concealment. We focus on malware for Windows on x86 (32 bits). Intrusion correspond to the protection of Win 95 / XP / 7. After short summary of infection, we mention recent polymorphic techniques for concealment, such as mutation engine.

The latter half introduces our current collaboration (between HCMUT and JAIST) on binary analysis, which consists of two steps: pushdown model generation and pushdown model checking. Different from high-level programming languages, it is not easy to generate a model for binary codes. For instance, (1) disassembly is decided dynamically, (2) jump destination addresses can be values on registers or memory (indirect jumps), (3) binary code loaded on memory can be dynamically modified (self-modification). We tackle this problem with on-the-fly model generation using concolic testing on a binary emulater, which are implemented as BE-PUM (Binary Emulator for PUshdown Model generation). We report our current experimantal results of pushdown model generation (including 1700 malwares from VX Heaven), and our ongoing investigation on its weighted pushdown model checking.

Contact nao-aoki