| --- |
| language: |
| - en |
| tags: |
| - code |
| - symbolic-math |
| - deobfuscation |
| - mixed-boolean-arithmetic |
| license: mit |
| pipeline_tag: other |
| --- |
| |
| # MBA Simplifier — Pipeline v5 |
|
|
| Simplifies **Mixed Boolean-Arithmetic (MBA)** expressions used in code obfuscation. |
| Combines BFS lookup over a pre-computed expression table, symbolic rewriting (40+ rules), |
| and optional neural-guided search. Every output is oracle-verified correct. |
|
|
| ## Quick Start |
|
|
| ```bash |
| git clone https://huggingface.co/<your-username>/mba-simplifier |
| cd mba-simplifier |
| pip install -r requirements.txt |
| python inference.py "(x & y) + (x | y)" |
| ``` |
|
|
| Expected output: |
| ``` |
| BFS: 18,189 entries (182ms) |
| Input: (x & y) + (x | y) |
| Simplified: x + y |
| Reduction: 57% (bfs) |
| Latency: 186 ms (cold), ~2 ms (warm) |
| ``` |
|
|
| ## Python API |
|
|
| ```python |
| from inference import simplify |
| |
| result = simplify("(x & y) + (x | y)") |
| print(result["simplified"]) # "x + y" |
| print(result["reduction"]) # 0.571 |
| print(result["strategy"]) # "bfs" |
| print(result["latency_ms"]) # ~2 ms warm |
| |
| # 32-bit mode (symbolic only — BFS table is 8-bit) |
| result = simplify("(x & y) + (x | y)", bits=32) |
| # → "x + y" (strategy: symbolic) |
| |
| # With neural guidance |
| result = simplify("complex_expr", model_path="mba_classifier_v2.pt") |
| ``` |
|
|
| ### Return fields |
|
|
| | Field | Type | Description | |
| |---|---|---| |
| | `simplified` | str | Simplified infix expression | |
| | `original` | str | Input expression | |
| | `reduction` | float | Tree-size reduction (0.0–1.0) | |
| | `strategy` | str | `bfs` / `symbolic` / `neural` / `none` | |
| | `latency_ms` | float | Wall-clock time in milliseconds | |
|
|
| ## Input / Output Examples |
|
|
| | Input | Output | Strategy | |
| |---|---|---| |
| | `(x & y) + (x \| y)` | `x + y` | bfs | |
| | `(x \| y) - (x & y)` | `x ^ y` | bfs | |
| | `(x + y) - 2 * (x & y)` | `x ^ y` | bfs | |
| | `~(~x)` | `x` | bfs | |
| | `-(~x) - 1` | `x` | symbolic | |
| | `~(~x & ~y)` | `x \| y` | symbolic | |
| | `x & (x \| y)` | `x` | symbolic | |
| | `x ^ x` | `0` | bfs | |
| | `x * 1 + y * 0` | `x` | bfs | |
| | `(x & ~y) \| (x & y)` | `x` | bfs | |
|
|
| ## Architecture |
|
|
| **Three-layer pipeline** (first hit wins): |
|
|
| 1. **BFS lookup** — pre-computed table of 18,189 minimal 8-bit expressions |
| (loaded from `bfs_table_6.json`, ~180ms first call, ~2ms warm). |
| Coverage: all 2-variable expressions up to AST size 6. |
|
|
| 2. **Symbolic rewriting** — 40+ algebraic rules covering MBA identities, |
| De Morgan, absorption, two's complement, XOR-NOT, cancellation, |
| constant folding. Runs to fixpoint (up to 30 passes). Works for 8-bit |
| and 32-bit. |
|
|
| 3. **Neural-guided beam search** (optional, requires `mba_classifier_v2.pt`) — |
| Transformer classifier predicts rewrite rules to try. Symbolic executor |
| applies them; oracle verifies each candidate. Requires `torch`. |
|
|
| **Oracle verification:** every candidate result is verified by random sampling |
| (512 points). The pipeline never returns a wrong answer — it falls back to the |
| original if verification fails. |
|
|
| ## Benchmark Results |
|
|
| | Method | Correct% | Reduced% | Size reduction | ms/expr | |
| |---|---|---|---|---| |
| | **Pipeline v5 (ours)** | **100%** | **100%** | **77%** | **6.5ms** | |
| | MBA-Blast (USENIX '21) | 100% | 100% | 77% | 15.8ms | |
| | SSPAM (Quarkslab) | 100% | 0% | 0% | 298.6ms | |
| | LLaMA-3.3-70B | 93% | 12% | 16% | 34.4ms | |
|
|
| *Dataset: MBA-Blast paper dataset, 62 expressions, 8-bit 2-var.* |
|
|
| ## Files |
|
|
| | File | Description | |
| |---|---| |
| | `inference.py` | Standalone inference — the only file you need | |
| | `bfs_table_6.json` | Pre-computed BFS table, 18K entries (1.7MB) | |
| | `mba_classifier_v2.pt` | Neural model, 2.2M params (8.6MB, optional) | |
|
|
| ## Limitations |
|
|
| - **BFS table:** 8-bit only, variables `x` and `y` only. Expressions with 3+ |
| variables or 32-bit semantics fall through to symbolic rewriting. |
| - **Variables:** up to 2 variables for BFS; symbolic handles more. |
| - **Bit width:** 8 and 32 only. |
| - **Cold start:** BFS table loads in ~180ms on first call; subsequent calls |
| are fast (~2ms). |
| - **Neural model trained on 8-bit** — may not generalize perfectly to 32-bit. |
|
|
| ## Requirements |
|
|
| ``` |
| torch>=1.13.0 # required for neural layer (optional otherwise) |
| numpy>=1.21.0 # required for oracle exhaustive check (8-bit) |
| ``` |
|
|
| Python 3.10+ required (structural pattern matching). |
|
|
