Commit 7b495c0f authored by Ballabriga Clément's avatar Ballabriga Clément
Browse files

Merge branch 'public' of gitlab.cristal.univ-lille.fr:otawa-plugins/polymalys into public

parents 7c0de1d5 27897b52
# 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/
......@@ -87,17 +112,21 @@ cd tests
Read `tests/poly.cpp`
## Known limitations (future works):
## Future works
* No modular inter-procedural analysis
* No support for integer wrap/overflow
* Loops with equality (instead of inequality) in loop condition will have pessimistic bounds
* We assume that each memory access has 32bits-size, and is 32bits-aligned
* 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
## Questions:
mail: Clement.Ballabriga@univ-lille1.fr
[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).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment