# An In-Place Simplification on Mixed Boolean-Arithmetic Expressions

Authors: Binbin Liu; Qilong Zheng; Jing Li; Dongpeng Xu
Journal: Security and Communication Networks
 (2022)

---

## Abstract

Mixed Boolean-arithmetic (MBA) expression, which involves both bitwise operations (e.g., NOT, AND, and OR) and arithmetic operations (e.g.,+, −, and ∗), is a software obfuscation scheme. On the other side, multiple methods have been proposed to simplify MBA expressions. Among them, table-based solutions are the most powerful simplification research. However, a fundamental limitation of the table-based solutions is that the space complexity of the transformation table drastically explodes with the number of variables in the MBA expression. In this study, we propose a novel method to simplify MBA expressions without any precomputed requirements. First, a bitwise expression can be transformed into a unified form, and we provide a mathematical proof to guarantee the correctness of this transformation. Then, the arithmetic reduction is smoothly performed to further simplify the expression and produce a concise result. We implement the proposed scheme as an open-source tool, named MBA-Flatten, and evaluate it on two comprehensive benchmarks. The evaluation results show that MBA-Flatten is a general and effective MBA simplification method. Furthermore, MBA-Flatten can assist malware analysis and boost SMT solvers’ performance on solving MBA equations.


---

## Body

## 1. Introduction

Mixed Boolean-arithmetic (MBA) expression [1, 2] is defined as the expression that mixes the usage of bitwise operations (e.g., ∼, &, |, and ∧) and arithmetic operations (e.g., +, −, and ∗). Several formal methods [1, 3] are designed to generate a new complex MBA expression that is equal to a simple expression. MBA expression, which can be used to replace a simple expression with an equivalent representation that is hard to understand, is an advanced software obfuscation scheme [3–5]. The MBA obfuscation has been adopted by many academic projects and industrial products to protect software [5–9].The wide practical applications of MBA obfuscation have attracted research on simplifying MBA expression. Recent studies [10, 11] demonstrate that existing computer algebra software has a very limited effect on MBA simplification. Consequently, multiple methods are proposed to simplify MBA expressions, including bit blasting [12], pattern matching [13], program synthesis [14–16], deep learning [17, 18], and table-based solutions [5, 11]. Among them, table-based solutions are the state-of-the-art MBA simplification method. However, one strong limitation is that the complexity of creating and storing the precomputed table is O22t, where t is the number of variables in the MBA expression. Thus, it has an overwhelming overhead to produce and store the tables for any t≥5.In this study, we propose a novel scheme to simplify an MBA expression without any precomputed requirements. The key idea is that a transformation procedure can be used to reduce a bitwise expression to a unified form, and a mathematical proof is provided to guarantee the correctness of the transformation. Then, the arithmetic reduction is smoothly performed to further simplify the expression and generate the final result. We implement the approach as an open-source tool, named MBA-Flatten. To demonstrate the capability of MBA-Flatten, we evaluate it on two comprehensive MBA benchmarks. The evaluation results show that MBA-Flatten outperforms existing tools in terms of more solved MBA expressions. Due to the low-cost arithmetic computation, MBA-Flatten is also an effective MBA simplification tool. In addition, the evaluation demonstrates that MBA-Flatten can assist malware analysis and boost SMT solving on MBA equations.In summary, this study makes the following key contributions:(1)
We find that a bitwise expression can be transformed into a unified form and provide a mathematical proof to support it. To the best of our knowledge, we are the first to prove the existence of the transformation.(2)
The bitwise expression transformation paves the way for our novel in-place MBA simplification method. Our proposed scheme first replaces the bitwise expressions with the corresponding equivalent form. In this way, arithmetic reduction rules can be seamlessly applied to further produce the simplification result.(3)
We have implemented our idea as an open-source tool, called MBA-Flatten, and evaluated it on two comprehensive MBA benchmarks. The evaluation results demonstrate that MBA-Flatten is a general and effective MBA simplification method.The remainder of this study is structured as follows. Section2 shows the background of MBA expression. Section 3 illustrates the proposed scheme that can be used to simplify an MBA expression. The proof of Theorem 1 can be found in Section 4. In Section 5, we describe the experimental evaluation of the proposed approach. Section 6 discusses some limitations of our proposed scheme, and Section 7 concludes this study.


## 2. Related Work

In this section, we first introduce the background of MBA expression and its wide applications. Then, we discuss the existing research on simplifying MBA expressions, pointing out the limitations, which also serve as a motivation in this study.


### 2.1. MBA Expression

Zhou et al. [1, 2] propose the concept of mixed Boolean-arithmetic (MBA) expression based on Boolean-arithmetic algebra, which mixes the usage of bitwise operators (e.g., NOT, AND, and OR) and arithmetic operations (e.g., +, −, and ∗). MBA expression is specified as linear MBA, polynomial MBA, and non-polynomial MBA [1, 11]. The formal definitions of linear and polynomial MBA expression are denoted as follows, and the linear MBA expression is a subset of polynomial MBA expression [1]. The MBA expression, which fails to satisfy Definition 1, is considered as a non-polynomial MBA expression [11].Definition 1.
(Zhou [1]). A polynomial MBA expression is of the form:(1)Epx1,⋯,xt=∑iϵIai∗∏j∈Jiei,jx1,⋯,xt,where aiis integer constant,ei,jis bitwise expression of variablesx1,…,xtoverBn,B=0,1, n,tare positive integers, andI,Ji⊂Z, ∀i∈I.Definition 2.
(Zhou [1]). A linear MBA expression is a polynomial MBA expression of the form:(2)Elx1,⋯,xt=∑i∈Iai∗eix1,⋯,xt,where aiis integer constant,eiis bitwise expression of variablesx1,⋯,xtoverBn, B=0,1, n,tare positive integers, andI⊂Z.
Zhou et al. [1] design a generator using truth tables to produce infinite linear MBA equations. Based on existing linear MBA rules, Liu et al. [3] propose several formal methods to generate an unlimited number of polynomial and non-polynomial MBA expressions. Examples of MBA expressions are shown below. In particular, (3) is a linear MBA expression, (4) is a polynomial MBA expression, and (5) is a non-polynomial MBA expression.(3)2∗x∧y+y−3∗x|y+5,(4)x∗x∧y−x+2∗∼x|y∗xy−1,(5)x∧x+y∗y−3∗x|x+y+∼x+7.
Due to its solid theoretical foundation and simplicity of implementation, MBA expression has been applied in multiple academic tools and industrial products to protect software [5–9]. For example, Cloakware, Irdeto, and Quarkslab apply MBA obfuscation in their commercial products [5, 7]. Tigress [6], an academic C source code obfuscator, encodes simple expressions into complex MBA forms. Blazy et al. [8] develop a C program obfuscator, in which formally verified MBA obfuscation rules are integrated. Ma et al. [9] apply MBA expressions to develop a novel dynamic software watermarking scheme. Figure 1 shows how to use MBA expressions to make software obfuscation [4]. Figure 1(a) demonstrates that the expression x+y is substituted with a complex but equivalent expression. The opaque predicate [19] is shown in Figure 1(b), andthe predicate (x∗y==x∧y∗x|y+x∧∼y∗∼x∧y) is actually always true.Figure 1
Applications of MBA expression implemented in C programming language. (a) Data flow obfuscation. (b) Opaque predicate.
(a)(b)


### 2.2. MBA Expression Simplification

The wide practical application of MBA obfuscation has encouraged research on simplifying MBA expressions. Eyrolles’ PhD thesis [10] shows that popular symbol software (Maple, SageMath, Wolfram Mathematica, and Z3 [20]) fails to simplify MBA expressions. The root cause is that existing reduction rules cannot reduce expressions that mix the usage of bitwise and arithmetic operators [11]. Researchers have developed multiple solutions to simplify MBA expressions, including bit blasting [12], pattern matching [13], program synthesis [14–16], and deep learning-based [17, 18]. While promising, these simplification methods are still in their infancy: they either suffer from high-performance penalties, or they produce many false simplification cases.To effectively reduce MBA expression, researchers investigate the MBA mechanism and propose table-based solutions. Liu et al. [5] prove a two-way feature in the MBA transformation and design a two-variable transformation table to simplify MBA expression. Xu et al. [11] create multiple semantic-preserving transformation tables, which enumerate all bitwise expressions and the corresponding simplified forms. Using these transformation tables, MBA-Solver can effectively simplify an MBA expression.So far, table-based solutions are the state-of-the-art MBA simplification methods. However, the space complexity of the transformation table isO22t and t is the number of variables in the MBA expression. Therefore, table-based solutions are not scalable to reduce an MBA expression involving five or more variables. Here, (6) is a linear MBA expression with five variables, and table-based solutions fail to simplify it. Note that multiple methods are proposed to generate an unlimited number of MBA expressions [1, 3], and thus, an emerging challenge for MBA simplification is the MBA expression with five or more variables.(6)fx,y,z,t,a=−∼x∨y∨t∧∼a−∼xy∼t∧∼a−∼xyz|t∧a−∼x∧∼y∧z∨t∧a−2∗y−1+x∧y.


## 2.1. MBA Expression

