feat: python package refactor

.github/workflows/python-style.yml

@@ -0,0 +1,38 @@
+name: Python Style
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+  workflow_dispatch:
+
+jobs:
+  lint:
+    name: ${{ matrix.session }}
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        session: [ruff, mypy]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+      - name: Install uv
+        run: |
+          curl -LsSf https://astral.sh/uv/install.sh | sh
+      - name: Create uv virtual environment
+        run: |
+          cd crackers_python
+          uv venv
+      - name: Install dev dependencies
+        run: |
+          cd crackers_python
+          uv pip install -e .[dev]
+      - name: Run nox session
+        run: |
+          cd crackers_python
+          uv run nox -s ${{ matrix.session }}

.github/workflows/python.yml

@@ -14,7 +14,7 @@ on:
       - main
   workflow_dispatch:
   release:
-    types: [published]
+    types: [ published ]
 
 permissions:
   contents: read
@@ -34,14 +34,11 @@ jobs:
       - uses: actions/checkout@v4
         with:
           submodules: true
-      - uses: actions/setup-python@v5
-        with:
-          python-version: 3.x
       - name: Build wheels
         uses: PyO3/maturin-action@v1
         with:
           target: ${{ matrix.platform.target }}
-          args: --release --out dist --find-interpreter --auditwheel skip
+          args: --release --out dist --interpreter python3.10 python3.11 python3.12 python3.13 python3.13t pypy3.10 pypy3.11 --auditwheel skip
           working-directory: crackers_python
           manylinux: manylinux2_28
           before-script-linux: |

README.md

@@ -7,45 +7,129 @@
 
 # `crackers`: A Tool for Synthesizing Code-Reuse Attacks from `p-code` Programs
 
