Code obfuscation against symbolic execution with mixed Boolean-arithmetic permutation

Abstract

Code obfuscation is a fundamental technique for software protection and intellectual property defense, yet its effectiveness has been increasingly undermined by advances in symbolic execution and automated deobfuscation. Existing countermeasures based on path explosion, path divergence, or complex constraints suffer from high overhead, environment dependence, or vulnerability to algebraic simplification. To address these limitations, this article proposes a novel anti-symbolic execution obfuscation scheme built upon formally proven mixed Boolean-arithmetic (MBA) permutations on BA [ n ] . By combining polynomial, xor-shift, and cyclic-shift permutations, we construct non-linear MBA expressions that generate highly intricate constraints while preserving semantic equivalence and low runtime cost. A comprehensive evaluation under the automated Man-At-The-End attack model demonstrates that the proposed scheme (i) exponentially scales analysis complexity, consistently exceeding a 24-hour timeout against both isolated state-of-the-art Satisfiability Modulo Theories solvers and Dynamic Symbolic Execution frameworks (e.g., KLEE), (ii) achieves substantial runtime efficiency gains ranging from about 57 × (vs. MD5) and 66 × (vs. SHA1/SHA256) to over 2.2 × 10 4 (vs. CKKS), and (iii) attains 0% simplification on parseable instances while causing parser failures for full sequential expressions in the tested SiMBA/GAMBA versions. These results confirm that permutation-based MBA obfuscation offers a practical, composite, and resilient defense against symbolic execution, balancing strong protection with lightweight performance overhead. We further validated the scheme on coreutils, increasing symbolic-execution difficulty with only 0.40% binary-size overhead and no observable runtime penalty.