quarkslab / sspam Goto Github PK

Symbolic Simplification with PAttern Matching

License: BSD 3-Clause "New" or "Revised" License

Python 99.86% Makefile 0.14%

sspam's Introduction

sspam: Symbolic Simplification with PAttern Matching

sspam is a software for simplifying mixed expressions (expressions using both arithmetic and boolean operators) with pattern matching. It uses sympy for arithmetic simplification, and z3 for flexible matching (matching equivalent expressions with different representations).

Requirements

To use sspam, you need:

The SMT solver z3 version 4.4.2
The Python library for symbolic mathematics sympy
The Python module for ast unparsing astunparse

To contribute to sspam, you need:

The Python module for source checking [flake8] (https://pypi.python.org/pypi/flake8)
The Python module for source checking [pylint] (https://www.pylint.org/)
The Python framework for testing [pytest] (http://docs.pytest.org/en/latest/index.html)

Installation

You can install most requirements with pip install -r requirements.txt (or pip install -r requirements-dev.txt to contribute)
To install z3, you can either:
Compile it from source
Or download a release and add the bin/ directory to your $PYTHONPATH
To install SSPAM:

$ sudo python setup.py install

Using sspam

You can use sspam either with the command line:

$ sspam "(x & y) + (x | y)"

(x + y)

Or in a python script:

from sspam import simplifier

print simplifier.simplify("(x & y) + (x | y)")

You'll see a few examples of utilisation of sspam in the examples/ directory.

Note that a cse module is provided in order to do common subexpression elimination (avoid dealing with the same subexpressions several times).

Tests

To run tests of sspam please use make test

Contribute

To contribute to sspam, create a branch with your contribution (feature, fix...). Please use the command make check for some basic checkings of your codestyle. As not all errors of pylint might be relevant, you can use #pylint: disable= comments in your code to disable irrelevant errors.

To check that your contribution does not affect normal behaviour of sspam, please use make test.

sspam's People

Contributors

Stargazers

Watchers

Forkers

cequencer wellcomez codingsf rainoftime threatinteltest freemanzyq noutoff moneytech masterscott trietptm-on-coding-algorithms darkersquirrel cjdresel gmh5225 normanpatrick

add patterns, e.g.(A & B & ~A) -> 0 and simplification passes, e.g. (A & 0xFF...FF) -> A
or use z3 (to avoid extract / concat insertion, only boolean exprs as input)

=> those two only support boolean, not bitwise ! To have both:

use arybo with a minimal identification function (big dependance on arybo)
or implement everything from scratch (long and painful)

Sanitize expression (miasm)

We could have a script for each "standard" tool to extract expressions (miasm, medusa, triton, etc).

Let's start with miasm output (obtained via Translator.to_language("Python") function)

ECX = memory(((ESP + 0x10) & 0xffffffff), 0x4)
EAX = memory(((ESP + 0x14) & 0xffffffff), 0x4)
EBX = ((((ECX & 0xff) & 0xff) << 0) | (((0xFFFFFF if (((ECX >> 7) & 0x1)) else 0x0) & 0xffffff) << 8))
EDX = ((((EAX & 0xff) & 0xff) << 0) | (((0xFFFFFF if (((EAX >> 7) & 0x1)) else 0x0) & 0xffffff) << 8))
ESI = EBX
EDX = ((EDX ^ 0xFFFFFFFF) & 0xffffffff)
ESI = ((ESI + ((- EDX) & 0xffffffff)) & 0xffffffff)
EDX = ((EDX + ((- EBX) & 0xffffffff)) & 0xffffffff)
EDI = ESI
ESI = ((ESI ^ 0xFFFFFFFE) & 0xffffffff)
EDI = ((EDI | 0x1) & 0xffffffff)
EDX = ((EDI + EDX) & 0xffffffff)
EBX = ((EDX * 0x2) & 0xffffffff)
ESI = ((EBX & ESI) & 0xffffffff)
EBX = ((ESI * 0x2) & 0xffffffff)
ESI = EAX
EAX = ((EAX ^ 0xFFFFFFFF) & 0xffffffff)
ESI = ((ECX | ESI) & 0xffffffff)
ECX = ((EAX ^ ECX) & 0xffffffff)
ESI = ((ESI + ESI) & 0xffffffff)
ESI = ((ESI ^ 0xFFFFFFFE) & 0xffffffff)
EAX = ESI
ECX = ((ECX + ((- EAX) & 0xffffffff)) & 0xffffffff)
EAX = ((EDX * 0x2) & 0xffffffff)
ECX = ((ECX ^ 0x1) & 0xffffffff)
ECX = ((EAX ^ ECX) & 0xffffffff)
EAX = ECX
af = ((((EAX ^ EBX ^ ((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff)) & 0xffffffff) >> 4) & 0x1)
pf = (((((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff) & 0xFF) & 0xffffffff) & 0x1)
zf = (0x0 if (((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff)) else 0x1)
of = ((((((EAX ^ EBX) & 0xffffffff) & ((EAX ^ ((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff)) & 0xffffffff)) & 0xffffffff) >> 31) & 0x1)
nf = ((((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff) >> 31) & 0x1)
cf = ((((EAX ^ EBX ^ ((((EAX ^ EBX) & 0xffffffff) & ((EAX ^ ((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff)) & 0xffffffff)) & 0xffffffff) ^ ((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff)) & 0xffffffff) >> 31) & 0x1)
EAX = ((EAX + ((- EBX) & 0xffffffff)) & 0xffffffff)
IRDst = loc_0000000000000045:0x00000045

A sanitization of this ouput should:

lower all identifiers (eax instead of EAX)
replace memory(...) with variable names (e.g. x, y)
remove all expressions concerning flags (af, pf, zf, of, nf cf) and last expression IRDst

CSE not commutative

2*x + 2*x as input produces:

cse0Mult0 = (2 * x)
result = (cse0Mult0 + cse0Mult0)

but 2*x + x*2 produces:

result = 2*x + x*2

SMT-LIB2 input?

Hi~ Can sspam accept a SMT-LIB2 file input?

Verbosity option

Add a verbose option, for example three levels:

0: only the final expression
1: temporary expressions of cse also displayed
3: log informations of every step

(should replace the ugly "debug=True" in simplifier.py)

Documentation

Some documentation, with:

how to use the simplifier
organisation of code
guidelines for new patterns: for example, 2*(A & B) - A -> (A ^ B) + 1 is better than 2*(A & B) - A - 1 -> (A ^ B) (avoid constant in the matching)

quarkslab / sspam Goto Github PK

sspam's Introduction

sspam's People

Contributors

Stargazers

Watchers

Forkers

sspam's Issues

Recommend Projects

Recommend Topics

Recommend Org