SSLEM: A Simplifier for MBA Expressions based on Semi-linear MBA Expressions and Program Synthesis

MBA (Mixed Boolean and Arithmetic) expressions are the expressions mixed with arithemethic operators like ‘$+$’, ‘$-$’ and $\times$’, and boolean operators like ‘$\&$’, ‘$|$’ and ‘$\wedge$’. Program rewriting to insert MBA expressions is a popular way of program obfuscation because such expressions are difficult to analyze with popular solvers like Z3 and Mathematica.

While MBA obfuscation is a helpful method for software protection, it is also used for malware obfuscation. Once malware is obfuscated with the MBA-obfuscation option, it entails a herculean effort of analysts to understand its behavior. Thus there have been various simplification efforts to handle this problem.

The methods used by existing works to simplify MBA expressions are classified into two kinds; First, logic-based simplifiers have been devised to simplify MBA expressions. Based on theoretical foundation [1][2], this logic-based approach suffers from the scalability problem [3]. Thus most of the previous works narrowed the problem scope. For instance, typically logic-based simplifiers have been dedicated to a specific form of MBA expressions like linear MBA expressions to make the problem tractable, systematic and fast [2]. However, it does not seem appropriate for obfuscated malware, because trivial MBA expressions shown in obfuscated malware like $x\times y$, $x\ \&\ (x+y)$ and $x\ \&\ 0x1$ are not linear expressions.

Second, synthesis-based MBA expression simplication [4][5][6] has been recently introduced. This approach searches a simpler expression of the original program, if any, by program synthesis. It is applicable to general complicated forms of MBA expressions, besides specific forms of expressions. However, the solution is imcomplete and relatively slow [6].

In this poster, we proposed a method and tool to develop an enhanced simplifier of MBA expressions to help deobfuscate MBA-obfuscated malware, taking advantage of program synthesis as well as logic-based solutions.

Previous works recognized nested categories of MBA expressions. “Linear MBA expressions” is a summation of terms, where a summation means an arithmetic operation with $+$, a term is a multiplication of a coefficient $a_{i}$ and a pure boolean expression $e_{i}(x_{1},\dots x_{T})$, $T$ is the number of variables and $N$ is the number of terms, as depicted in the following fomula [1][2][3];

Examples of linear expressions include $10\times(x\ \&\ y)$, $5\times(x\ |\ y)+6\times(x\ \&\ y)$, $3\times(x\ \&\ y)-20\times(x\ |\ y)-1$ and $y+376\times(x\ \&\ -1)$.

As mentioned earlier, most traditional simplification of MBA expressions dedicated to linear MBA expressions. Depending on pattern matching and rule rewritting, they are not feasible for complicated non-linear expressions due to the lack of the scalability.

It is proved a valuable proposition that a simplified form of any of the linear MBA expressions with 1-bit variables also represents a simplified form of the one with the n-bit variables, and vice versa [2][1]. This means that if we simplify any linear MBA expression with 1-bit variables, the simplification result can be also considered as a simplification of the corresonding, same looking expression with n-bit variables [2]. This makes the simplification process much more efficient.

For some insight, let us consider an expression a function which maps a combination of input variables to the output. Regardless representation of an expression whether it is complicated or simple, the number of unique mappings will be limited by the size and the number of the input and output variables. For instance, if we use two 1-bit variables $x$ and $y$ as inputs, the possible combination of $x$ and $y$ will be 00, 01, 10 and 11. The simplification of a given linear MBA expression would be a searching problem. Among all the possible output-bit-combinations for each input-bit-combination, a simplifier should find a simpler expression corresponding to the given expression. The property proven by the previous works dramatically reduced the searching space from $2^{2^{2^{16}}}$ (that is, $16^{16}=1.84e+19$) to $2^{2^{2^{1}}}$ (that is, $8$) .

Note that the proposition proved by previous methods only for linear MBA expressions. However, solution dedicated to linear MBA expressions cannot handle a lot of general MBA expressions-only $2^{2^{2^{1}}}$ expressions can be handled. Thus, they adopted heuristics to spot any linear subexpressions in a given complicated expression. Otherwise $2^{2^{2^{1}6}}-2^{2^{2^{1}}}$ MBA expressions cannot be handled, some of which might appear in obfuscated malware.

In this section, we introduce SSLEM, a new MBA expression simplification solution To overcome limitations of existing works, SSLEM makes use of both kinds of existing tools (the logic-based simplifier and the program synthesis-based simplifier), we envision that the proposed mehod will enhance performance some corner cases.

As mentioned earlier, a logic-based simplifier is fast and effiecient but simplifying only limited category of expressions (linear MBA expressions). Aiming to overcome this problem, the proposed SSLEM proposes to preprocess the general MBA expressions to linear MBA expressions, and input the result to a logic-based simplifier. However, transformation to linear expressions would fail in most cases, because linear MBA expressions are only a small subset of the whole MBA expressions, as we compared the number of unique semantics in the previous section.

Thus, SSLEM uses an intermediate form of MBA expressions called “semi-linear” MBA expressions, and transforms a general MBA expressions to a semi-linear MBA expression, first, by the program synthesis-based simplifier. Then the resulting semi-linear MBA expression is transformed into a combined expression which is made of several linear expressions. Since each of the resulting linear MBA expressions can be simplified by the logic-based simplifier, we can finally earn simplification of a non-linear expression with a logic-based simplier.

Overall process of the proposed SSLEM is composed of three steps, as depicted in Fig. 1:

1. 1.

   PLASynth-SL finds preliminary candidates for the logic-based simplifier working at Step III. It is a search-based synthesizer to find a semi-linear MBA expression corresponding to a general non-linear MBA expressions, keeping the semantics the same.

2. 2.

   LEM transforms a semi-linear MBA expression to a combination of linear MBA expressions

3. 3.

   The linear subexpressions of the semi-linear MBA expression resulting from LEM, are in turns fed to the logic-based simplifier. This step might leverage an existing powerful linear MBA expression simplifier like MBA Blast [2]

We propose a novel MBA simplifier, called “SSLEM,” based on a new concept of “semi-linear” MBA expression transformation, as well as existing logic based simplifiers that restrict their target into linear MBA expressions. We assume that more semi-linear MBA expressions exist in real-world obfuscated malware, than linear MBA expressions do. The shorter contiguous sequences of the same bits in a -bit-valued constant complicates the result. For instance, 0101 0101 0101 01 0101 will require 16 separated linear expressions and 15 shifts in the simplification result, which might not be simpler than the original expression. However, our method will be effective with the small number of changes in the bits of constants like 0x01 and 0xFE. By taking the advantages of program synthesis and logically proved solutions, we envision that SSELM will show better performance. Since some expressions are likely to be simplified by program synthesis, while some others are simplified by logic-based rewriting methods, we expect that SSLEM would be able to handle the corner cases that the existing solutions could not hanldle.