Department of Computer, Control and Management Engineering

Symbolic execution is a program analysis technique that aims to automatically identify interesting inputs for an application, using them to generate program executions covering different parts of the code. It is widely used in the context of vulnerability discovery and reverse engineering. In this paper we present SENINJA, a symbolic execution plugin for the BINARYNINJA disassembler. The tool allows the user to perform symbolic execution analyses directly within the user interface of the disassembler, and can be used to support a variety of reverse engineering tasks.