TUM Logo

Compiler-Based Symbolic Execution on Hypervisors

Compiler-Based Symbolic Execution on Hypervisors

Supervisor(s): Manuel Andreas
Status: inprogress
Topic: Others
Type of Thesis: Masterthesis Bachelorthesis Guided Research


Topic Description

The goal of this thesis is to enable efficient symbolic execution on common hypervisors (Xen, KVM) in order to further enhance a hypervisor fuzzer that is currently being developed at the chair. For this we look towards building our own compiler instrumentation pass (e.g. on top of LLVM) or porting an existing symbolic executor such as SymCC.


  • Very confident programming in C
  • Comfortable with reading and writing x86 assembly
  • Familiarity with OS and virtualization concepts
  • Familiarity with fuzzing, e.g. AFL
  • Interest in diving into LLVM (and therefore C++)
  • Excited about discovering CVEs


Manuel Andreas