Zhou et al. [1, 2] propose the concept of mixed Boolean-arithmetic (MBA) expression based on Boolean-arithmetic algebra, which mixes the usage of bitwise operators (e.g., NOT, AND, and OR) and arithmetic operations (e.g., +, −, and ∗). MBA expression is specified as linear MBA, polynomial MBA, and non-polynomial MBA [1, 11]. The formal definitions of linear and polynomial MBA expression are denoted as follows, and the linear MBA expression is a subset of polynomial MBA expression [1]. The MBA expression, which fails to satisfy Definition 1, is considered as a non-polynomial MBA expression [11].Definition 1.
(Zhou [1]). A polynomial MBA expression is of the form:(1)Epx1,⋯,xt=∑iϵIai∗∏j∈Jiei,jx1,⋯,xt,where aiis integer constant,ei,jis bitwise expression of variablesx1,…,xtoverBn,B=0,1, n,tare positive integers, andI,Ji⊂Z, ∀i∈I.Definition 2.
(Zhou [1]). A linear MBA expression is a polynomial MBA expression of the form:(2)Elx1,⋯,xt=∑i∈Iai∗eix1,⋯,xt,where aiis integer constant,eiis bitwise expression of variablesx1,⋯,xtoverBn, B=0,1, n,tare positive integers, andI⊂Z.
Zhou et al. [1] design a generator using truth tables to produce infinite linear MBA equations. Based on existing linear MBA rules, Liu et al. [3] propose several formal methods to generate an unlimited number of polynomial and non-polynomial MBA expressions. Examples of MBA expressions are shown below. In particular, (3) is a linear MBA expression, (4) is a polynomial MBA expression, and (5) is a non-polynomial MBA expression.(3)2∗x∧y+y−3∗x|y+5,(4)x∗x∧y−x+2∗∼x|y∗xy−1,(5)x∧x+y∗y−3∗x|x+y+∼x+7.
Due to its solid theoretical foundation and simplicity of implementation, MBA expression has been applied in multiple academic tools and industrial products to protect software [5–9]. For example, Cloakware, Irdeto, and Quarkslab apply MBA obfuscation in their commercial products [5, 7]. Tigress [6], an academic C source code obfuscator, encodes simple expressions into complex MBA forms. Blazy et al. [8] develop a C program obfuscator, in which formally verified MBA obfuscation rules are integrated. Ma et al. [9] apply MBA expressions to develop a novel dynamic software watermarking scheme. Figure 1 shows how to use MBA expressions to make software obfuscation [4]. Figure 1(a) demonstrates that the expression x+y is substituted with a complex but equivalent expression. The opaque predicate [19] is shown in Figure 1(b), andthe predicate (x∗y==x∧y∗x|y+x∧∼y∗∼x∧y) is actually always true.Figure 1
Applications of MBA expression implemented in C programming language. (a) Data flow obfuscation. (b) Opaque predicate.
(a)(b)


## 2.2. MBA Expression Simplification

The wide practical application of MBA obfuscation has encouraged research on simplifying MBA expressions. Eyrolles’ PhD thesis [10] shows that popular symbol software (Maple, SageMath, Wolfram Mathematica, and Z3 [20]) fails to simplify MBA expressions. The root cause is that existing reduction rules cannot reduce expressions that mix the usage of bitwise and arithmetic operators [11]. Researchers have developed multiple solutions to simplify MBA expressions, including bit blasting [12], pattern matching [13], program synthesis [14–16], and deep learning-based [17, 18]. While promising, these simplification methods are still in their infancy: they either suffer from high-performance penalties, or they produce many false simplification cases.To effectively reduce MBA expression, researchers investigate the MBA mechanism and propose table-based solutions. Liu et al. [5] prove a two-way feature in the MBA transformation and design a two-variable transformation table to simplify MBA expression. Xu et al. [11] create multiple semantic-preserving transformation tables, which enumerate all bitwise expressions and the corresponding simplified forms. Using these transformation tables, MBA-Solver can effectively simplify an MBA expression.So far, table-based solutions are the state-of-the-art MBA simplification methods. However, the space complexity of the transformation table isO22t and t is the number of variables in the MBA expression. Therefore, table-based solutions are not scalable to reduce an MBA expression involving five or more variables. Here, (6) is a linear MBA expression with five variables, and table-based solutions fail to simplify it. Note that multiple methods are proposed to generate an unlimited number of MBA expressions [1, 3], and thus, an emerging challenge for MBA simplification is the MBA expression with five or more variables.(6)fx,y,z,t,a=−∼x∨y∨t∧∼a−∼xy∼t∧∼a−∼xyz|t∧a−∼x∧∼y∧z∨t∧a−2∗y−1+x∧y.


## 3. The Proposed Scheme

To reduce MBA expressions, we first present an existing finding: a bitwise expression can be transformed into a unified form. This finding paves the way for our novel in-place MBA simplification scheme, MBA-Flatten.


### 3.1. Bitwise Expression Transformation

A bitwise expression is denoted asex1,⋯,xt of variables xk∈Bn, k=1,⋯,t. The transformation T is defined as follows:(7)∼xi↦−xi+1,xi∧xj↦xi∗xj,xi|xj↦xi+xj−xi∗xj,xi∧xj↦xi+xj−2∗xi∗xj,xi∗⋯∗xi↦xi,where xi,xj∈Bn. Equation (7) can be recursively applied to transform a bitwise expression ex1,⋯,xt into an arithmetic expression denoted as Te, which is shown as follows:(8)Te=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∗xi2+⋯+a1⋯tx1∗⋯∗xt+ae,where ai1⋯ik and ae are integers determined by e. After replacing all xij∗⋯∗xik in Te with xij∧⋯∧xik, (8) will be reduced as follows:(9)Re=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∧xi2+⋯+a1⋯tx1∧⋯∧xt+ae.An instance of the above transformation procedures is shown in Example1. One interesting observation is that there is a gap between e and Re, because ∼x1|x2 is equal to the expression −x1+x1∧x2−1 rather than −x1+x1∧x2+1.Example 1.
For a bitwise expressione=∼x1|x2, we have(10)Te=−x1+1+x2−−x1+1∗x2=−x1+x1∗x2+1,Re=−x1+x1∧x2+1.
Moreover, Theorem1 shows that the gap between a bitwise expression e and the corresponding Re is actually a constant value, 0 or −2. In other words, a bitwise expression e can be successfully reduced to a unified form, Equation (10). Theorem 1 can be proved by induction on the number of bitwise operators in the bitwise expression ex1,⋯,xt. For detailed proof of the theorem, refer to Section 4 of this study.Theorem 1.
Letn,tbe positive integers,ex1,⋯,xtbe a bitwise expression of variablesxk∈Bn, k=1,⋯,t, and Fe=Re−2∗aewith the form of(11)Fe=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∧xi2+⋯+a1⋯tx1∧⋯∧xt−ae.
Then,Fe≡ewithae=0or1.
By this theorem, Example2 shows that a bitwise expression ∼x|∼y is reduced to y−x∧y.Example 2.
For a bitwise expressione=∼x|∼y, we have(12)Te=−x+−y+1−x∗−y+1+1,=y−x∗y,Re=y−x∧y,Fe=y−x∧y.
The above procedures introduced so far are integrated into Algorithm 1. The algorithm takes a bitwise expressione as the input and outputs the transformation result e. Algorithm 1 applies arithmetic computation to transform a bitwise expression, so it does not introduce extra memory cost to maintain the heap or precomputed tables.
Algorithm 1: Transformation procedure of a bitwise expression.
(i)
Input: a bitwise expressione.(ii)
Output: the simplification result ofe.(1)
Function BitTranse(2)
Recursively apply the transformationT to transform e into Te.(3)
Replace allxij∗⋯∗xik in Te with xij&⋯&xik to get Re.(4)
Fe=Re−2∗ae.(5)
ReturnFe.(6)
End function


### 3.2. Simplifying MBA Expression

As noted above, Algorithm 1 can transform a bitwise expressione into a unified form. Using Algorithm 1, we will discuss how to simplify linear, polynomial, and non-polynomial MBA expressions.We first introduce how to simplify a linear MBA expression. According to Equation (2), a linear MBA expression is essentially a linear combination of bitwise expressions. Using Algorithm 1, the bitwise expressions in (2) are first substituted with the corresponding transformation result. After combining like terms, (2) will be reduced to the following simple form:(13)Elx1,⋯,xt=∑i=12tAi∗e˜ix1,⋯,xt=∑i1=1tAi1xi1+∑1≤i1<i2≤tAi1i2xi1∧xi2+⋯+A1⋯tx1∧⋯∧xt+AEl,where Ai is integer, e˜ix1,⋯,xt∈x1,x2,⋯,x1∧x2,x2∧x3,⋯,x1∧⋯∧xt,−1. (13) indicates that a linear MBA expression can be simplified to the concise form including at most 2t terms and t is the number of variables in the MBA expression. Example 3 shows that a complex linear MBA expression can be reduced to a simple result x+y.Example 3.
For the MBA expression in Figure1(a), we have(14)2∗x∧y+5∗x∧∼y+2∗x∧y+6∗∼x|y−1∗∼x|∼y−6∗∼y=2∗x∧y+5∗x−x∧y+2∗x+y−2∗x∧y+6∗−x−y+x∧y−1−1∗y−x∧y−6∗−y−1=x+y.
Enlighten by the above simplification procedure, using Algorithm 1, (1) will be transformed to an equivalent form shown as follows:(15)Epx1,⋯,xt=∑iϵIAi∗∏j∈Jie˜i,jx1,⋯,xt,where Ai are integers, e˜i,jx1,⋯,xt∈x1,x2,⋯,x1∧x2,x2∧x3,⋯,x1∧⋯∧xt,−1, and I,Ji⊂Z, ∀i∈I. The following example shows how to simplify a polynomial MBA expression. First, every bitwise expression is substituted with the equivalent form; e.g., x∧∼y is replaced with x−x∧y. Then, arithmetic reduction rules are performed to produce the simplification result x∗y. Note that the linear MBA expression is also polynomial, so the polynomial MBA simplification method can reduce a linear MBA expression.Example 4.
For the MBA expression in Figure1(b), we have(16)x∧y∗x|y+x∧∼y∗∼x∧y=x−x∧y∗y−x∧y+x∧y∗x+y−x∧y=x∗y−x∗x∧y−x∧y∗y+x∧y∗x∧y+x∧y∗x+x∧y∗y−x∧y∗x∧y=x∗y.
For a non-polynomial MBA expression, we notice that it includes multiple sub-expressions obfuscated by polynomial MBA rules. This finding inspires us to use the polynomial MBA simplification procedure to reduce a non-polynomial MBA expression. In particular, we first simplify the inner sub-expression (polynomial MBA expression), and the simplification result of the inner sub-expression is treated as a temporary variable to expose further reduction opportunities. An instance is shown in Example5. During the simplification procedure, the inner polynomial MBA expressions are reduced to the simplified form, such as x∧y+2∗x∧y, which is reduced to x+y. By replacing x+y with an intermediate variable t1, the expression can be further reduced to t1+x. At the last step, all temporary variables ti are substituted back to produce the final result 2∗x+y.Example 5.
For the non-polynomial MBA expressionx∧y+2∗x∧y|x+2∗x|y−x∧y∧x, we have(17)x∧y+2∗x∧y|x+2∗x|y−x∧y∧x=x+y−2∗x∧y|x+2∗x+y−x∧y−x+y−2∗x∧y∧x=x+y|x+x+y∧xt1=x+y=t1|x+t1|x=t1+x=2∗x+y.


### 3.3. Algorithm and Implementation

The MBA simplification scheme we have described above is illustrated in Algorithm 2. The algorithm takes an MBA expressionE as input and outputs its concise form. First, it checks whether the MBA expression is a polynomial MBA or not. For polynomial MBA, the algorithm applies Algorithm 1 to simplify the bitwise expressions. Then, an arithmetic reduction is performed to return the simplification result. For non-polynomial MBA, the algorithm applies the polynomial MBA simplification procedure to recursively reduce each inner sub-expression (polynomial MBA) and replace it with the simplified result. At last, the algorithm performs the arithmetic reduction to generate the final result. Note that Algorithm 2 applies Algorithm 1 and arithmetic computation to simplify an MBA expression, so it does not introduce any additional tables or manage extra heap memory.Algorithm 2: Simplification procedure of an MBA expression.
(i)
Input: an MBA expressionE.(ii)
Output: the simplification result ofE.(1)
Function MBA-FlattenE(2)
IfE is a polynomial MBA expression then(3)
Return PolySimE.(4)
Else(5)
For inner sub-expressionEi is a polynomial MBA expression do(6)
Ei′← PolySim Ei.(7)
ReplaceEi with Ei′.(8)
ReplaceEi′ with temp variable ti.(9)
End for(10)
Replace allti with Ei′.(11)
Arithmetic reduction onE.(12)
ReturnE.(13)
End if(14)
End function(15)
Function PolySimE(16)
For every bitwise expressione∈E do(17)
e′← BitTrans e.(18)
Replacee with e′ in E.(19)
End for(20)
Arithmetic reduction onE.(21)
ReturnE.(22)
End functionWe implement Algorithm 2 as an open-source tool, named MBA-Flatten. It accepts a complex MBA expression as the input and outputs the corresponding simplification result. An overview of MBA-Flatten’s architecture is shown in Figure2. The whole framework is written in around 1,800 lines of Python code. The parser and AST traversal components are coded based on the Python AST library. Moreover, we leverage the Python SymPy library for arithmetic reduction.Figure 2
An overview of MBA-Flatten’s architecture.Inside MBA-Flatten, the main program consists of three major components. First, a parser receives the MBA expression and translates it to abstract syntax tree (AST) for the remaining process. Then, MBA-Flatten reduces the expression to a concise form. For polynomial MBA expression, the program uses the transformation procedure to reduce a bitwise expression, and a math reduction module is adopted to further simplify the expression. The math reduction module also includes the optimization function to generate an optimal result for some expressions; e.g.,x+y−2∗x∧y can be further reduced to x∧y. For non-polynomial MBA expression, MBA-Flatten traverses the AST bottom-up and simplifies every inner subtree (polynomial MBA expression). After reducing each sub-expression, the simplified expression is replaced with the temporary variable. At last, arithmetic reduction rules are further performed to reduce the expression and return the final simplification result. MBA-Flatten also includes utilities for measuring the complexity metrics of MBA expressions, such as counting the number of nodes in the directed acyclic graph (DAG) representation of an MBA expression, and we will discuss the complexity measurement of MBA expressions further in Section 5.1.


## 3.1. Bitwise Expression Transformation

A bitwise expression is denoted asex1,⋯,xt of variables xk∈Bn, k=1,⋯,t. The transformation T is defined as follows:(7)∼xi↦−xi+1,xi∧xj↦xi∗xj,xi|xj↦xi+xj−xi∗xj,xi∧xj↦xi+xj−2∗xi∗xj,xi∗⋯∗xi↦xi,where xi,xj∈Bn. Equation (7) can be recursively applied to transform a bitwise expression ex1,⋯,xt into an arithmetic expression denoted as Te, which is shown as follows:(8)Te=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∗xi2+⋯+a1⋯tx1∗⋯∗xt+ae,where ai1⋯ik and ae are integers determined by e. After replacing all xij∗⋯∗xik in Te with xij∧⋯∧xik, (8) will be reduced as follows:(9)Re=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∧xi2+⋯+a1⋯tx1∧⋯∧xt+ae.An instance of the above transformation procedures is shown in Example1. One interesting observation is that there is a gap between e and Re, because ∼x1|x2 is equal to the expression −x1+x1∧x2−1 rather than −x1+x1∧x2+1.Example 1.
For a bitwise expressione=∼x1|x2, we have(10)Te=−x1+1+x2−−x1+1∗x2=−x1+x1∗x2+1,Re=−x1+x1∧x2+1.
Moreover, Theorem1 shows that the gap between a bitwise expression e and the corresponding Re is actually a constant value, 0 or −2. In other words, a bitwise expression e can be successfully reduced to a unified form, Equation (10). Theorem 1 can be proved by induction on the number of bitwise operators in the bitwise expression ex1,⋯,xt. For detailed proof of the theorem, refer to Section 4 of this study.Theorem 1.
Letn,tbe positive integers,ex1,⋯,xtbe a bitwise expression of variablesxk∈Bn, k=1,⋯,t, and Fe=Re−2∗aewith the form of(11)Fe=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∧xi2+⋯+a1⋯tx1∧⋯∧xt−ae.
Then,Fe≡ewithae=0or1.
By this theorem, Example2 shows that a bitwise expression ∼x|∼y is reduced to y−x∧y.Example 2.
For a bitwise expressione=∼x|∼y, we have(12)Te=−x+−y+1−x∗−y+1+1,=y−x∗y,Re=y−x∧y,Fe=y−x∧y.
The above procedures introduced so far are integrated into Algorithm 1. The algorithm takes a bitwise expressione as the input and outputs the transformation result e. Algorithm 1 applies arithmetic computation to transform a bitwise expression, so it does not introduce extra memory cost to maintain the heap or precomputed tables.
Algorithm 1: Transformation procedure of a bitwise expression.
(i)
Input: a bitwise expressione.(ii)
Output: the simplification result ofe.(1)
Function BitTranse(2)
Recursively apply the transformationT to transform e into Te.(3)
Replace allxij∗⋯∗xik in Te with xij&⋯&xik to get Re.(4)
Fe=Re−2∗ae.(5)
ReturnFe.(6)
End function


## 3.2. Simplifying MBA Expression

As noted above, Algorithm 1 can transform a bitwise expressione into a unified form. Using Algorithm 1, we will discuss how to simplify linear, polynomial, and non-polynomial MBA expressions.We first introduce how to simplify a linear MBA expression. According to Equation (2), a linear MBA expression is essentially a linear combination of bitwise expressions. Using Algorithm 1, the bitwise expressions in (2) are first substituted with the corresponding transformation result. After combining like terms, (2) will be reduced to the following simple form:(13)Elx1,⋯,xt=∑i=12tAi∗e˜ix1,⋯,xt=∑i1=1tAi1xi1+∑1≤i1<i2≤tAi1i2xi1∧xi2+⋯+A1⋯tx1∧⋯∧xt+AEl,where Ai is integer, e˜ix1,⋯,xt∈x1,x2,⋯,x1∧x2,x2∧x3,⋯,x1∧⋯∧xt,−1. (13) indicates that a linear MBA expression can be simplified to the concise form including at most 2t terms and t is the number of variables in the MBA expression. Example 3 shows that a complex linear MBA expression can be reduced to a simple result x+y.Example 3.
For the MBA expression in Figure1(a), we have(14)2∗x∧y+5∗x∧∼y+2∗x∧y+6∗∼x|y−1∗∼x|∼y−6∗∼y=2∗x∧y+5∗x−x∧y+2∗x+y−2∗x∧y+6∗−x−y+x∧y−1−1∗y−x∧y−6∗−y−1=x+y.
Enlighten by the above simplification procedure, using Algorithm 1, (1) will be transformed to an equivalent form shown as follows:(15)Epx1,⋯,xt=∑iϵIAi∗∏j∈Jie˜i,jx1,⋯,xt,where Ai are integers, e˜i,jx1,⋯,xt∈x1,x2,⋯,x1∧x2,x2∧x3,⋯,x1∧⋯∧xt,−1, and I,Ji⊂Z, ∀i∈I. The following example shows how to simplify a polynomial MBA expression. First, every bitwise expression is substituted with the equivalent form; e.g., x∧∼y is replaced with x−x∧y. Then, arithmetic reduction rules are performed to produce the simplification result x∗y. Note that the linear MBA expression is also polynomial, so the polynomial MBA simplification method can reduce a linear MBA expression.Example 4.
For the MBA expression in Figure1(b), we have(16)x∧y∗x|y+x∧∼y∗∼x∧y=x−x∧y∗y−x∧y+x∧y∗x+y−x∧y=x∗y−x∗x∧y−x∧y∗y+x∧y∗x∧y+x∧y∗x+x∧y∗y−x∧y∗x∧y=x∗y.
For a non-polynomial MBA expression, we notice that it includes multiple sub-expressions obfuscated by polynomial MBA rules. This finding inspires us to use the polynomial MBA simplification procedure to reduce a non-polynomial MBA expression. In particular, we first simplify the inner sub-expression (polynomial MBA expression), and the simplification result of the inner sub-expression is treated as a temporary variable to expose further reduction opportunities. An instance is shown in Example5. During the simplification procedure, the inner polynomial MBA expressions are reduced to the simplified form, such as x∧y+2∗x∧y, which is reduced to x+y. By replacing x+y with an intermediate variable t1, the expression can be further reduced to t1+x. At the last step, all temporary variables ti are substituted back to produce the final result 2∗x+y.Example 5.
For the non-polynomial MBA expressionx∧y+2∗x∧y|x+2∗x|y−x∧y∧x, we have(17)x∧y+2∗x∧y|x+2∗x|y−x∧y∧x=x+y−2∗x∧y|x+2∗x+y−x∧y−x+y−2∗x∧y∧x=x+y|x+x+y∧xt1=x+y=t1|x+t1|x=t1+x=2∗x+y.


