A symbolic execution engine for amd64 binaries presented at ekoparty 2013

by Felipe Manzano,

Summary : Current popular approaches to bug hunting largely rely on the use of fuzzing, it's effectiveness is tightly coupled with the quality and number of the harvested base cases and/or the previous knowledge of the format/protocol. We present an implementation of a generic technique that overcomes these limitations: symbolic execution. The presentation showcase a Python tool that enables the symbolic execution of stripped Linux Intel binaries. This tool automatically generates interesting test cases that exercise different traces of the application without using its source code nor any knowledge of its inner workings. The attendees will get the overview of symbolic execution and the technical challenges in achieving amd64 emulation in Python with the aim of searching for bugs.