Quick Start

Jakstab is invoked via the command line, it comes with both a Windows and a Unix shell script for setting the correct classpath. The package contains a set of examples for unit testing, you can try it out on those by running

  jakstab -m input/helloworld.exe

for a default Bounded Address Tracking run on the helloworld executable, or by running

  jakstab -m input/jumptable.exe --cpa xfi

for analyzing a jumptable example with Bounded Address Tracking, forward expression substitution, and interval analysis. It is still a research prototype, so all interfaces are likely to change with new versions without further notice. Documentation is still sparse, but will hopefully improve over time.

The analyses (CPAs) that should be working correctly are:

• Bounded Address Tracking (x)
• Constant Propagation (c)
• Forward Expression Substitution (f)
• Interval Analysis (i)
• Call Stack Analysis (s)
• K-Set Analysis (k)

Publications

The CAV 2008 tool paper describes an early implementation of Jakstab, which was based on iterative constant propagation and branch resolution:

• Johannes Kinder, Helmut Veith. Jakstab: A Static Analysis Platform for Binaries. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), vol. 5123, Lecture Notes in Computer Science, Springer, July 2008, pp. 423–427. [ DOI ]  [ PDF ] 
   

Our VMCAI 2009 paper introduces a generic framework for disassembly and control flow reconstruction guided by data flow analysis and defines the theoretical background for Jakstab. The framework is not fixed in its choice of domain, but allows to combine control flow reconstruction with any data flow analysis that provides abstract evaluation of expressions:

• Johannes Kinder, Helmut Veith, Florian Zuleger. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009), vol. 5403, Lecture Notes in Computer Science, Springer, January 2009, pp. 214–228. [ DOI ]  [ PDF ] 
   

In FMCAD 2010, we give an overview on the Jakstab architecture and describe Bounded Address Tracking, a practical abstract domain used for control flow reconstruction and verification of API usage specifications on device driver binaries:

• Johannes Kinder, Helmut Veith. Precise Static Analysis of Untrusted Driver Binaries. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), October 2010, pp. 43–50. [ PDF ]