Polymalys
Polymalys: Polyhedra-based Memory Analysis.
- Version XX for Otawa XX
Author
Clement Ballabriga Clement.Ballabriga@nospamuniv-lille.fr
License: GPL 2.1 or higher.
Please remove "nospam" from the email address.
Introduction
Polymalys is a tool for static analysis of binary code. It discovers linear relations between data locations (i.e. memory locations as well as registers) of the code. The analysis relies on abstract interpretation using a polyhedra-based abstract domain. The current implementation exploits the discovered linear relations to compute upper bounds to loop iterations. For more information on the underlying theory, refer to [1].
Requirements
-
Parma Polyhedra Library (PPL): http://bugseng.com/products/ppl/
-
For testing, you will need an ARM cross-compiler
First, install all required dependencies. On debian/ubuntu:
sudo apt install build-essential python2 git cmake flex bison libxml2-dev libxslt-dev ocaml gcc-arm-none-eabi
To prevent compatibility issues, Polymalys is linked to a specific version of OTAWA 2, which is bundled in the Polymalys directory.
Compiling:
make
Installing (in home directory, no root required):
make install
Automated tests (optionnal)
make test
Testing with a source code target program:
cd tests
./do.sh <filename> # where <filename>.c is a C program
Testing with a binary target program:
cd tests
./poly.sh <binary> [<optional function name, defaults to main>] # where <binary> is an ARM binary program
Using in your program:
Read tests/poly.cpp
Future works
- Use discovered linear relations for other static analyses: out-of-stack accesses detection, dead-code detection, ...
- Inter-procedural analysis
- Support for integer wrap/overflow
- Loops conditions with equality tests (instead of inequality) currently have pessimistic bounds
- We currently assume that each memory access has 32bits-size, and is 32bits-aligned
- Lots of speed optimization needs to be done
References
[1] Ballabriga, C., Forget, J., Gonnord, L., Lipari, G. and Ruiz, J., 2019, January. Static Analysis Of Binary Code With Memory Indirections Using Polyhedra. In International Conference on Verification, Model Checking, and Abstract Interpretation (pp. 114-135).