-This repo contains the source code of `crackers`, a procedure for synthesizing
-code-reuse attacks (e.g. ROP). `crackers` takes as input a "reference program", usually
-written in an assembly language, a binary (of the same architecture) in which to look
-for gadgets, and user-provided constraints to enforce on synthesized chains. It will always
-return an answer (though there is no strict bound to runtime), reporting either that the problem
-is UNSAT, or providing an assignment of gadgets that meet all constraints, and a model
-of the memory state of the PCODE virtual machine at every stage of the computation.
+[![Build](https://github.com/toolCHAINZ/crackers/actions/workflows/build.yml/badge.svg)](https://github.com/toolCHAINZ/crackers/actions/workflows/build.yml)
+[![docs.rs](https://docs.rs/crackers/badge.svg)](https://docs.rs/crackers)
+
+This repository contains the source code for `crackers`, a tool for synthesizing
+code-reuse attacks (e.g., ROP) built around the Z3 SMT Solver and Ghidra's SLEIGH code translator.
 
-`crackers` will assume that _all_ system state is usable unless the user prohibits it by providing a constraint.
-This approach, while requiring more human guidance, allows it to minimize the assumptions it makes about the
-arrangement and roles of memory in an exploit.
+## How does it work?
 
-To validate chains, `crackers` builds a mathematical model of the trace through the gadgets. This model, along
-with user-provided constraints, is verified against a model of the "reference program". When this verification
+`crackers` takes as input a "reference program," usually
+written in an assembly language, a binary (of the same architecture) in which to look
+for gadgets, and user-provided constraints to enforce on synthesized chains. It will always
+return an answer (though there is no strict bound on runtime), reporting either that the problem
+is UNSAT or providing an assignment of gadgets that meet all constraints, along with a model
+of the memory state of the PCODE virtual machine at every step in the chain. This memory model can
+then be used to derive the inputs necessary to realize the ROP chain.
+
+`crackers` itself makes _no_ assumptions about the layout of memory in the target program, nor the extent of an attacker's
+control over it: it assumes that _all_ system state is usable unless explicitly prohibited through a constraint.
+This approach increases flexibility, with the drawback of requiring more human-guided
+configuration than many other ROP tools.
+
+To validate chains, `crackers` builds a mathematical model of the execution of a candidate chain and makes assertions on it
+against a model generated from a specification (itself expressed as a sequence of PCODE operations). When this verification
 returns SAT, `crackers` returns the Z3 model of the memory state of the chain at every point of its execution. This
 memory model may be used to derive the contents of memory needed to invoke the chain, and transitively the input needed to
 provide to the program to realize it.
 
-Note that the provided CLI of crackers currently only prints the selected gadgets to the command line.
-To make use of the logical memory model it must be used through the programmatic API.
-
-There is also an experimental Python binding for `crackers`, allowing for basic configuration, execution, and model
-inspection from python. These bindings also feature cross-FFI support with the python z3 bindings, allowing
-constraints to be expressed as python functions or `lambda` expressions returning Python Z3 `BoolRef` instances.
+`crackers` is available as a command-line tool, a Rust crate, or a Python package.
 
 ### This software is still in alpha and may change at any time
 
-## CLI Usage
+## How do I use it?
+
+You have three options:
+
+### Python Package
+
+[![PyPI](https://img.shields.io/pypi/v/crackers)](https://pypi.org/project/crackers/)
+
+The easiest way to use `crackers` is through the [PyPI](https://pypi.org/project/crackers/) package. For every release, we provide wheels for `[MacOS, Windows, Linux] x [3.10, 3.11, 3.12, 3.13]`.
+
+A simple usage looks like the following:
+
+```python
+import logging
+logging.basicConfig(level=logging.INFO)
+
+from z3 import BoolRef, BoolVal
+
+from crackers import State, ModeledBlock
+from crackers.config import MetaConfig, LibraryConfig, SleighConfig,
+    ReferenceProgramConfig, SynthesisConfig, ConstraintConfig, CrackersConfig
+from crackers.config.constraint import RegisterValuation,
+    RegisterStringValuation, MemoryValuation, PointerRange,
+    CustomStateConstraint, CustomTransitionConstraint, PointerRangeRole
+from crackers.config.log_level import LogLevel
+from crackers.config.synthesis import SynthesisStrategy
+
+# Custom state constraint example
+def my_constraint(s: State, _addr: int) -> BoolRef:
+    rdi = s.read_register("RDI")
+    rcx = s.read_register("RCX")
+    return rdi == (rcx ^ 0x5a5a5a5a5a5a5a5a)
+
+
+# Custom transition constraint example
+def my_transition_constraint(block: ModeledBlock) -> BoolRef:
+    # Dummy: always true
+    return BoolVal(True)
+
+
+meta = MetaConfig(log_level=LogLevel.INFO, seed=42)
+library = LibraryConfig(max_gadget_length=8, path="libz.so.1", sample_size=None,
+                        base_address=None)
+sleigh = SleighConfig(ghidra_path="/Applications/ghidra")
+reference_program = ReferenceProgramConfig(path="sample.o", max_instructions=8, base_address=library.base_address)
+synthesis = SynthesisConfig(strategy=SynthesisStrategy.SAT, max_candidates_per_slot=200, parallel=8, combine_instructions=True)
+constraint = ConstraintConfig(
+    precondition=[
+        RegisterValuation(name="rdi", value=0xdeadbeef),
+        MemoryValuation(space="ram", address=0x1000, size=4, value=0x41),
+        RegisterStringValuation(reg="rsi", value="/bin/sh"),
+        CustomStateConstraint(code=my_constraint)
+    ],
+    postcondition=[
+        RegisterValuation(name="rax", value=0x1337),
+        CustomStateConstraint(code=my_constraint)
+    ],
+    transition=[
+        PointerRange(role=PointerRangeRole.READ, min=0x2000, max=0x3000),
+        CustomTransitionConstraint(code=my_transition_constraint)
+    ]
+)
+config = CrackersConfig(meta=meta, library=library, sleigh=sleigh, specification=reference_program, synthesis=synthesis, constraint=constraint)
+config.run()
+```
+
+### Rust CLI
+
+You can install the `crackers` CLI from `crates.io` by running:
+
+```sh
+cargo install --all-features crackers
+```
+
+You can then run:
+
+```sh
+crackers new my_config.toml
+```
+
+to generate a new configuration for the tool at `my_config.toml`. This config file can be adjusted
+for your use case and then used with:
 
 ```sh
-cargo install --all-features --path . 
+crackers synth my_config.toml
 ```
 
-This will install the `crackers` binary in your path. `crackers` takes a single command line argument,
-pointing to a config file. An example file follows:
+There are many options to configure in this file. An example is below:
 
 ```toml
-# location to find a ghidra installation. This is only used for
-# locating architecture definitions
+# Location to find a Ghidra installation. This is only used for
+# SLEIGH architecture definitions
 [sleigh]
 ghidra_path = "/Applications/ghidra"
 
@@ -56,34 +140,34 @@ ghidra_path = "/Applications/ghidra"
 # * "optimize" is a weighted SAT problem, giving preference to shorter gadgets
 # Optimize tends to perform better when only one validation worker is present and SAT scales better with more workers
 strategy = "sat"
-# the maximum number of candidates that are considered for each sub-slice of the specification
-# if you don't want to cap this, just set it arbitrarily high. Might make it optional later
+# The maximum number of candidates considered for each sub-slice of the specification
+# If you don't want to cap this, just set it arbitrarily high. Might make it optional later
 max_candidates_per_slot = 50
 # The number of chain validation workers to use
 parallel = 8
 
 # crackers works by taking in an "example" computation and synthesizing a compatible chain
-# right now, it does not support specifications with controlflow
+# Right now, it does not support specifications with control flow
 [specification]
-# the path at which to find the raw binary containing the bytes of the specification computation
+# The path at which to find the raw binary containing the bytes of the specification computation
 path = "bin/execve_instrs.bin"
-# the number of assembly instructions in the specification
+# The number of assembly instructions in the specification
 max_instructions = 5
 
-# settings involving the file from which to pull gadgets
+# Settings involving the file from which to pull gadgets
 [library]
-# the path to the file. It can be any type of object file that gimli_object can parse (e.g. ELF, PE)
+# The path to the file. It can be any type of object file that gimli_object can parse (e.g., ELF, PE)
 path = "bin/libc_wrapper"
-# the maximum length of gadget to extract. Raising this number increases both the complexity of the gadgets
+# The maximum length of gadget to extract. Raising this number increases both the complexity of the gadgets
 # that are reasoned about and the total number of found gadgets
 max_gadget_length = 4
-# optionally randomly sample the set of parsed gadgets to a given size
+# Optionally randomly sample the set of parsed gadgets to a given size
 random_sample_size = 20000
-# optionally use a set seed for gadget selection
+# Optionally use a set seed for gadget selection
 # random_sample_seed = 0x234
 
-# from this point on are constraints that we put on the synthesis
-# these are fairly self-explanatory
+# From this point on are constraints that we put on the synthesis
+# These are fairly self-explanatory
 [constraint.precondition.register]
 RAX = 0
 RCX = 0x440f30
@@ -109,75 +193,48 @@ RAX = 0x3b
 RSI = 0
 RDX = 0
 
-# this constraint enforces that the value pointed to by this register
+# This constraint enforces that the value pointed to by this register
 # must be equal to the given string
 [constraint.postcondition.pointer]
 RDI = "/bin/sh"
 
-# ANY pointer access, read or write must fall in this range
-# might separate read/write later
+# ANY pointer access, read or write, must fall in this range
+# Might separate read/write later
 [constraint.pointer]
 min = 0x7fffffffde00
 max = 0x7ffffffff000
 ```
 
-A successful synthesis will print out a listing of the gadgets were selected.
-
-## Library Usage
+Note that using the CLI, a successful synthesis will print out a listing of the gadgets that were selected,
+but not the memory model found in synthesis.
 
-`crackers` intended mode of use is as a library. All of the above settings from the config correspond
-to settings that can be set programmatically by API consumers.
+### Rust Crate
 
-When using the API, rather than getting a listing of gadgets as an output, you get a model of the synthesized chain.
-This model of the chain includes information about what gadgets were selected as well as a Z3 `Model` representing the
-memory at all states of execution in the gadget chain. This model can be queried to derive the memory conditions
-necessary to execute the chain.
+[![Crates.io](https://img.shields.io/crates/v/crackers.svg)](https://crates.io/crates/crackers)
 
-### Constraints
+`crackers` is on `crates.io` and can be added to your project with:
 
-Constraints work a little differently with the API. Instead of specifying registers and register equality,
-`crackers` allows consumers to provide a closure of the following types:
-
-```rust
-pub type StateConstraintGenerator = dyn for<'a, 'b> Fn(&'a Context, &'b State<'a>) -> Result<Bool<'a>, CrackersError>
-    + Send
-    + Sync
-    + 'static;
-pub type PointerConstraintGenerator = dyn for<'a, 'b> Fn(
-        &'a Context,
-        &'b ResolvedVarnode<'a>,
-        &'b State<'a>,
-    ) -> Result<Option<Bool<'a>>, CrackersError>
-    + Send
-    + Sync
-    + 'static;
+```sh
+cargo add crackers
 ```
 
-The first type is used for asserting initial and final space constraints. These functions take a z3 context, and a handle
-to the program state, returning a `Result<Bool>`. The decision procedure will automatically evaluate
-provided functions and assert the booleans they return.
+API documentation can be found on [docs.rs](https://docs.rs/crackers/latest/crackers/).
 
-The second type is used for asserting read/write invariants. These functions take in a handle to z3, as well as a struct containing
-the bitvector corresponding to the read/write address, as well as the state the read/write is being performed on. 
-Any time a chain reads or writes from memory, the procedure will automatically call these functions and assert the returned
-booleans. This can allow for setting safe/unsafe ranges of memory or even the register space.
+** The API is unstable and largely undocumented at this time. **
 
 # Research Paper
 
-`crackers` was developed in support of our research paper _Synthesis of Code-Reuse Attacks from `p-code` Programs_.
-You can find the author accepted manuscript [here](https://ora.ox.ac.uk/objects/uuid:906d32ca-407c-4cab-beab-b90200f81d65).
-This work has been accepted to [Usenix Security 2025](https://www.usenix.org/conference/usenixsecurity25/presentation/denhoed).
+`crackers` was initially developed in support of our research paper, _Synthesis of Code-Reuse Attacks from `p-code` Programs_,
+presented at [Usenix Security 2025](https://www.usenix.org/conference/usenixsecurity25/presentation/denhoed).
 
-You can cite this work with the following BibTex:
+If you found the paper or the implementation useful, you can cite it with the following BibTeX:
 
 ```bibtex
-@inproceedings {denhoed2025synthesis,
-author = {Mark DenHoed and Thomas Melham},
-title = {Synthesis of Code-Reuse Attacks from p-code Programs},
-booktitle = {34th USENIX Security Symposium (USENIX Security 25)},
-year = {2025},
-address = {Seattle, WA},
-publisher = {USENIX Association},
-month = aug
+@inproceedings{denhoed2025synthesis,
+  title={Synthesis of ${Code-Reuse}$ Attacks from p-code Programs},
+  author={DenHoed, Mark and Melham, Tom},
+  booktitle={34th USENIX Security Symposium (USENIX Security 25)},
+  pages={395--411},
+  year={2025}
 }
 ```

crackers/Cargo.toml

@@ -24,7 +24,7 @@ toml = ["dep:toml_edit"]
 z3-gh-release = ["z3/gh-release"]
 
 [dependencies]
-jingle = { version = "0.3.0", features = ["gimli"] }
+jingle = { version = "0.3.2", features = ["gimli"] }
 z3 = "0.18.2"
 serde = { version = "1.0.203", features = ["derive"] }
 thiserror = "2.0"

crackers_python/Cargo.toml

@@ -12,11 +12,13 @@ crate-type = ["cdylib"]
 [dependencies]
 pyo3 = { version = "0.26", features = ["extension-module", "py-clone"] }
 crackers = {path = "../crackers", features = ["pyo3"], version = "0.5.4" }
-jingle = { version = "0.3.0", features = ["pyo3"]}
+jingle = { version = "0.3.2", features = ["pyo3"]}
 toml_edit = { version = "0.23.4", features = ["serde"] }
 z3 = "0.18.2"
 serde_json = "1.0.140"
 lazy_static = "1.5.0"
+tracing = "0.1.41"
+tracing-subscriber = "0.3.20"
 
 [dev-dependencies]
 pyo3 = { version = "0", features = ["extension-module"] }