## 3.3. Algorithm and Implementation

The MBA simplification scheme we have described above is illustrated in Algorithm 2. The algorithm takes an MBA expressionE as input and outputs its concise form. First, it checks whether the MBA expression is a polynomial MBA or not. For polynomial MBA, the algorithm applies Algorithm 1 to simplify the bitwise expressions. Then, an arithmetic reduction is performed to return the simplification result. For non-polynomial MBA, the algorithm applies the polynomial MBA simplification procedure to recursively reduce each inner sub-expression (polynomial MBA) and replace it with the simplified result. At last, the algorithm performs the arithmetic reduction to generate the final result. Note that Algorithm 2 applies Algorithm 1 and arithmetic computation to simplify an MBA expression, so it does not introduce any additional tables or manage extra heap memory.Algorithm 2: Simplification procedure of an MBA expression.
(i)
Input: an MBA expressionE.(ii)
Output: the simplification result ofE.(1)
Function MBA-FlattenE(2)
IfE is a polynomial MBA expression then(3)
Return PolySimE.(4)
Else(5)
For inner sub-expressionEi is a polynomial MBA expression do(6)
Ei′← PolySim Ei.(7)
ReplaceEi with Ei′.(8)
ReplaceEi′ with temp variable ti.(9)
End for(10)
Replace allti with Ei′.(11)
Arithmetic reduction onE.(12)
ReturnE.(13)
End if(14)
End function(15)
Function PolySimE(16)
For every bitwise expressione∈E do(17)
e′← BitTrans e.(18)
Replacee with e′ in E.(19)
End for(20)
Arithmetic reduction onE.(21)
ReturnE.(22)
End functionWe implement Algorithm 2 as an open-source tool, named MBA-Flatten. It accepts a complex MBA expression as the input and outputs the corresponding simplification result. An overview of MBA-Flatten’s architecture is shown in Figure2. The whole framework is written in around 1,800 lines of Python code. The parser and AST traversal components are coded based on the Python AST library. Moreover, we leverage the Python SymPy library for arithmetic reduction.Figure 2
An overview of MBA-Flatten’s architecture.Inside MBA-Flatten, the main program consists of three major components. First, a parser receives the MBA expression and translates it to abstract syntax tree (AST) for the remaining process. Then, MBA-Flatten reduces the expression to a concise form. For polynomial MBA expression, the program uses the transformation procedure to reduce a bitwise expression, and a math reduction module is adopted to further simplify the expression. The math reduction module also includes the optimization function to generate an optimal result for some expressions; e.g.,x+y−2∗x∧y can be further reduced to x∧y. For non-polynomial MBA expression, MBA-Flatten traverses the AST bottom-up and simplifies every inner subtree (polynomial MBA expression). After reducing each sub-expression, the simplified expression is replaced with the temporary variable. At last, arithmetic reduction rules are further performed to reduce the expression and return the final simplification result. MBA-Flatten also includes utilities for measuring the complexity metrics of MBA expressions, such as counting the number of nodes in the directed acyclic graph (DAG) representation of an MBA expression, and we will discuss the complexity measurement of MBA expressions further in Section 5.1.


## 4. Proof of Theorem 1

To prove Theorem1, we first present that the transformation T is well defined. The definitions of value and form equivalence between two MBA expressions are shown as follows.Definition 3.
Suppose two MBA expressionsE1x1,⋯,xt,E2x1,⋯,xtof variablesxk∈Bn,k=1,⋯,t.E1x1,⋯,xt=VE2x1,⋯,xt if E1a1,⋯,at≡E2a1,⋯,at for all ak∈BnE1x1,⋯,xt=FE2x1,⋯,xt if E1x1,⋯,xt and E2x1,⋯,xt are of the same form
The maps in Equation (7) are identical in one-bit space. In other words, the bitwise expression e is equivalent to Te with xk∈B, which is shown as follows:(18)Te1x1,⋯,xt=Ve1x1,⋯,xt,xk∈B,k=1,⋯,t.
Proposition1 shows that the transformation T is well defined, and one instance is shown in Example 6.Proposition 1.
Letenbe the bitwise expression of variablesxk∈Bn,k=1,⋯,t. Given two bitwise expressionse1nande2n, ife1n=Ve2n, thenTe1n=FTe2n.Proof.
e1n=Ve2n induces e11=Ve21. According to Equation (18), there is Te11=VTe21. Note the uniqueness of Te, and then, Te11=FTe21. Since Te1=FTen, we have Te1n=FTe2n.Example 6.
For the bitwise expressionse1=∼x1∧x2, e2=x1∧x2|∼x1∧∼x2, and e1=e2. We have(19)Te1=−x1+x2−2∗x1∗x2+1=−x1−x2+2∗x1∗x2+1,Te2=x1∗x2+−x1+1∗−x2+1−x1∗x2∗−x1+1∗−x2+1=−x1−x2+2∗x1∗x2+1.
Thus,Te1=Te2.
Next, we present the concept of the signature vector shown as follows. The signature vector of a linear MBA expression is a vector with2t dimensions, where t is the number of variables in the expression.Definition 4.
(Xu [11]). LetE=∑i=1saieibe a linear MBA expression, whereaiis integers andeiis bitwise expressions. Let M be the2t∗sBoolean matrix representing the truth table ofe1,⋯es, v⟶=a1,⋯,asT.The signature vectorsEis the product of the MBA truth table matrixMand the coefficient vectorv⟶.(20)sE=Mv⟶.
Table1 shows the truth table of multiple 2-variable bitwise expressions, and the column with all “1” is encoded as “−1” [1, 11]. Using Table 1, Example 7 presents the procedure of calculating the signature vector for expression −x1−x2+2∗x1∧x2−1. The signature vector of a bitwise expression is actually to treat its corresponding truth table as a column vector, such as sx1∧x2=0,0,0,1T.Table 1
Truth table of multiple bitwise expressions with 2 variables.
x2x1∼x1∼x2x1&x2x1|x2−10011001010101110100111100111Example 7.
For a linear MBA expressionE=−x1−x2+2∗x1∧x2−1, using Table 1, we have(21)M=0001100101011111,v⟶=−1−121,sE=Mv⟶=1001.
Then, we introduce the following lemma.Lemma 1.
(Xu [11]). Given two linear MBA expressionsE1andE2,E1=E2, if and only ifsE1=sE2.
Using Proposition1 and Lemma 1, Theorem 1 can be proved as below.Proof.
Letsej be the jth element of se, j=1,⋯,2t. Note that Equation (11) is a linear MBA expression, s−1j=1, and sej=0 or 1.
We proveFe≡e using mathematical induction on the number of bitwise operators in the expression ex1,⋯,xt of variables xk∈Bn.
Base step: the basis is the bitwise expressionex1,⋯,xt with a single bitwise operator, which is one of the following four cases:(22)∼x,x∧y,x|y,andx∧y,where x,y∈x1,⋯,xt.Case 1.
Supposee=∼x, we have Te=−x+1, and then, ae=1; thus Fe=−x−1.Ifsxj=0, then sej=1 and sFej=−sxj+s−1j=1Ifsxj=1, then sej=0 and sFej=−sxj+s−1j=0
Therefore,sej≡sFej.Case 2.
Supposee=x∧y, we have Te=x∗y, and then, ae=0; thus, Fe=x∧y. It is plainly correct that sej≡sFej.Case 3.
Supposee=x|y, we have Te=x+y−x∗y, and then, ae=0; thus Fe=x+y−x∧y.Ifsxj=0 and syj=0, then sej=0 and sFej=sxj+syj−sx∧yj=0Ifsxj=0 and syj=0, then sej=1 and sFej=sxj+syj−sx∧yj=1Ifsxj=1 and syj=0, then sej=1 and sFej=sxj+syj−sx∧yj=1Ifsxj=1 and syj=1, then sej=1 and sFej=sxj+syj−sx∧yj=1
Therefore,sej≡sFej.Case 4.
Supposee=x∧y, proven as above.
The above four cases led toae=0 or 1 and sej≡sFej that implies se≡sFe. By Lemma 1, e≡Fe holds where variables xk∈Bn.
Induction step: assumeFe≡e holds with r bitwise operators r≥1 in e. Performing one more bitwise operator to e, the new expression e¯x1,⋯,xt is one of the following forms:(23)∼e,e∧x,x∧e,ex,xe,e∧x,x∧e,where x∈x1,⋯,xt. Due to the commutative law of bitwise operators ∧,|,∧ and the following equations:(24)e∧∼x=∼∼e|x,e|∼x=∼∼e∧x,e∧∼x=∼∼e∧x,we only need to show that Fe¯≡e¯ holds on the following four cases with r+1 bitwise operators:(25)∼e,e∧x,e|x,e∧x.
AssumeFe≡e with ae=0, and we get se≡sFe and the following inductive hypothesis:(26)Te=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∗xi2+⋯+a1⋯tx1∗⋯∗xt,(27)Fe=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∧xi2+⋯+a1⋯tx1∧⋯∧xt.Case 5.
Supposee¯=∼e; from the inductive hypothesis (Equation (26)), we have(28)Te=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∗xi2−⋯−a1⋯tx1∗⋯∗xt+1.
Then,ae¯=1; thus,(29)Fe¯=∑i1=1tai1xi1−∑1≤i1<i2≤tai1i2xi1∧xi2−⋯−a1⋯tx1∧⋯∧xt−1.
According to (27), we get Fe¯=−Fe−1.Ifsej=0, then se¯j=1 and sFe¯j=−sFej+s−1j=1Ifsej=1, then se¯j=0 and sFe¯j=−sFej+s−1j=0
Therefore,sej≡sFej.Case 6.
Supposee¯=e∧x; from the inductive hypothesis (Equation (26)), we have(30)Te¯=∑i1=1tai1xi1∗x+∑1≤i1<i2≤tai1i2xi1∗xi2∗x+⋯+a1⋯tx1∗⋯∗xt∗x.
Then,ae¯=0; thus,(31)Fe¯=∑i1=1tai1xi1∧x+∑1≤i1<i2≤tai1i2xi1∧xi2∧x+⋯+a1⋯tx1∧⋯∧xt∧x.
Ifsxj=0, then se¯j=0 and(32)sFe¯j=∑i1=1tai1∗sxi1∧xj+∑1≤i1<i2≤tai1i2∗sxi1∧xi2∧xj+⋯+a1⋯t∗sx1∧⋯∧xt∧xj.=∑i1=1tai1∗0+∑1≤i1<i2≤tai1i2∗0+⋯+a1⋯t∗0=0.
Ifsxj=1, then se¯j=sej and(33)sFe¯j=∑i1=1tai1∗sxi1j+∑1≤i1<i2≤tai1i2∗sxi1∧xi2jc+⋯+a1⋯t∗sx1∧⋯∧xtj=sFej.
Therefore,sej≡sFej.Case 7.
Supposee¯=e|x; from the inductive hypothesis (Equation (26)), we have(34)Te¯=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∗xi2+⋯+a1⋯tx1∗⋯∗xt+x−∑i1=1tai1xi1∗x+∑1≤i1<i2≤tai1i2xi1∗xi2∗x−⋯−a1⋯tx1∗⋯∗xt∗x.
Then,ae¯=0; thus,(35)Fe¯=∑i1=1tai1xi1+∑1≤i1<i2≤tai1i2xi1∧xi2+⋯+a1⋯tx1∧⋯∧xt+x−∑i1=1tai1xi1∧x+∑1≤i1<i2≤tai1i2xi1∧xi2∧x−⋯−a1⋯tx1∧⋯∧xt∧x.
According to (27) and (31), we get Fe¯=Fe+x−Fe∧x.Ifsxj=0, then se¯j=sej and sFe¯j=sFej+sxj−sFe∧xj=sFejIfsxj=1, then se¯j=1 and sFe¯j=sFej+sxj−sFe∧xj=sFej+1−sej=1
Therefore,sej≡sFej.Case 8.
Supposee¯=e∧x, proven as above.
The above four cases led toae¯=0 or 1 and se¯j≡sFe¯j that implies se¯≡sFe¯. By Lemma 1, e¯≡Fe¯ holds where variables xk∈Bn.
AssumeFe≡e with ae=1; from the similar discussion as above, we have(36)ae¯=0,ife¯=∼eore∧x,1,ife¯=e|xore∧x,.ande¯≡Fe¯ with variables xk∈Bn.
As discussed above, the induction is completed. Thus, we haveFe≡e with variables xk∈Bn and ae=0 or 1 determined by e.


