Bounded model checking for ROP gadget chaining

Allgemein

Betreuer: Tim Blazytko

Beginn: as soon as pos­si­ble

Dauer: 6 months

Weitere Details:

Beschreibung

Return-oriented programming (ROP) is an exploitation primitive in which an attacker executes a chain of gadgets which end in return instructions. Manual ROP chain generation is laborious. For this reason, a lot of research was done to automatise this task.

Bounded model checking is a formal technique that uses SMT solvers to prove properties of software. The key idea is to generate a first-order logic formula that represents the program semantics and the property to prove. First experiments indicate that it works efficiently for path selection on a control-flow graph.

Modelling ROP chain generation as a path selection problem for bounded model checking might be a flexible approach, since it is possible to define the initial and final memory layout as constraints. In other words, the ROP chain can be automatically generated in dependence on the memory context that is defined by an attacker.

The thesis’ goal is to model and evaluate ROP gadget chaining as a path selection problem for bounded model checking. For this, a framework for bounded model checking on the binary level will be provided. In addition, the performance of this approach has to be evaluated. For that purpose, the following steps are required:

  • building a control-flow graph from ROP gadgets
  • refining the control flow encoding for path selection
  • modelling the return instruction semantics in SMT formulas
  • evaluating correctness and performance

Voraussetzungen

  • good understanding of the x86 64 architecture
  • basic knowledge of SMT solvers is helpful
  • enjoying slightly more formal aspects of reverse engineering and exploitation