Reverse engineering: Difference between revisions

From miki
Jump to navigation Jump to search
Line 24: Line 24:
* [https://pythonhosted.org/arybo/index.html Arybo], a tool that gives a bit-level symbolic representation of expressions involving various types of operations on bit vectors
* [https://pythonhosted.org/arybo/index.html Arybo], a tool that gives a bit-level symbolic representation of expressions involving various types of operations on bit vectors
:This tool generates mixed-boolean arithmetics (MBA) expressions...
:This tool generates mixed-boolean arithmetics (MBA) expressions...
* [[z3], a theorem prover from Microsoft Research.
* [[z3]], a theorem prover from Microsoft Research.
:Can be used to solve obfuscated expression, solve polynomial expressions under constraints...
:Can be used to solve obfuscated expression, solve polynomial expressions under constraints...
* [https://github.com/quarkslab/sspam SSPAM], Symbolic Simplification with PAttern Matching.
* [https://github.com/quarkslab/sspam SSPAM], Symbolic Simplification with PAttern Matching.

Revision as of 18:59, 5 October 2019

Tools

Debuggers:

  • GDB
  • LLDB
  • windbg
  • Ghidra, an open-source software reverse-engineering tool developped by the NSA.
Similar to IDA / IDA Pro, but free and open source.
  • IDA / IDA Pro

Simulators / emulators:

  • QEMU
  • Unicorn, is a lightweight multi-platform, multi-architecture CPU emulator framework.
Based on QEMU, allows for running binary from any CPU with nice Python integration.
  • capstone, a lightweight multi-platform, multi-architecture disassembly framework.

Binary instrumentation framework:

  • Frida
  • DynamoRio
  • QBDI, open-sourc equivalent of DynamoRio.

Reverse analysis tools:

  • Triton, a dynamic binary analysis (DBA) framework.
This tool can reverse state machines or obfuscated code using virtual machine.
  • Arybo, a tool that gives a bit-level symbolic representation of expressions involving various types of operations on bit vectors
This tool generates mixed-boolean arithmetics (MBA) expressions...
  • z3, a theorem prover from Microsoft Research.
Can be used to solve obfuscated expression, solve polynomial expressions under constraints...
  • SSPAM, Symbolic Simplification with PAttern Matching.
Can simplify complex arithmetic expressions using pattern matching.

Obfuscation tools:

  • OLLVM (old)
  • Tigress