Amoco – Advancing Symbolic Binary Analysis In Python

Amoco is a cutting-edge Python package designed for the symbolic analysis of binaries, streamlining the decoding process across various architectures.

It provides a robust framework for instruction semantics and a flexible execution model to handle both concrete and symbolic values efficiently.

Amoco’s ongoing development promises to expand its capabilities, making it an indispensable tool for developers and security researchers alike.

Amoco is a python package dedicated to symbolic analysis of binaries.

It features:

• a generic framework for decoding instructions, developed to reduce the time needed to implement support for new architectures. For example the decoder for most IA32 instructions (general purpose) fits in less than 800 lines of Python. The full SPARCv8 RISC decoder (or the ARM THUMB-1 set as well) fits in less than 350 lines. The ARMv8 instruction set decoder is less than 650 lines.
• a symbolic algebra module which allows to describe the semantics of every instructions and compute a functional representation of instruction blocks.
• a generic execution model which provides an abstract memory model to deal with concrete or symbolic values transparently, and other system-dependent features.
• various classes implementing usual disassembly techniques like linear sweep, recursive traversal, or more elaborated techniques like path-predicate which relies on SAT/SMT solvers to proceed with discovering the control flow graph or even to implement techniques like DARE (Directed Automated Random Exploration).
• various generic helpers and arch-dependent pretty printers to allow custom look-and-feel configurations (think AT&T vs. Intel syntax, absolute vs. relative offsets, decimal or hex immediates, etc).

Amoco is still work in progress. See Todo for a list of features to be merged from develop branch or to be more thoroughly implemented.

Todo

Some components of amoco are still in the process of being pushed to the release branch or further developed. More precisely:

• x86 fpu instructions semantics are not implemented,
• arm SIMD, VFP, NEON, TrustZone, Jazelle instruction sets are not implemented,
• some solver-based disassembling strategies are not merged yet.
• idb import/export features are not implemented.

Contributions to fulfill uncomplete/unimplemented parts are welcome.

Developer Notes

The default Qt stylesheet is inspired by the excellent QDarkStyleSheet and uses most of its icons through the QResource API made available from the generated rc_icons.py module:

<pyenv>/lib/python3.<x>/site-packages/PySide6/rcc -g python icons.qrc > rc_icons.py

For more information click here.