quarkslab / arybo Goto Github PK

Manipulation, canonicalization and identification of mixed boolean-arithmetic symbolic expressions

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

Python 32.48% CMake 4.71% C 1.05% C++ 61.68% Batchfile 0.08%

arybo's Introduction

Arybo

Arybo is a software for manipulating such expressions using bit vectors and gives a bit-per-bit symbolic representation.

The ANF (Algebric Normal Form) form is used, which basically represents boolean expressions using the XOR and AND operators.

The whole documentation is available here: https://pythonhosted.org/arybo/

Quick start

Under Linux/OSX/Windows, Arybo can be installed through pip for Python 2 and 3:

$ pip install arybo

Please note that Python 2 support for pytanque under Windows isn't available, as the official compiler for Python extensions is Visual Studio 2010, which can't compile libpetanque.

You will need at least clang 3.5 or GCC 4.9 to compile the python extension "pytanque" under Linux/OS.

Users of Ubuntu 14.04 need to install GCC 6. See the documentation for detailed instructions: https://github.com/quarkslab/arybo/blob/master/docs/source/setup.rst#notes-for-ubuntu-1404.

More details on the installation process can be found here: https://pythonhosted.org/arybo/setup.html

To quickly use Arybo, you can the IPython shell by simply launching iarybo:

# Starts an IPython interactive shell with 8-bit symbolic variables defined
$ iarybo 8
In [1]: x|0x7f
Out[1]:Vec([
1,
1,
1,
1,
1,
1,
1,
x7
])
In [2]: (x^y)&a
Out[2]:
Vec([
((x0 * a0) + (y0 * a0)),
((x1 * a1) + (y1 * a1)),
((x2 * a2) + (y2 * a2)),
((x3 * a3) + (y3 * a3)),
((x4 * a4) + (y4 * a4)),
((x5 * a5) + (y5 * a5)),
((x6 * a6) + (y6 * a6)),
((x7 * a7) + (y7 * a7))
])

Tutorials can be found here: https://pythonhosted.org/arybo/tutorial.html. Advanced usage examples can be found in the examples directory.

License

This is published under a BSD license (see LICENSE.txt file)

Contact

For any issue, do not hesitate to open an issue/create a pull request on Github.

arybo's People

Contributors

Stargazers

Watchers

arybo's Issues

AttributeError: 'ExprConcat' object has no attribute 'urem'

Should be fixed with 38dd93c

I have tried the getType(), but it still have another error.
the log said that AttributeError: 'ExprConcat' object has no attribute 'urem'
here is the complete log.

[+] Generating symbolic_expressions/sample4-unprotected.bin.py
[+] Converting symbolic expressions to an LLVM module...
Traceback (most recent call last):
  File "./solve-vm.py", line 761, in <module>
    retValue  = main()
  File "./solve-vm.py", line 671, in main
    M = generateLLVMExpressions(ctx, 0)
  File "./solve-vm.py", line 623, in generateLLVMExpressions
    e = tritonexprs2arybo(exprs)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 169, in tritonexprs2arybo
    e = tritonast2arybo(e.getAst(), True, False, context)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 36, in tritonast2arybo
    v = next(children)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 30, in <genexpr>
    children = (tritonast2arybo(c,use_exprs,use_esf,context) for c in children_)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 60, in tritonast2arybo
    v = next(children)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 30, in <genexpr>
    children = (tritonast2arybo(c,use_exprs,use_esf,context) for c in children_)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 139, in tritonast2arybo
    return reduce(binop, children)
  File "~/.local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 132, in <lambda>
    TAstN.BVUREM: lambda x,y: x.urem(y),
AttributeError: 'ExprConcat' object has no attribute 'urem'
Command exited with non-zero status 1

Originally posted by @windy1946 in https://github.com/quarkslab/arybo/issue_comments#issuecomment-456111753

NumPy has deprecated int type

Title, results in :

AttributeError: module 'numpy' has no attribute 'int'.
`np.int` was a deprecated alias for the builtin `int`. To avoid this error in existing code, use `int` by itself. Doing this will not modify any behavior and is safe. When replacing `np.int`, you may wish to use e.g. `np.int64` or `np.int32` to specify the precision. If you wish to review your current use, check the release note link for additional information.
The aliases was originally deprecated in NumPy 1.20; for more details and guidance see the original release note at:
    https://numpy.org/devdocs/release/1.20.0-notes.html#deprecation

error: invalid use of incomplete type 'PyFrameObject' {aka 'struct _frame'}

Python bindings fail on macOS with gcc12:

:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h: In function 'std::string pybind11::detail::error_string()':
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:442:36: error: invalid use of incomplete type 'PyFrameObject' {aka 'struct _frame'}
:info:build   442 |                 "  " + handle(frame->f_code->co_filename).cast<std::string>() +
:info:build       |                                    ^~
:info:build In file included from /opt/local/Library/Frameworks/Python.framework/Versions/3.11/include/python3.11/Python.h:42:
:info:build /opt/local/Library/Frameworks/Python.framework/Versions/3.11/include/python3.11/pytypedefs.h:22:16: note: forward declaration of 'PyFrameObject' {aka 'struct _frame'}
:info:build    22 | typedef struct _frame PyFrameObject;
:info:build       |                ^~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:442:75: error: expected primary-expression before '>' token
:info:build   442 |                 "  " + handle(frame->f_code->co_filename).cast<std::string>() +
:info:build       |                                                                           ^
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:442:77: error: expected primary-expression before ')' token
:info:build   442 |                 "  " + handle(frame->f_code->co_filename).cast<std::string>() +
:info:build       |                                                                             ^
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:444:29: error: invalid use of incomplete type 'PyFrameObject' {aka 'struct _frame'}
:info:build   444 |                 handle(frame->f_code->co_name).cast<std::string>() + "\n";
:info:build       |                             ^~
:info:build /opt/local/Library/Frameworks/Python.framework/Versions/3.11/include/python3.11/pytypedefs.h:22:16: note: forward declaration of 'PyFrameObject' {aka 'struct _frame'}
:info:build    22 | typedef struct _frame PyFrameObject;
:info:build       |                ^~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:444:64: error: expected primary-expression before '>' token
:info:build   444 |                 handle(frame->f_code->co_name).cast<std::string>() + "\n";
:info:build       |                                                                ^
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:444:66: error: expected primary-expression before ')' token
:info:build   444 |                 handle(frame->f_code->co_name).cast<std::string>() + "\n";
:info:build       |                                                                  ^
:info:build /opt/local/var/macports/build/_opt_PPCRosettaPorts_math_libpetanque/libpetanque/work/arybo-1.1.0/petanque/third-party/pybind11/cast.h:445:26: error: invalid use of incomplete type 'PyFrameObject' {aka 'struct _frame'}
:info:build   445 |             frame = frame->f_back;
:info:build       |                          ^~
:info:build /opt/local/Library/Frameworks/Python.framework/Versions/3.11/include/python3.11/pytypedefs.h:22:16: note: forward declaration of 'PyFrameObject' {aka 'struct _frame'}
:info:build    22 | typedef struct _frame PyFrameObject;
:info:build       |                ^~~~~~

Without Python bindings the library builds fine and all tests pass: macports/macports-ports#17103

petanque tests fail to find TBB

ERROR: Intel TBB NOT found!
-- Looked for Threading Building Blocks in /opt/intel/tbb;/usr/local/include;/usr/include

I have TBB installed:

$ pkg info | grep tbb
onetbb-2021.3.0                Library that provides thread building blocks

Version: 1.1.0
FreeBSD 13

arybo latest on pip broken

['__add__', '__and__', '__class__', '__cmp__', '__coerce__', '__delattr__', '__div__', '__doc__', '__eq__', '__format__', '__ge__', '__getattribute__', '__gt__', '__hash__', '__iadd__', '__iand__', '__idiv__', '__ilshift__', '__imod__', '__imul__', '__init__', '__invert__', '__ior__', '__irshift__', '__isub__', '__ixor__', '__le__', '__lshift__', '__lt__', '__mod__', '__mul__', '__ne__', '__neg__', '__new__', '__or__', '__radd__', '__rand__', '__rdiv__', '__reduce__', '__reduce_ex__', '__repr__', '__rlshift__', '__rmod__', '__rmul__', '__ror__', '__rrshift__', '__rshift__', '__rsub__', '__rxor__', '__setattr__', '__sizeof__', '__str__', '__sub__', '__subclasshook__', '__xor__', 'equalTo', 'evaluate', 'getBitvectorMask', 'getBitvectorSize', 'getChildren', 'getHash', 'getKind', 'getParents', 'getValue', 'isLogical', 'isSigned', 'isSymbolized', 'setChild']
Traceback (most recent call last):
  File "./solve-vm.py", line 760, in <module>
    retValue  = main()
  File "./solve-vm.py", line 670, in main
    M = generateLLVMExpressions(ctx, 0)
  File "./solve-vm.py", line 623, in generateLLVMExpressions
    e = tritonexprs2arybo(exprs)
  File "/home/sudhakar/.virtualenvs/sym/local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 168, in tritonexprs2arybo
    e = tritonast2arybo(e.getAst(), True, False, context)
  File "/home/sudhakar/.virtualenvs/sym/local/lib/python2.7/site-packages/arybo/tools/triton_.py", line 31, in tritonast2arybo
    children_ = e.getChilds()