## 5. Experimental Results

In this section, a set of experiments are conducted to evaluate the MBA simplification scheme, MBA-Flatten. We first run MBA-Flatten and existing peer tools on two comprehensive MBA benchmarks. Z3 SMT solver [19] is used to check whether the simplified result is equivalent to the original MBA expression. The corresponding simplification results are discussed in Section 5.2–5.4. As reported in Section 5.5 and 5.6, MBA-Flatten can assist humans in analyzing software. At last, Section 5.7 studies MBA-Flatten’s performance data, such as running time and memory footprint.


### 5.1. Experimental Setup

#### 5.1.1. Peer Tools for Comparison

We collect and check existing state-of-the-art MBA simplification tools: MBA-Blast [5] and MBA-Solver [11]. MBA-Blast is a Python tool for simplifying MBA expressions via a two-variable transformation table. MBA-Solver produces multiple precomputed transformation tables, which enumerate all bitwise expressions and corresponding concise forms. Then, MBA-Solver uses these tables to simplify an MBA expression. For a more thorough evaluation, we also check other MBA simplification tools: GraphMR [18], SSPAM [13], and Syntia [14]. GraphMR is a neural network-based solution to reduce an MBA expression. SSPAM (symbolic simplification with pattern matching) is a pattern matching method that detects and reduces MBA expressions by multiple known MBA rules. Syntia is a program synthesis framework for approximating the semantics of expressions. It uses a set of input-output samples from the expression, learns the semantics of the samples, and synthesizes a simpler expression that is equal to the original expression.


#### 5.1.2. Benchmarks

To fully expose the capability of diverse methods on simplifying MBA expressions, a large scale of MBA expressions is required for evaluation. Therefore, we consider two comprehensive MBA benchmarks: Dataset 1 [14] and Dataset 2 [11]. Dataset 1 comprises 500 MBA samples generated by Tigress [6] with up to three variables. Dataset 2 collects 3,000 MBA equations with up to four variables, which contains 2,000 polynomial MBA (1,000 linear MBA) and 1,000 non-polynomial MBA expressions. Every sample in datasets is a 2-tuple: (Ec, Eg). Ec is the complex MBA expression, and Eg is the related equivalent simple form. Multiple samples in benchmarks are shown in Table 2.Table 2
MBA samples in the benchmarks.
EcEga∧∼a+2∗a|a+1a+a2∗∼x∧y+3∗∼x&y+3∗x&∼y−2∗∼x&yx+y∼x&y∗x|y+x&∼y∗∼x&y−1−x∗y


#### 5.1.3. MBA Complexity Metrics

We use the following metrics to measure MBA complexity: number of DAG nodes and MBA alternation. For example, the expression∼x∧y+3∗x|y, whose DAG representation is shown in Figure 3, has 8 nodes and an MBA alternation (a red arrow means one MBA alternation) of 2. The larger a metric’s value, the more complex an MBA expression. We expect the metrics’ values will be reduced after simplification.(1)
Number of DAG Nodes. An MBA expression is transformed into a directed acyclic graph (DAG) representation in which the nodes are operators, variables, and constants. The number of nodes in the DAG is defined as a complexity metric for an MBA expression.(2)
MBA Alternation. The MBA complexity mainly comes from mixing bitwise operations and arithmetic operations. We adopt “MBA alternation” to measure the number of edges linking different types of operations in the DAG representation of an MBA expression.Figure 3
DAG representation of an MBA expression∼x&y+3∗x|y.


#### 5.1.4. Machine Configuration

All of our experiments are performed on a server with Intel Core i9 3.00 GHz CPU, 64 GB DDR4 RAM, 2 TB SSD Hard Drive, and running Ubuntu 20.04 OS.


### 5.2. Simplification on Dataset 1

In the first experiment, we run MBA-Flatten and other peer tools on Dataset 1. The evaluation result in Table3 shows that only MBA-Flatten successfully produces verifiable simplification outputs for all MBA expressions with negligible overhead (within 0.1 seconds).Table 3
Simplification results using Dataset 1.
Tools✓✗TimeoutRatio (%)Average time (s)GraphMR137363027.40.01SSPAM332168066.41.45Syntia369131073.838.5MBA-Blast41608483.20.02MBA-Solver45404690.80.02MBA-Flatten50000100.00.02We first study thecorrectness that means an expression before and after simplification is semantically equivalent. Z3 solver [19] is adopted to check whether the output of a simplification tool is equivalent to the input. The solver may not return the solving result due to the MBA’s complexity, so we set 1 hour as a practical threshold for this and the following experiments.Table3 presents the number of MBA expressions that can be reduced by simplification tools. GraphMR is trained on the linear MBA dataset, so it can only simplify 137 of 500 MBA expressions. SSPAM outputs 168 wrong simplification results because of the limited number of MBA rules in the pattern library. Syntia uses stochastic program synthesis to generate a simple expression, which successfully synthesizes 369 simplification results. MBA-Blast performs well on simplifying 2-variable MBA expressions rather than three or more variables, and therefore, it generates 416 simplification results. MBA-Solver can successfully simplify the majority of the MBA expressions (454 of 500), but it cannot process several special cases, e.g., the non-polynomial MBA expression including sub-expression ∼x−1. In contrast to MBA-Solver, MBA-Flatten can successfully simplify all 500 MBA samples, and it reduces ∼x−1 to the expression −x.Next, we investigate theeffectiveness that reflects how much complexity is reduced by the simplification methods. Table 4 reports the expression complexity before and after simplification. Two quantitative metrics are used to measure expression complexity: the number of DAG nodes and MBA alternation. Table 4 shows that all simplification tools (except SSPAM) can considerably reduce the complexity measurement of the solved MBA expressions. SSPAM cannot effectively reduce a complex MBA expression to a simpler form due to the limited known MBA rules used in the software.Table 4
Complexity metrics of the results on correctly simplified samples in Dataset 1 before and after simplification.
ToolsAverage # of nodesAverage MBA alternationBeforeAfterA/B (%)BeforeAfterA/B (%)GraphMR9.73.637.13.60.25.6SSPAM6.24.064.52.41.562.5Syntia9.43.436.23.70.25.4MBA-Blast9.03.538.93.30.26.1MBA-Solver9.63.637.53.60.25.6MBA-Flatten9.83.737.83.70.25.4


### 5.3. Simplification on Dataset 2

