Limitations

BAP Limitations

The Z3 theorem prover currently has broken OCaml bindings. Attempts by myself at building these bindings using the BAP supplied build procedure (see $BAP/solvers/getz3.sh in the BAP distribution) have not been successful, so Z3 is currently considered unsupported.

The Binary Analysis Platform only has support for x86 (32 bit) and AMD processors.

For x86, the FPU and MMX instructions have not been modelled in BAP IL (these translate to BAP IL unknowns). Moreover, INT instructions are currently translated to BAP IL special instructions. By accessing the kernel code within a Volatility image, this latter restriction can be overcome.

BAP appears to be primarily designed(?) to operate on code traces/straight line code (e.g. as extracted by PIN). As a result, a number of program analysis techniques have implementations that inadequately handle looping conditions (e.g. WPs and VSA) - these are partially handled using the rm_cycles() and unroll(num) BAP commands.

Libbap Limitations

Currently, compiling Volatility plugins written in OCaml requires ocaml/Makefile and setup.py to be modified to include the code (obviously, libbap then needs to be rebuilt!).