Although the version here in working fine. Just a heads up.

Examples using outdated Triton API

I noticed one example using older version of Triton API as shown below:

arybo/examples/triton_ida_patch.py

Line 34 in 89d9a42

rax_ast = triton.buildSymbolicRegister(triton.REG.RAX)

According to JonathanSalwan/Triton#689, buildSymbolicRegister has been renamed to getRegisterAst.

Other examples might be affected this.

llvmlite should be added as a dependency

Traceback (most recent call last):
  File "./solve-vm.py", line 760, in <module>
    retValue  = main()
  File "./solve-vm.py", line 670, in main
    M = generateLLVMExpressions(ctx, 0)
  File "./solve-vm.py", line 625, in generateLLVMExpressions
    M = to_llvm_function(e,[var.v])
  File "build/bdist.linux-x86_64/egg/arybo/lib/exprs_asm.py", line 201, in to_llvm_function
RuntimeError: llvmlite module unavailable! can't assemble to LLVM IR...

Installing llvmlite fixes this problem.
However it is not listed as a dependency.

'AstNode' object has no attribute 'getKind'

branch 'fix/triton' the python file 'triton_.py' run error.
it can not find getKind() in AstNode.

Infinity loop when reading complex expression

Hi,

I am currently trying to transform this expression into an arybo expression:

(((((((- (((((((((((((((- x) & 0xffffffff) + 0x2C) & 0xffffffff) & ((((((- x) & 0xffffffff) + 0x2C) & 0xffffffff) | 0xC4) & 0xffffffff)) & 0xffffffff) ^ ((x + 0xFFFFFFD4) & 0xffffffff)) & 0xffffffff) + 0x80403064) & 0xffffffff) ^ 0xED) & 0xffffffff) | 0x403053) & 0xffffffff) & 0xff)) & 0xff) + 0x7E) & 0xff) & 0xff) << 0) | ((0x0 & 0xffffff) << 8))

With these instructions:

from arybo.lib import MBA

def transform(x):
    return (((((((- (((((((((((((((- x) & 0xffffffff) + 0x2C) & 0xffffffff) & ((((((- x) & 0xffffffff) + 0x2C) & 0xffffffff) | 0xC4) & 0xffffffff)) & 0xffffffff) ^ ((x + 0xFFFFFFD4) & 0xffffffff)) & 0xffffffff) + 0x80403064) & 0xffffffff) ^ 0xED) & 0xffffffff) | 0x403053) & 0xffffffff) & 0xff)) & 0xff) + 0x7E) & 0xff) & 0xff) << 0) | ((0x0 & 0xffffff) << 8))

mba = MBA(32)
x = mba.var('x')

print transform(x)

But apparently, it somehow runs into an infinity loop as it run on 100% cpu for ~10 minutes until I killed the process.

app_inverse for expressions with more than one symbols

Thank you for building such a brilliant tool.
It seems that app_inverse does not support expressions with two or more symbols.
For example:

from arybo.lib import MBA
from arybo.tools import app_inverse
mba = MBA(32)
a = mba.var('a')
b = mba.var('b')
t = a & b
F = t.vectorial_decomp([a,b])
app_inverse(F) # returns None

Is there any workaround for this?

tritonast2arybo: unsupported node type 79 (BVSMOD)

Trying to go from Triton AST to LLVM IR by running some examples but getting unsupported node type 79 for BVSMOD

Is it possible to support this in arybo or is there a workaround?

Arybo does not support Python 2.7 in Windows

Trying to use Arybo in Windows with Triton, since Triton only support Python 2.7, I hope Arybo can fix Python 2.7 support in Windows

with the exception of Python 2 not available under Windows
https://pythonhosted.org/arybo/setup.html

Steps to reproduce in Windows:

install python-2.7.15.amd64
pip install arybo shows error compling pytanque:
building 'pytanque' extension ... include\pa/exprs.h(30) : fatal error C1083: Cannot open include file: 'cstdint': No such file or directory

Thanks

std::bad_alloc thrown in symbolic expression computation

The script to reproduce the issue is here:

from arybo.lib import MBA