As the second experiment, we run MBA-Flatten and other baseline tools on Dataset 2. As shown in Table5, MBA-Flatten can successfully simplify 2,943 of 3,000 MBA expressions, and its average processing time is less than 0.2 seconds.Table 5
Simplification results using Dataset 2.
Tools✓✗TimeoutRatio (%)Average time (s)GraphMR3792621012.60.01SSPAM705320197523.5143.1Syntia4372563014.638.9MBA-Blast17630123758.80.05MBA-Solver2899010196.70.10MBA-Flatten294305798.10.16Considering the MBA expression in Dataset 2 is more complex and diverse than the one in Dataset 1, this experiment exposes more detailed findings. GraphMR and Syntia have limited effect on simplifying complex MBA expression, which can only correctly simplify less than 450 MBA samples. SSPAM cannot generate a simpler expression, so nearly 2/3 (1,975 of 3,000) of the simplified results cannot be checked by the Z3 solver within the time threshold. Compared with MBA-Blast (1,763 simplified samples), MBA-Solver can reduce more MBA expressions with three or four variables, and it successfully simplifies 2,899 MBA samples. MBA-Flatten can reduce 2,943 MBA samples, but it fails to simplify several special cases. One exception is the non-polynomial MBA expression∼x−1∧y∗∼x−1|y+∼x−1∧∼y∗∼∼x−1∧y. Table 6 reports that all solutions (except SSPAM) can generate a simpler equivalent expression. Overall, MBA-Flatten presents its advanced capability by successfully simplifying 98.1% of MBA samples.Table 6
Complexity metrics of the results on correctly simplified samples in Dataset 2 before and after simplification.
ToolsAverage # of nodesAverage MBA alternationBeforeAfterA/B (%)BeforeAfterA/B (%)GraphMR32.16.921.56.80.913.2SSPAM35.330.486.17.56.586.7Syntia30.95.417.56.20.711.3MBA-Blast37.410.427.911.61.512.9MBA-Solver45.413.229.112.22.117.2MBA-Flatten45.311.224.712.31.512.2Furthermore, we compare the average solving time of simplification tools on the two benchmarks. From Tables3 and 5, the simplification time of GraphMR and Syntia is almost not increased, but SSPAM takes much more time when it simplifies a more complex MBA expression. MBA-Blast takes less than 0.1 seconds to simplify a two-variable MBA expression. Compared with MBA-Solver, MBA-Flatten takes slightly more time to simplify an MBA expression. The main reason is that MBA-Solver directly gets the bitwise expression simplification results from the transformation tables, rather than reduces it by multiple simplification procedures.


### 5.4. Case Study

The evaluation results in Tables3 and 5 show that MBA-Solver and MBA-Flatten are the most powerful MBA simplification tools. Throughout this case study, we demonstrate the strengths and weaknesses between MBA-Solver and MBA-Flatten.We manually check the MBA expressions solved by MBA-Solver or MBA-Flatten, and one interesting observation is that MBA-Flatten can reduce all polynomial MBA expressions in the datasets, as MBA-Solver does. Does this scenario mean that MBA-Solver and MBA-Flatten can be substituted for each other? The answer is relevant to the number of variables in an MBA expression: as described in Section2.2, MBA-Solver can successfully simplify a polynomial MBA expression with up to four variables; compared with MBA-Flatten, MBA-Solver is more efficient when it reduces an MBA expression. However, MBA-Flatten can simplify a polynomial MBA expression with an arbitrary number of variables, and the form of simplification result is shown in Equation (15). The following example shows how to apply MBA-Flatten to simplify Equation (6), which is an MBA expression with five variables.Example 8.
For Equation (6), we have(37)A=−∼x|y|t∧∼a=−a∧t∧x∧y−a∧t∧x−a∧t∧y+a∧t−a∧x∧y+a∧x+a∧y−a−t∧x∧y+t∧x+t∧y−t+x∧y−x−y−1,B=−∼xy∼t∧∼a=−−a∧t∧x∧y+a∧t∧x+a∧t∧y−a∧t+t∧x∧y−t∧x−t∧y+t,C=−∼x|y|z|t∧a=−a∧t∧x∧y∧z−a∧t∧x∧y−a∧t∧x∧z+a∧t∧x+a−a∧t∧y∧z+a∧t∧y+a∧t∧z−a∧t−a∧x∧y∧z+a∧x∧y+a∧x∧z−a∧x+a∧y∧z−a∧y−a∧z,,D=−∼x∧∼y∧z|t∧a=−−a∧t∧x∧y∧z+a∧t∧x∧y+a∧t∧x∧z−a∧t∧x+a∧t∧y∧z−a∧t∧y−a∧t∧z+a∧t+a∧x∧y∧z−a∧x∧z−a∧y∧z+a∧z,and thus,(38)fx,y,z,t,a=A+B+C+D−2∗y−1+x∧y=x−y.
The other observation is that MBA-Flatten can simplify all non-polynomial MBA expressions solved by MBA-Solver, but not vice versa. It is because that MBA-Solver treats the common sub-expression as an intermediate variable, rather than a sub-expression itself. Therefore, MBA-Flatten can simplify more special cases that cannot be simplified by MBA-Solver. Moreover, MBA-Flatten can reduce a non-polynomial MBA expression with five or more variables.
From the description above, MBA-Flatten is a general MBA simplification method.


### 5.5. MBA-Powered Malware Deobfuscation

MBA expression is always used to obfuscate code, so malware developer also adopts the MBA expression to complicate the program. Liu et al. [5] report that MBA expressions are used in a ransomware sample to protect the encryption key, and they also observe that MBA rules are integrated into the software obfuscator VMProtect, which is widely used by malware developers.In this experiment, we demonstrate that MBA-Flatten can assist in reverse-engineering the malware obfuscated by MBA expressions. We collect all MBA expressions used in malware from existing work [5]. Then, MBA-Flatten is applied to simplify the expressions, and the Z3 solver is used to check the correctness of the simplified result. The evaluation result shows that MBA-Flatten can successfully simplify all MBA expressions collected from existing malware samples. One simplification procedure is shown as follows, and MBA-Flatten produces the final result x−y.(39)∼∼x+y∧∼∼x+y=∼−x−1+y∧∼−x−1+yt1=−x−1+y=∼t1∧∼t1=−t1–1=x−y.Furthermore, we replace the MBA expressions used in malware with new MBA expressions involving five or more variables and produce 130 variants, such as the above expression∼∼x+y∧∼∼x+y, which is replaced with Equation (6). We apply MBA-Blast and MBA-Flatten to simplify the new MBA expressions. Unfortunately, MBA-Blast fails to simplify them. In contrast, MBA-Flatten can successfully simplify all new MBA expressions. Therefore, this experiment shows that MBA-Flatten can simplify the MBA expressions used in existing malware and the complex MBA expression with five or more variables.


### 5.6. Boosting SMT Solving MBA Equations

Satisfiability modulo theory (SMT) solvers have been widely applied in diverse software engineering areas, such as software analysis [21, 22], symbolic execution [23, 24], and test generation [25]. Existing work [10, 11] has presented that SMT solvers are hard to solve MBA equations. However, the MBA simplification method, MBA-Solver, can be used to boost the SMT solver’s performance on solving MBA equations (11).In this experiment, we report that MBA-Flatten (denoted as MF) can assist SMT solvers in solving MBA equations. We consider the benchmark from work [11] and test three popular SMT solvers: Boolector [26], STP [27], and Z3 [20]. The benchmark is actually considered as Dataset 2 in this study, and MBA-Solver (denoted as MS) is considered as the baseline. MBA-Flatten and MBA-Solver are used to simplify all MBA equations in the benchmark, and then, the simplification results are output to the three SMT solvers.The evaluation result is shown in Table7, and the solving time threshold is set as 1 hour. Before simplification, all three SMT solvers can only solve a small portion (Boolector 496 (16.5%), STP 98 (3.3%), Z3 84 (2.8%)) of the MBA equations within the time threshold, but after simplification, all three solvers can solve over 96% of MBA equations. Compared with MBA-Solver, all SMT solvers can solve more MBA equations after MBA-Flatten’s simplification. This is because MBA-Flatten can successfully simplify more MBA expressions than MBA-solver, as shown in Table 5. After MBA-Flatten’s simplification, all SMT solvers can solve 2,943 of 3,000 MBA equations, which means that the distinction between solvers’ performance on solving MBA expressions becomes insignificant. These results indicate that MBA-Flatten is a generic method to boost SMT solver’s performance on solving MBA expressions.Table 7
Experiment result of SMT solving on Dataset 2.
BoolectorSTPZ3BeforeMSMFBeforeMSMFBeforeMSMFPolynomial4682000200070200020005620002000Non-polynomial288999432889994328899943Total4962899294398289929438428992943


### 5.7. Performance

This section reports MBA-Flatten’s performance data. Table8 shows the time and memory cost when MBA-Flatten processes an MBA expression with different complexity measured by the number of nodes. For every complexity measurement, 100 different MBA expressions are generated to do the test. As some of the timings are small, we repeat every test 100 times. MBA-Flatten is effective because it only performs low-cost arithmetic computation. Our implementation adopts the Python SymPy library to efficiently perform the arithmetic reduction. Overall, MBA-Flatten is an effective tool for simplifying MBA expressions.Table 8
MBA-Flatten’s performance on MBA expressions with different complexity.
# of nodesTime (s)Memory (MB)100.020.2500.181.11000.534.31500.917.6


## 5.1. Experimental Setup

### 5.1.1. Peer Tools for Comparison

We collect and check existing state-of-the-art MBA simplification tools: MBA-Blast [5] and MBA-Solver [11]. MBA-Blast is a Python tool for simplifying MBA expressions via a two-variable transformation table. MBA-Solver produces multiple precomputed transformation tables, which enumerate all bitwise expressions and corresponding concise forms. Then, MBA-Solver uses these tables to simplify an MBA expression. For a more thorough evaluation, we also check other MBA simplification tools: GraphMR [18], SSPAM [13], and Syntia [14]. GraphMR is a neural network-based solution to reduce an MBA expression. SSPAM (symbolic simplification with pattern matching) is a pattern matching method that detects and reduces MBA expressions by multiple known MBA rules. Syntia is a program synthesis framework for approximating the semantics of expressions. It uses a set of input-output samples from the expression, learns the semantics of the samples, and synthesizes a simpler expression that is equal to the original expression.


