Modelling CPUs in SMT solvers

Allgemein

Betreuer: Tim Blazytko

Beginn: as soon as possible

Dauer: 6 months

Weitere Details:

Beschreibung

SMT solvers decide formulas of first-order logic that are, in the general case, at least NP-complete. However, SMT solvers are known to perform efficiently on many real-world problems. For this reason, they are widely used in modern program analysis.

Modelling a CPU connotes modelling a CPU’s instruction cycle (fetch, decode, execute) in an SMT formula. Then, the SMT solver implicitly handles techniques such as disassembly, control flow con- struction, loop unrolling and static single assignment (SSA). As a consequence, the SMT solver can be used to decide reachability of code parts, to consider self-modifying code and to predict indirect jumps.

The thesis’ goal is to model the x86 64 architecture in an SMT solver. In addition, the performance of this approach has to be evaluated. For that purpose, the following steps are required:

  • modelling a generic CPU
  • modelling the instruction decoding of the x86 64 architecture
  • modelling the instruction semantics for a subset of the x86 64 architecture
  • evaluating correctness and performance

Voraussetzungen

  • good understanding of the x86 64 architecture
  • enjoying slightly more formal aspects of reverse engineering