Analyzing x86 Executables with Jakstab

Date: Thursday, June 09, 2011
Speaker: Johannes Kinder
Venue: IST Austria
Notes:

Mondi 2

Binary executables are a promising analysis target in many scenarios, ranging from bug finding over execution time analysis to malware detection. Still, problems such as indirect control flow and the lack of types make it hard to adapt traditional static analysis tool-chains to binaries. While earlier attempts mostly use heuristics to preprocess binaries into a format understandable by static analyzers, we argue for the integration of disassembly, control flow reconstruction, and static analysis in a unified process. This enables sound static analysis of binaries, without fragile and generally unsound preprocessing by heuristic disassemblers.

The result of our work is the novel binary analysis tool Jakstab, which supports classic data flow analysis with domains such as intervals, but also path sensitive, bounded model checking style explicit analysis. Jakstab works directly on binaries and disassembles instructions on demand while exploring the program’s state space. We demonstrate its practical usefulness in case studies on open and closed source Windows drivers and system tools. In ongoing work, we are extending our framework to support under-approximate information from execution traces to recover from unknown control flow due to imprecision of the analysis.

Posted in RiSE Seminar