### 5.1.2. Benchmarks

To fully expose the capability of diverse methods on simplifying MBA expressions, a large scale of MBA expressions is required for evaluation. Therefore, we consider two comprehensive MBA benchmarks: Dataset 1 [14] and Dataset 2 [11]. Dataset 1 comprises 500 MBA samples generated by Tigress [6] with up to three variables. Dataset 2 collects 3,000 MBA equations with up to four variables, which contains 2,000 polynomial MBA (1,000 linear MBA) and 1,000 non-polynomial MBA expressions. Every sample in datasets is a 2-tuple: (Ec, Eg). Ec is the complex MBA expression, and Eg is the related equivalent simple form. Multiple samples in benchmarks are shown in Table 2.Table 2
MBA samples in the benchmarks.
EcEga∧∼a+2∗a|a+1a+a2∗∼x∧y+3∗∼x&y+3∗x&∼y−2∗∼x&yx+y∼x&y∗x|y+x&∼y∗∼x&y−1−x∗y


### 5.1.3. MBA Complexity Metrics

We use the following metrics to measure MBA complexity: number of DAG nodes and MBA alternation. For example, the expression∼x∧y+3∗x|y, whose DAG representation is shown in Figure 3, has 8 nodes and an MBA alternation (a red arrow means one MBA alternation) of 2. The larger a metric’s value, the more complex an MBA expression. We expect the metrics’ values will be reduced after simplification.(1)
Number of DAG Nodes. An MBA expression is transformed into a directed acyclic graph (DAG) representation in which the nodes are operators, variables, and constants. The number of nodes in the DAG is defined as a complexity metric for an MBA expression.(2)
MBA Alternation. The MBA complexity mainly comes from mixing bitwise operations and arithmetic operations. We adopt “MBA alternation” to measure the number of edges linking different types of operations in the DAG representation of an MBA expression.Figure 3
DAG representation of an MBA expression∼x&y+3∗x|y.


### 5.1.4. Machine Configuration

All of our experiments are performed on a server with Intel Core i9 3.00 GHz CPU, 64 GB DDR4 RAM, 2 TB SSD Hard Drive, and running Ubuntu 20.04 OS.


## 5.1.1. Peer Tools for Comparison

We collect and check existing state-of-the-art MBA simplification tools: MBA-Blast [5] and MBA-Solver [11]. MBA-Blast is a Python tool for simplifying MBA expressions via a two-variable transformation table. MBA-Solver produces multiple precomputed transformation tables, which enumerate all bitwise expressions and corresponding concise forms. Then, MBA-Solver uses these tables to simplify an MBA expression. For a more thorough evaluation, we also check other MBA simplification tools: GraphMR [18], SSPAM [13], and Syntia [14]. GraphMR is a neural network-based solution to reduce an MBA expression. SSPAM (symbolic simplification with pattern matching) is a pattern matching method that detects and reduces MBA expressions by multiple known MBA rules. Syntia is a program synthesis framework for approximating the semantics of expressions. It uses a set of input-output samples from the expression, learns the semantics of the samples, and synthesizes a simpler expression that is equal to the original expression.


## 5.1.2. Benchmarks

To fully expose the capability of diverse methods on simplifying MBA expressions, a large scale of MBA expressions is required for evaluation. Therefore, we consider two comprehensive MBA benchmarks: Dataset 1 [14] and Dataset 2 [11]. Dataset 1 comprises 500 MBA samples generated by Tigress [6] with up to three variables. Dataset 2 collects 3,000 MBA equations with up to four variables, which contains 2,000 polynomial MBA (1,000 linear MBA) and 1,000 non-polynomial MBA expressions. Every sample in datasets is a 2-tuple: (Ec, Eg). Ec is the complex MBA expression, and Eg is the related equivalent simple form. Multiple samples in benchmarks are shown in Table 2.Table 2
MBA samples in the benchmarks.
EcEga∧∼a+2∗a|a+1a+a2∗∼x∧y+3∗∼x&y+3∗x&∼y−2∗∼x&yx+y∼x&y∗x|y+x&∼y∗∼x&y−1−x∗y


## 5.1.3. MBA Complexity Metrics

We use the following metrics to measure MBA complexity: number of DAG nodes and MBA alternation. For example, the expression∼x∧y+3∗x|y, whose DAG representation is shown in Figure 3, has 8 nodes and an MBA alternation (a red arrow means one MBA alternation) of 2. The larger a metric’s value, the more complex an MBA expression. We expect the metrics’ values will be reduced after simplification.(1)
Number of DAG Nodes. An MBA expression is transformed into a directed acyclic graph (DAG) representation in which the nodes are operators, variables, and constants. The number of nodes in the DAG is defined as a complexity metric for an MBA expression.(2)
MBA Alternation. The MBA complexity mainly comes from mixing bitwise operations and arithmetic operations. We adopt “MBA alternation” to measure the number of edges linking different types of operations in the DAG representation of an MBA expression.Figure 3
DAG representation of an MBA expression∼x&y+3∗x|y.


## 5.1.4. Machine Configuration

All of our experiments are performed on a server with Intel Core i9 3.00 GHz CPU, 64 GB DDR4 RAM, 2 TB SSD Hard Drive, and running Ubuntu 20.04 OS.


## 5.2. Simplification on Dataset 1

In the first experiment, we run MBA-Flatten and other peer tools on Dataset 1. The evaluation result in Table3 shows that only MBA-Flatten successfully produces verifiable simplification outputs for all MBA expressions with negligible overhead (within 0.1 seconds).Table 3
Simplification results using Dataset 1.
Tools✓✗TimeoutRatio (%)Average time (s)GraphMR137363027.40.01SSPAM332168066.41.45Syntia369131073.838.5MBA-Blast41608483.20.02MBA-Solver45404690.80.02MBA-Flatten50000100.00.02We first study thecorrectness that means an expression before and after simplification is semantically equivalent. Z3 solver [19] is adopted to check whether the output of a simplification tool is equivalent to the input. The solver may not return the solving result due to the MBA’s complexity, so we set 1 hour as a practical threshold for this and the following experiments.Table3 presents the number of MBA expressions that can be reduced by simplification tools. GraphMR is trained on the linear MBA dataset, so it can only simplify 137 of 500 MBA expressions. SSPAM outputs 168 wrong simplification results because of the limited number of MBA rules in the pattern library. Syntia uses stochastic program synthesis to generate a simple expression, which successfully synthesizes 369 simplification results. MBA-Blast performs well on simplifying 2-variable MBA expressions rather than three or more variables, and therefore, it generates 416 simplification results. MBA-Solver can successfully simplify the majority of the MBA expressions (454 of 500), but it cannot process several special cases, e.g., the non-polynomial MBA expression including sub-expression ∼x−1. In contrast to MBA-Solver, MBA-Flatten can successfully simplify all 500 MBA samples, and it reduces ∼x−1 to the expression −x.Next, we investigate theeffectiveness that reflects how much complexity is reduced by the simplification methods. Table 4 reports the expression complexity before and after simplification. Two quantitative metrics are used to measure expression complexity: the number of DAG nodes and MBA alternation. Table 4 shows that all simplification tools (except SSPAM) can considerably reduce the complexity measurement of the solved MBA expressions. SSPAM cannot effectively reduce a complex MBA expression to a simpler form due to the limited known MBA rules used in the software.Table 4
Complexity metrics of the results on correctly simplified samples in Dataset 1 before and after simplification.
ToolsAverage # of nodesAverage MBA alternationBeforeAfterA/B (%)BeforeAfterA/B (%)GraphMR9.73.637.13.60.25.6SSPAM6.24.064.52.41.562.5Syntia9.43.436.23.70.25.4MBA-Blast9.03.538.93.30.26.1MBA-Solver9.63.637.53.60.25.6MBA-Flatten9.83.737.83.70.25.4


## 5.3. Simplification on Dataset 2

As the second experiment, we run MBA-Flatten and other baseline tools on Dataset 2. As shown in Table5, MBA-Flatten can successfully simplify 2,943 of 3,000 MBA expressions, and its average processing time is less than 0.2 seconds.Table 5
Simplification results using Dataset 2.
Tools✓✗TimeoutRatio (%)Average time (s)GraphMR3792621012.60.01SSPAM705320197523.5143.1Syntia4372563014.638.9MBA-Blast17630123758.80.05MBA-Solver2899010196.70.10MBA-Flatten294305798.10.16Considering the MBA expression in Dataset 2 is more complex and diverse than the one in Dataset 1, this experiment exposes more detailed findings. GraphMR and Syntia have limited effect on simplifying complex MBA expression, which can only correctly simplify less than 450 MBA samples. SSPAM cannot generate a simpler expression, so nearly 2/3 (1,975 of 3,000) of the simplified results cannot be checked by the Z3 solver within the time threshold. Compared with MBA-Blast (1,763 simplified samples), MBA-Solver can reduce more MBA expressions with three or four variables, and it successfully simplifies 2,899 MBA samples. MBA-Flatten can reduce 2,943 MBA samples, but it fails to simplify several special cases. One exception is the non-polynomial MBA expression∼x−1∧y∗∼x−1|y+∼x−1∧∼y∗∼∼x−1∧y. Table 6 reports that all solutions (except SSPAM) can generate a simpler equivalent expression. Overall, MBA-Flatten presents its advanced capability by successfully simplifying 98.1% of MBA samples.Table 6
Complexity metrics of the results on correctly simplified samples in Dataset 2 before and after simplification.
ToolsAverage # of nodesAverage MBA alternationBeforeAfterA/B (%)BeforeAfterA/B (%)GraphMR32.16.921.56.80.913.2SSPAM35.330.486.17.56.586.7Syntia30.95.417.56.20.711.3MBA-Blast37.410.427.911.61.512.9MBA-Solver45.413.229.112.22.117.2MBA-Flatten45.311.224.712.31.512.2Furthermore, we compare the average solving time of simplification tools on the two benchmarks. From Tables3 and 5, the simplification time of GraphMR and Syntia is almost not increased, but SSPAM takes much more time when it simplifies a more complex MBA expression. MBA-Blast takes less than 0.1 seconds to simplify a two-variable MBA expression. Compared with MBA-Solver, MBA-Flatten takes slightly more time to simplify an MBA expression. The main reason is that MBA-Solver directly gets the bitwise expression simplification results from the transformation tables, rather than reduces it by multiple simplification procedures.