def f(rdi, rsi, rdx, rcx, r8d):
   cse0Mult0 = (2816510611 * r8d)
   cse0Add1 = (1338184181 + (2816510611 * rdx))
   cse0Add2 = (2956783114 + (1478456685 * r8d))
   cse6Add4 = (1 + cse0Mult0)
   cse0BitOr0 = (cse0Add2 | (2956783114 + (1478456685 * rdx)))
   cse0BitOr1 = ((1338184181 + cse0Mult0) | cse0Add1)
   cse1Mult7 = ((cse6Add4 + cse0BitOr0) * ((3107144530 + (1438524315 * cse0BitOr1)) + (4294967295 * r8d)))
   cse0BitOr2 = (cse0Add1 | cse0Add2)
   cse2Mult13 = ((cse6Add4 + cse0BitOr2) * ((2856442981 + rdx) + (2856442981 * cse0BitOr2)))
   cse5Add12 = ((((((cse1Mult7 * 2816510611) + (2115068335 * rdx)) + (1338184181 * cse0BitOr1)) + (2115068335 * r8d)) + (1338184181 * cse0BitOr0)) + (cse2Mult13 * 2816510611))
   cse0Mult13 = (1478456685 * rdi)
   result = ((((cse5Add12 + 4294967293) + cse0Mult13) + (4294967295 * ((1618598933 + (2956913370 * rdi)) | ((((((1618598933 + (cse1Mult7 * 2956913370)) + (1618598934 * cse0BitOr0)) + (1618598934 * cse0BitOr1)) + (cse2Mult13 * 2956913370)) + (64830626 * r8d)) + (64830626 * rdx))))) + (4294967294 * ((2956783114 + cse0Mult13) | (cse5Add12 + 1338184181))))
   return result

mba = MBA(32)
rdi = mba.var('rdi')
rsi = mba.var('rsi')
rdx = mba.var('rdx')
rcx = mba.var('rcx')
r8d = mba.var('r8d')
ret = f(rdi, rsi, rdx, rcx, r8d)
print(ret)

Error is thrown here:

Traceback (most recent call last):
  File "ary-test", line 24, in <module>
    ret = f(rdi, rsi, rdx, rcx, r8d)
  File "ary-test", line 4, in f
    cse0Mult0 = (2816510611 * r8d)
  File "/home/vagrant/.local/lib/python3.7/site-packages/arybo/lib/mba_if.py", line 183, in __rmul__
    return self.__mul__(o)
  File "/home/vagrant/.local/lib/python3.7/site-packages/arybo/lib/mba_if.py", line 180, in __mul__
    return self.__call_op('mul', o)
  File "/home/vagrant/.local/lib/python3.7/site-packages/arybo/lib/mba_if.py", line 158, in __call_op
    ret = getattr(self.mba, fname)(self.vec, o)
  File "/home/vagrant/.local/lib/python3.7/site-packages/arybo/lib/mba_impl_petanque.py", line 323, in mul_n
    self.iadd_lshifted_Y(ret, X, i)
  File "/home/vagrant/.local/lib/python3.7/site-packages/arybo/lib/mba_impl_petanque.py", line 234, in iadd_lshifted_Y
    carry_new = simplify_inplace(mul_XY + (carry * Xi))
MemoryError: std::bad_alloc

I used a function sample that can be found here.

Pytanque installation fails on Ubuntu 14.04

Hi,

I'm trying to install branch feature/exprs of Arybo and I'm getting the following error when I run the command to install pytanque: sudo pip install pytanque

Command "/usr/bin/python -u -c "import setuptools, tokenize;__file__='/tmp/pip-build-3EsubV/pytanque/setup.py';exec(compile(getattr(tokenize, 'open', open)(__file__).read().replace('\r\n', '\n'), __file__, 'exec'))" install --record /tmp/pip-nseUJr-record/install-record.txt --single-version-externally-managed --compile" failed with error code 1 in /tmp/pip-build-3EsubV/pytanque/

Any ideas of how I could get passed this error or successfully install pytanque?

Thanks,
Sebastian

Installation Arybo via pip on Windows, 'ssize_t': redefinition

Hi, I install Arybo via pip and Python 3.6.5 32bit on Windows and receive this error:

C:\Program Files (x86)\python36-32\include\pyconfig.h(174): error C2371: 'ssize_t': redefinition; different basic types
include\pa/compat.h(32): note: see declaration of 'ssize_t'

After I comment the lines defining ssize_t in pyconfig.h, I could install Arybo via pip.

Support new design of Triton in Python examples

Hi, I think you should support the new design of Triton in Python examples of Arybo.

https://github.com/JonathanSalwan/Triton/tree/master/src/examples/python
https://github.com/JonathanSalwan/Triton/releases

CMake Script is incorrect?

Hi:

For me it seems FindTBB()'s library has been used and linked, but it's header search path is not.

I had to add target_include_directories(petanque PUBLIC ${TBB_INCLUDE_DIRS}) for it to pick up TBB