Jakstab: A Static Analysis Platform for Binaries

Lecture notes in computer sciencePublished 12 August 2008Open access

Johannes Kinder, Helmut Veith

Citations135

TL;DR

This work presents their fully configurable binary analysis platform Jakstab, which resolves indirect branches by multiple rounds of disassembly interleaved with dataflow analysis, and demonstrates that this iterative disassembling strategy achieves better results than the state-of-the-art tool IDA Pro.

Abstract

For processing compiled code, model checkers require accurate model extraction from binaries. We present our fully configurable binary analysis platform Jakstab, which resolves indirect branches by multiple rounds of disassembly interleaved with dataflow analysis. We demonstrate that this iterative disassembling strategy achieves better results than the state-of-the-art tool IDA Pro.

Keywords

Computer Science

Obfuscation of executable code to improve resistance to static disassembly

596 Citations2003Cullen Linn, Saumya Debray

Experimental results indicate that significant portions of executables that have been obfuscated using the techniques described are disassembled incorrectly, thereby showing the efficacy of the methods.

Lecture notes in computer scienceAnalyzing Memory Accesses in x86 Executables

370 Citations2004Gogul Balakrishnan, Thomas Reps

The aim of the work is to recover intermediate representations that are similar to those that can be created for a program written in a high-level language by static-analysis algorithms for analyzing x86 executables.

ACM Transactions on Programming Languages and SystemsWYSINWYX

274 Citations2010Gogul Balakrishnan, Thomas Reps

The article presents the algorithms that were developed, explains how they are used to recover Intermediate Representations from executables that are similar to the IRs that would be available if one started from source code, and describes their application in the context of program understanding and automated bug hunting.

View PDF

SYNERGY

251 Citations2006Bhargav S. Gulavani, Thomas A. Henzinger +3 more

This paper proposes a new algorithm, Synergy, which combines testing and verification, and unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.

Lecture notes in computer scienceDetecting Malicious Code by Model Checking

177 Citations2005Johannes Kinder, Stefan Katzenbeisser +2 more

This paper introduces the specification language CTPL (Computation Tree Predicate Logic) which extends the well-known logic CTL, and describes an efficient model checking algorithm which is able to detect a large number of worm variants with a single specification.

Reverse compilation techniques

154 Citations1994Cristina Cifuentes

Techniques for writing reverse compilers or decompilers are presented in this thesis, based on compiler and optimization theory, and applied to decompilation in a unique way; these techniques have never before been published.

Lecture notes in computer scienceWYSINWYX: What You See Is Not What You eXecute

153 Citations2008Gogul Balakrishnan, Thomas Reps +2 more

Using a decompiler for real-world source recovery

62 Citations2005M. Van Emmerik, T. Waddington

This work describes the experience gained from applying a native executable decompiler, assisted by a commercial disassembler and hand editing, to a real-world Windows-based application.

Specifying the semantics of machine instructions

43 Citations2002Cristina Cifuentes, Shane Sendall

The design process used to develop a semantic specification language, SSL, to integrate into a retargetable binary translation framework, and the techniques described herein are suitable not just to binary translators but also to machine-code manipulation tools such as optimizing compilers, binary profilers, instrumentors, and binary debuggers.

View PDF

Lecture notes in computer scienceAnalyzing Stripped Device-Driver Executables

29 Citations2008Gogul Balakrishnan, Thomas Reps

This work represents the first known application of automatic program verification/analysis to stripped industrial executables, and allows one to check that an executable does not violate known API usage rules (rather than simply trusting that the implementation is correct).