## 5.4. Case Study

The evaluation results in Tables3 and 5 show that MBA-Solver and MBA-Flatten are the most powerful MBA simplification tools. Throughout this case study, we demonstrate the strengths and weaknesses between MBA-Solver and MBA-Flatten.We manually check the MBA expressions solved by MBA-Solver or MBA-Flatten, and one interesting observation is that MBA-Flatten can reduce all polynomial MBA expressions in the datasets, as MBA-Solver does. Does this scenario mean that MBA-Solver and MBA-Flatten can be substituted for each other? The answer is relevant to the number of variables in an MBA expression: as described in Section2.2, MBA-Solver can successfully simplify a polynomial MBA expression with up to four variables; compared with MBA-Flatten, MBA-Solver is more efficient when it reduces an MBA expression. However, MBA-Flatten can simplify a polynomial MBA expression with an arbitrary number of variables, and the form of simplification result is shown in Equation (15). The following example shows how to apply MBA-Flatten to simplify Equation (6), which is an MBA expression with five variables.Example 8.
For Equation (6), we have(37)A=−∼x|y|t∧∼a=−a∧t∧x∧y−a∧t∧x−a∧t∧y+a∧t−a∧x∧y+a∧x+a∧y−a−t∧x∧y+t∧x+t∧y−t+x∧y−x−y−1,B=−∼xy∼t∧∼a=−−a∧t∧x∧y+a∧t∧x+a∧t∧y−a∧t+t∧x∧y−t∧x−t∧y+t,C=−∼x|y|z|t∧a=−a∧t∧x∧y∧z−a∧t∧x∧y−a∧t∧x∧z+a∧t∧x+a−a∧t∧y∧z+a∧t∧y+a∧t∧z−a∧t−a∧x∧y∧z+a∧x∧y+a∧x∧z−a∧x+a∧y∧z−a∧y−a∧z,,D=−∼x∧∼y∧z|t∧a=−−a∧t∧x∧y∧z+a∧t∧x∧y+a∧t∧x∧z−a∧t∧x+a∧t∧y∧z−a∧t∧y−a∧t∧z+a∧t+a∧x∧y∧z−a∧x∧z−a∧y∧z+a∧z,and thus,(38)fx,y,z,t,a=A+B+C+D−2∗y−1+x∧y=x−y.
The other observation is that MBA-Flatten can simplify all non-polynomial MBA expressions solved by MBA-Solver, but not vice versa. It is because that MBA-Solver treats the common sub-expression as an intermediate variable, rather than a sub-expression itself. Therefore, MBA-Flatten can simplify more special cases that cannot be simplified by MBA-Solver. Moreover, MBA-Flatten can reduce a non-polynomial MBA expression with five or more variables.
From the description above, MBA-Flatten is a general MBA simplification method.


## 5.5. MBA-Powered Malware Deobfuscation

MBA expression is always used to obfuscate code, so malware developer also adopts the MBA expression to complicate the program. Liu et al. [5] report that MBA expressions are used in a ransomware sample to protect the encryption key, and they also observe that MBA rules are integrated into the software obfuscator VMProtect, which is widely used by malware developers.In this experiment, we demonstrate that MBA-Flatten can assist in reverse-engineering the malware obfuscated by MBA expressions. We collect all MBA expressions used in malware from existing work [5]. Then, MBA-Flatten is applied to simplify the expressions, and the Z3 solver is used to check the correctness of the simplified result. The evaluation result shows that MBA-Flatten can successfully simplify all MBA expressions collected from existing malware samples. One simplification procedure is shown as follows, and MBA-Flatten produces the final result x−y.(39)∼∼x+y∧∼∼x+y=∼−x−1+y∧∼−x−1+yt1=−x−1+y=∼t1∧∼t1=−t1–1=x−y.Furthermore, we replace the MBA expressions used in malware with new MBA expressions involving five or more variables and produce 130 variants, such as the above expression∼∼x+y∧∼∼x+y, which is replaced with Equation (6). We apply MBA-Blast and MBA-Flatten to simplify the new MBA expressions. Unfortunately, MBA-Blast fails to simplify them. In contrast, MBA-Flatten can successfully simplify all new MBA expressions. Therefore, this experiment shows that MBA-Flatten can simplify the MBA expressions used in existing malware and the complex MBA expression with five or more variables.


## 5.6. Boosting SMT Solving MBA Equations

Satisfiability modulo theory (SMT) solvers have been widely applied in diverse software engineering areas, such as software analysis [21, 22], symbolic execution [23, 24], and test generation [25]. Existing work [10, 11] has presented that SMT solvers are hard to solve MBA equations. However, the MBA simplification method, MBA-Solver, can be used to boost the SMT solver’s performance on solving MBA equations (11).In this experiment, we report that MBA-Flatten (denoted as MF) can assist SMT solvers in solving MBA equations. We consider the benchmark from work [11] and test three popular SMT solvers: Boolector [26], STP [27], and Z3 [20]. The benchmark is actually considered as Dataset 2 in this study, and MBA-Solver (denoted as MS) is considered as the baseline. MBA-Flatten and MBA-Solver are used to simplify all MBA equations in the benchmark, and then, the simplification results are output to the three SMT solvers.The evaluation result is shown in Table7, and the solving time threshold is set as 1 hour. Before simplification, all three SMT solvers can only solve a small portion (Boolector 496 (16.5%), STP 98 (3.3%), Z3 84 (2.8%)) of the MBA equations within the time threshold, but after simplification, all three solvers can solve over 96% of MBA equations. Compared with MBA-Solver, all SMT solvers can solve more MBA equations after MBA-Flatten’s simplification. This is because MBA-Flatten can successfully simplify more MBA expressions than MBA-solver, as shown in Table 5. After MBA-Flatten’s simplification, all SMT solvers can solve 2,943 of 3,000 MBA equations, which means that the distinction between solvers’ performance on solving MBA expressions becomes insignificant. These results indicate that MBA-Flatten is a generic method to boost SMT solver’s performance on solving MBA expressions.Table 7
Experiment result of SMT solving on Dataset 2.
BoolectorSTPZ3BeforeMSMFBeforeMSMFBeforeMSMFPolynomial4682000200070200020005620002000Non-polynomial288999432889994328899943Total4962899294398289929438428992943


## 5.7. Performance

This section reports MBA-Flatten’s performance data. Table8 shows the time and memory cost when MBA-Flatten processes an MBA expression with different complexity measured by the number of nodes. For every complexity measurement, 100 different MBA expressions are generated to do the test. As some of the timings are small, we repeat every test 100 times. MBA-Flatten is effective because it only performs low-cost arithmetic computation. Our implementation adopts the Python SymPy library to efficiently perform the arithmetic reduction. Overall, MBA-Flatten is an effective tool for simplifying MBA expressions.Table 8
MBA-Flatten’s performance on MBA expressions with different complexity.
# of nodesTime (s)Memory (MB)100.020.2500.181.11000.534.31500.917.6


## 6. Discussion

MBA-Flatten has demonstrated the feasibility of automatically reducing MBA expressions. However, we also note some potential enhancements for future improvement.As introduced in Section5.3, MBA-Flatten cannot simplify the non-polynomial MBA expression ∼x−1∧y∗∼x−1|y+∼x−1∧∼y∗∼∼x−1∧y. We further investigate how to reduce it, and the simplification procedure is shown below. During the simplification procedure, the sub-expression ∼x−1 is treated as an intermediate variable rather than the expression x−1. However, it is hard for an automatic tool to precisely detect and identify the sub-expression, such as the sub-expression ∼x−1. To mitigate this problem, one possible solution is to integrate multiple heuristic rules into MBA-Flatten. Therefore, MBA-Flatten can explore diverse reduction directions to generate a simpler result.(40)∼x−1∧y∗∼x−1|y+∼x−1∧∼y∗∼∼x−1∧y=t1∧y∗t1|y+t1∧∼y∗∼t1∧yt1=∼x−1=t1∗y=∼x−1∗y=∼t2∗yt2=x−1=−t2−1∗y=−x∗y.It is possible that an adversary attacks MBA-Flatten by combining MBA obfuscation with other obfuscation techniques to generate an expression that does not satisfy the MBA definition in this study. Note that MBA-Flatten is designed for simplifying MBA expressions, so it may correctly handle the certain MBA sub-expression, but cannot solve the remaining non-MBA part. It is interesting to further investigate whether MBA-Flatten can interact with other analysis techniques (e.g., symbolic execution) to produce a better result.


## 7. Conclusion

Existing work performs well on simplifying MBA expression with very few variables. However, the state-of-the-art methods are hard to simplify a multivariable MBA expression. We investigate it and address this challenge using an in-place simplification method. A transformation procedure is proposed to transform a bitwise expression into a unified form, and we provide a mathematical proof to guarantee the correctness of this transformation. Then, the arithmetic reduction is used to further simplify the expression and produce a simplified result. Our large-scale experiments show that MBA-Flatten is a general and effective MBA simplification method. Furthermore, developing MBA-Flatten not only advances automated malware analysis but also boosts SMT solving on the MBA equations.



---

*Source: 7307139-2022-09-14.xml*