Technical Summary: SIMBA - GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic

Problem Definition

The paper addresses the Mixed-Boolean Arithmetic (MBA) synthesis problem: given a set of input-output examples $S = \{(x_i, y_i)\}_{i=1}^n$ where inputs and outputs are fixed-width bitvectors (typically 32-bit), the goal is to find an expression $e$ in the MBA language that satisfies $e(x_i) = y_i$ for all $i$. MBA expressions combine bitwise operations (AND, OR, XOR, NOT) with arithmetic operations (addition, subtraction, multiplication) over bitvectors.

This problem is central to program deobfuscation, where MBA obfuscation techniques transform simple expressions into syntactically complex but semantically equivalent ones. It is also relevant to compiler superoptimization, reverse engineering, and cryptanalysis.

The Challenge: Existing synthesis methods struggle with scalability. Stochastic approaches lack completeness guarantees, algebraic simplifiers cover only specific subclasses, and SAT/SMT-based methods become prohibitively expensive at larger bit-widths. While recent GPU-accelerated synthesis methods have shown promise in qualitative domains (e.g., LTL learning, regular expression inference), they rely on language caches indexed by observational equivalence. In MBA synthesis, behavior is quantitative: each candidate produces a $w$-bit value per example. With $n$ examples and width $w$, the behavioral space size is $2^{wn}$ (e.g., $2^{320}$ for $n=10, w=32$). This enormous space renders caching ineffective due to memory pressure and collisions, causing cache-based GPU approaches to fail on even moderately sized specifications.

Methodology: SIMBA

The authors introduce SIMBA (Synthesis of Mixed-Boolean Arithmetic), a GPU-accelerated synthesizer designed specifically to overcome the limitations of cache-based approaches in quantitative domains. SIMBA employs a cache-free, bottom-up enumeration strategy based on three core principles:

1. Cache-Free On-the-Fly Evaluation:
   Unlike prior GPU synthesizers that store intermediate results in a language cache, SIMBA decodes each candidate expression directly from a thread identifier, evaluates it against the specification, and immediately discards it. This eliminates the memory bottleneck associated with storing observational behaviors.

2. Bijective Enumeration:
   SIMBA establishes a bijection between integers and MBA expressions of a given size. Each GPU thread is assigned a unique integer identifier, which it independently decodes into an expression using a precomputed counting table. This allows for massive parallelism without inter-thread communication (except for a final atomic write upon finding a solution).

3. Locally Consistent Encoding:
   To maximize GPU efficiency under the SIMT (Single Instruction, Multiple Threads) architecture, the bijection is designed such that consecutive thread identifiers decode to structurally similar expressions. Specifically, threads within the same warp (a group of 32 threads) evaluate expressions that differ primarily in their input variables, following nearly identical execution paths. This minimizes branch divergence, ensuring high hardware utilization.

Technical Implementation:

• Representation: Expressions are encoded in Reverse Polish Notation (RPN).
• Decoding: A precomputed table $T[s][op]$ counts the number of valid RPN expressions of size $s$ with a specific top-level operator. This table is stored in GPU constant memory. Threads use this table to decode their integer ID into an expression structure and operator sequence.
• Evaluation: Each thread evaluates its decoded expression against all $n$ input-output pairs using an RPN stack interpreter.
• Search Strategy: The algorithm iterates through expression sizes $s = 1, 2, \dots, C$. For each size and operator, the host launches a kernel with exactly the number of threads required to cover all expressions of that size/operator combination.

Key Contributions

1. First GPU-Accelerated MBA Synthesizer: SIMBA is the first tool to successfully apply GPU acceleration to the quantitative domain of MBA synthesis, moving beyond the qualitative domains (LTL, regex) where previous GPU methods operated.
2. Cache-Free Design: The paper demonstrates that for quantitative domains with huge behavioral spaces, cache-free enumeration is not just an alternative but a necessity. SIMBA avoids the memory explosion inherent in caching observational equivalence classes.
3. Locally Consistent Bijection: The authors propose a novel encoding scheme that aligns the mathematical bijection with GPU hardware constraints (warps), minimizing branch divergence and maximizing throughput.
4. Scalability: SIMBA handles specifications and expression sizes that are intractable for existing CPU-based and cache-based GPU methods.

Experimental Results

The authors evaluated SIMBA on a new benchmark suite of 2,340 randomly generated MBA expressions with varying sizes ($s=5$ to $30$), variable counts ($k=2$ to $10$), and 16 examples per specification.

• Performance vs. Baselines:

  • SIMBA vs. VFB (GPU-based): SIMBA solved 90% of the instances solved by both tools with a median speedup of 1.6x. Crucially, SIMBA solved 634 instances that were entirely out of reach for VFB (which ran out of memory).
  • SIMBA vs. CVC5 (CPU-based SMT): On shared solvable instances, SIMBA was significantly faster (median 0.67s). SIMBA solved 668 instances that CVC5 could not solve within the 60-second time limit.
  • Coverage: SIMBA solved nearly all instances up to size 11 and was the only algorithm capable of solving instances of sizes 12 through 16. No tool solved instances larger than size 16.

• Scalability Analysis:

  • Memory: VFB's cache-based approach exhausted GPU memory at size 11 (requiring >2.1 GB for size 10). SIMBA's memory footprint remained constant regardless of size, bounded only by GPU registers and the small counting table.
  • Ablation Study: A variant, SIMBA-RTID, which used pseudo-randomly permuted thread IDs (destroying local consistency), was 4 times slower than SIMBA. This confirms that the locally consistent encoding is critical for minimizing branch divergence and achieving high performance.

Significance and Claims

The paper claims that SIMBA establishes cache-free GPU synthesis as a practical and scalable approach for quantitative domains. The authors argue that the standard "cache-centric" design, effective for qualitative domains where behavioral equivalence classes are small, breaks down for MBA synthesis due to the exponential size of the behavioral space ($2^{wn}$).

The significance of the work lies in:

1. Paradigm Shift: It identifies that for quantitative synthesis, algorithms must be designed from the ground up to avoid caching bottlenecks, rather than adapting qualitative methods.
2. Practicality: It provides a tool that can deobfuscate complex MBA expressions that were previously unsolvable, directly aiding in security analysis and reverse engineering.
3. Generalizability: The approach suggests that GPU acceleration is viable for other quantitative synthesis problems where the output space is too large for caching, provided the enumeration strategy respects hardware locality.

Limitations: The authors note that SIMBA requires a GPU, remains practical only up to expression sizes of approximately 16 due to the super-exponential growth of the search space, and does not handle approximate oracles or numerical constants.