N eu R educe: Reducing Mixed B oolean-Arithmetic Expressions by Recurrent Neural Network (2020)

Abstract: Mixed Boolean-Arithmetic (MBA) expressions involve both arithmetic calculation (e.g.,plus, minus, multiply) and bitwise computation (e.g., and, or, negate, xor). MBA expressions have been widely applied in software obfuscation, transforming programs from a simple form to a complex form. MBA expressions are challenging to be simplified, because the interleaving bitwise and arithmetic operations causing mathematical reduction laws to be ineffective. Our goal is to recover the original, simple form from an obfuscated MBA expression. In this paper, we first propose NeuReduce, a string to string method based on neural networks to automatically learn and reduce complex MBA expressions. We develop a comprehensive MBA dataset, including one million diversified MBA expression samples and corresponding simplified forms. After training on the dataset, NeuReduce can reduce MBA rules to homelier but mathematically equivalent forms. By comparing with three state-of-the-art MBA reduction methods, our evaluation result shows that NeuReduce outperforms all other tools in terms of accuracy, solving time, and performance overhead.

## introduction mixed boolean-arithmetic (mba) expression emerges as a software obfuscation @xcite @xcite technique, converting software into a syntactic different but semantic equivalent form. software developers have broadly adopted mba expressions obfuscation to resist malicious reverse engineering attacks or illegal cracking. for instance, software vendors @xcite and communication providers @xcite employ mba obfuscation to protect critical information such as digital rights man-agement (drm) or communication protocols and protect users' private contents. mba obfuscation technology draws strength from its neat design and rigorous mathematical foundation @xcite . it transforms a simple expression into an equivalent but more complex form, which contained mixed arithmetic and bitwise calculations. however, existing mathematical reduction rules can hardly simplify complex mba expressions, because they only fit either pure arithmetic or bitwise operation. existing researches explore diverse solutions to conquer mba obfuscation, including bitblast @xcite , pattern matching @xcite , and software synthesis @xcite . nevertheless, these methods treat mba expressions as black-boxes and neglect expressions' inner structures, which led to inevitable limitations such as low simplification accuracy or high-performance penalty. in this paper, we propose neureduce 1 , a novel solution that utilizes neural networks to defeat complex mba expressions. our proposal can take complex mba expression input as a character string format and output the simplification results. neureduce leverages supervised learning to ensure the correctness and conciseness of its outputs. we also notice that no large scale or diverse mba expressions dataset is available for training and evaluating our proposed approach. we first generate a mba dataset consisting of 1,000,000 mba expressions with diversified features. to the best of our knowledge, this is the largest and most diverse mba expression dataset. second, we implemented neureduce based on modern neural network models, i.e., long short-term memory, gate recurrent unit, and attention-based recurrent networks. we train neureduce using our comprehensive mba dataset and compared its performance with state-of-the-art reduction tools. for an impartial comparison, we carefully reviewed previous researches and summarized three evaluation metrics, i.e., accuracy, complexity, and solving time, as described in section 5. our experiments show that neureduce presents a superior performance than advanced reduction tools in these three aspects. in summary, we make the following contributions: ## methodology it has been proven that the mba deobfuscation is an np-hard problem @xcite , which means no general deterministic algorithms can solve this problem effectively. existing methods mentioned in section 2.2 treat mba obfuscation as a black-box, rather than understand the mechanism. to address the limitation on existing mba deobfuscation methods, we propose neureduce, a novel approach based on the sequence to sequence architecture @xcite with encoder-decoder @xcite to reduce mba expressions. considering the characteristics of the mba reduction problem, the reasoning from one sequence to another, we review and compare several deep neural networks and adopt the most effective model as the basic module of neureduce. we compare four broadly used neural networks: long short-term memory @xcite , gated recurrent unit @xcite , recurrent neural network based on the attention mechanism @xcite , and transformer @xcite . the following sections elaborate the techniques in neureduce in details. ## mba dataset neureduce requires a large-scale dataset to train for good performance. unfortunately, existing mba researchers only contributed a few mba examples. we collected all existing specimens and found they are insufficient for training and evaluating neureduce. therefore, we extend the algorithm introduced by @xcite to build a large-scale, diversified mba dataset. our dataset includes 1,000,000 mba samples, and each sample comprises the complex mba form and the corresponding simple form. the complex mba expression is guaranteed to be equivalent to the simple form by the theoretical foundation. mba generation approach. @xcite 's work described a high-level principle for constructing mba obfuscation rules from the truth tables and the linear equation system. however, their work did not answer practical questions when building a large scale of mba transformation rules, such as the number of variables in one expression, the length of the mba corpus, or the cost of generation. enlightening by the existing work, we design a functional toolkit for generating mba formulas. by the theorem, a bitwise expression e n with n variables has 2 2 n different reduced boolean expression. we first synthesize the 2 2 n distinct boolean expressions based on the truth tables, such as ¬x ∧ y, x ⊕ y. then we generate one identity by linear equation system. the method can ensure that the generated rules are syntactic correct and semantically equal since the solid math foundation. moreover, we verify the equality of each rule through an smt solver z3 @xcite . one example of mba rule generation is shown bellow, moreover, mba expression can be generated by linear combination of multiple mba rules, such as @xmath0, @xmath1, ⇒ x + @xmath2. expression format and complexity. each rule in the dataset is composed of a tuple in the form of (e c , e g ), in which e c represents complex mba expression, and e g means the related simplified result as the ground truth. given the complexity and practicability of mba expression, the number of different variables ranges from 2 to 10. moreover, e c and e g are presented as character strings, of which the length ranges from 3 to 100(the maximum exceeds 500). scale. in theory, the mba generation method described above can produce an infinite number of mba rules. to serve the purpose of training and evaluating neureduce in practice, we use it to generate 1,000,000 mba expressions. @xcite has proven that 2-variable and 3-variable mba expressions are commonly used in practical software obfuscation. therefore, we split the dataset into three parts: 800,000 samples of 2-variable and 3-variable mba expression, the other 200,000 multiple-variable mba expressions are for testing the model's adaptability and generality. ## experiment settings in this section, we present our experimental setup in detail, including the dataset settings, peer tool baselines, evaluation metrics, and configurations of model training. ## results and analysis we use the small-sized training set t rain s to train the four different neural networks -lstm, gru, attention lstm, and transformer. after training, we compare the models with existing reduction the evaluated results are shown in arybo does not output any wrong result, because arybo uses the bit-blast method, which maps each variable to bit and then simplifies it. although arybo can ensure the correctness of simplified mba expression, it suffers from high performance cost. the solving time of arybo is up to 640s, and 90% of the mba expressions can not be simplified in 40 minutes. another problem with arybo is that its reduction result is more complicated than the original one -the average length of reduction results is 20k, which is unreadable and unacceptable for security experts. since the simplification rules of complex mba expressions are not included in sspam's pattern matching library, sspam cannot simplify 85% of mba expressions on test dataset. syntia can simplify one mba expression in 10 seconds, but only 1576 mba expressions can be correctly simplified by it. syntia's output largely relies on the quality of input-output samples. therefore, syntia is hard to handle complex mba expressions. after training, neureduce can output grammatically correct expression in 1 second. neureduce can simplify at least 71% of mba expressions on test dataset, and its simplification result is acceptable for humans. from the table, the accuracy of attention-based model is slightly lower than the one of gru-based. from the aspect of expression representation, gru-based neureduce uses a sparse 0/1 matrix to encode expressions, while attention mechanism uses dense vectors. the dense vector can reduce the number of model parameters, but it may lack useful information input to the model. on the other hand, attention mechanism can effectively allocate a large weight to critical information when processing long texts and filter out useless information. however, each character is essential for a correct mba expression. the experiment shows that transformer-based model can simplify more mba expressions, but gru-based model can output expression faster. to compare the output of these methods intuitively, we extract one mba expression that can be simplified by all peer tools and neureduce from the test dataset and the reduced results are shown in ## related work recent research has applied machine learning to perform mathematical reasoning. @xcite shows how to use tree neural network to predict one logic entails another logic. the work is different from neureduce since their task is to determine the implicit relationship of two propositional logic, which is a partial order, rather than to predict the equality between two expressions. @xcite and @xcite uses neural networks to extract mathematical problems from text and output correct answers. their work is more focused on natural language understanding of math problems, rather than purely reasoning the logical equivalence of different expressions. @xcite is an extensive survey of mathematical reasoning. they provide a dataset containing a variety of mathematical samples from algebra problems to probability calculation. their work well proves that state-of-the-art neural networks can work well in mathematical reasoning problem. however, the sample of expression reduction in their work only involves simple exponential equation reduction, which is not matched to the mba expression. there has also been a recent interest in solving mathematical problems. @xcite shows how to use a recurrent neural network to extract mathematical identities with a novel grammar framework. @xcite uses a convolutional neural network to solve the problem of addition and multiplication with excellent generalization capabilities. @xcite uses a message-passing network with a bipartite graph structure to determine satisfiability in formulas of conjunctive normal form. the other relevant re-search works are shown in @xcite ; @xcite ; @xcite . ## conclusion mixed boolean-arithmetic (mba) transformation, using arithmetic and bitwise operations to translate expressions, have been applied in software obfuscation. this paper introduces a new method, neureduce, to simplify complex mba expression by recurrent neural network. due to the insufficient number of existing mba expressions for training our neural network, we first extend a method to generate mba expressions and develop a largescale mba expression dataset, including 1,000,000 diversified complex mba samples and their simplified expressions. four neural network models-lstm, gru, attention lstm, transformer-are trained and tested on the dataset. the evaluation results show that, compared with state-of-the-art tools, neureduce has the highest accuracy with negligible overhead. our experiments also show that neureduce's performance can be further improved when training on more samples.