This part was originally an appendix to Part 1. We will treat MBA very formally and prove the "Fundamental Theorem". I don't recommend reading this part, unless you

• want to see the proof
• are trying to implement this and are confused about details (though you could just read my implementation)

It is totally expected for you to not understand all the details from Part 1 and I didn't even show the details as they require formality (in my opinion). If all you took away from last part is that we can find a linear combination of bitwise functions, that equal some given bitwise function, exponentially faster than with general functions, then I did my job and you can skip this part.

In my opinion, this is one of those times where being formal really pays off and helps organize everything. It also allows us to clarify some things that confused me when I first learned about MBA, which I will talk about at the end.

Definitions

Let ${\mathbb{Z}}_2=\{0,1\}$ be the ring of integers mod 2. Let $w\in \mathbb{N}$ be the integer width, i.e. the number of bits in an integer. Let ${\mathbb{Z}}_{2^w}=\{0,\dots ,2^w-1\}$ be the ring of integers mod $2^w$, i.e. the $w$-bit integers. To be completely formally correct, we will define the function $$\begin{array}{rl}\beta :{\mathbb{Z}}_2& \to {\mathbb{Z}}_{2^w}\\ 0& \mapsto 0\\ 1& \mapsto 1\end{array}$$ which basically lets us interpret an element of ${\mathbb{Z}}_2$ as an element of ${\mathbb{Z}}_{2^w}$. This helps to avoid some confusion, e.g. $\beta (-1)\ne -\beta (1)$ (for $w>1$).

Let ${\mathbb{Z}}_2^w={\mathbb{Z}}_2\times \cdots \times {\mathbb{Z}}_2$ be the ring of ${\mathbb{Z}}_2$-sequences of length $w$, i.e. vectors/lists of $w$ bits. Note that although ${\mathbb{Z}}_{2^w}$ and ${\mathbb{Z}}_2^w$ have the same number of elements, they are not isomorphic (for $w>1$), since their additive groups (and multiplicative monoids) are not isomorphic. Addition in ${\mathbb{Z}}_{2^w}$ is just integer addition mod $2^w$, whereas in ${\mathbb{Z}}_2^w$ addition is the XOR operation. (Multiplication in ${\mathbb{Z}}_2^w$ is the logical AND). However, we can define the obvious bijection between them: $$\begin{array}{rl}\phi :{\mathbb{Z}}_2^w& \to {\mathbb{Z}}_{2^w}\\ (b_w,\dots ,b_1)& \mapsto \sum _{i=1}^w\beta (b_i)2^{i-1}\end{array}$$ This is just interpreting the sequence of bits as the binary representation of an integer, e.g. for $w=4$, $\phi (0,0,1,1)=3$ or ${\phi }^{-1}(6)=(0,1,1,0)$. It is not a ring homomorphism.

Extending Boolean Functions to the Integers

$\phi$ allows us to extend an $n$-ary function $f:{\mathbb{Z}}_2^n\to {\mathbb{Z}}_2$ to a function $f_{\ast }:{\mathbb{Z}}_{2^w}^n\to {\mathbb{Z}}_{2^w}$. The notation is slightly confusing here (though it is completely consistent). A function ${\mathbb{Z}}_2^n\to {\mathbb{Z}}_2$ should be thought of as taking $n$ inputs in ${\mathbb{Z}}_2$ and mapping them to a value in ${\mathbb{Z}}_2$, instead of a function taking a single sequence of $n$ bits, although both views are of course equivalent. The idea of this extension is that the function will be separately applied to each bit. These are the bitwise functions that were informally introduced in the post. For example the logical and $\wedge$ is a binary (2-ary, i.e. it takes two inputs) function on bits (i.e. elements of ${\mathbb{Z}}_2$). E.g. $1\wedge 0=0$. We want to extend this to a function on $w$-bit integers, e.g. $3{\wedge }_{\ast }2=2$. The extension will be in two steps.

The extension to ${\mathbb{Z}}_2^w$ is defined as $$\begin{array}{rl}{f}^{\prime }:({\mathbb{Z}}_2^w{)}^n& \to {\mathbb{Z}}_2^w\\ (b_{1,w},\dots ,b_{1,1}),\dots ,(b_{n,w},\dots ,b_{n,1})& \mapsto (f(b_{1,w},\dots ,b_{n,w}),\dots ,f(b_{1,1},\dots ,b_{n,1}))\end{array}$$ This definition looks more confusing than it actually is. It just means we apply $f$ to the first bit of each input and the result will be the first bit of the output and so on. The extension to ${\mathbb{Z}}_{2^w}$ is then defined as $$\begin{array}{rl}{f}_{\ast }:({\mathbb{Z}}_{2^w}{)}^n& \to {\mathbb{Z}}_{2^w}\\ x_1,\dots ,x_n& \mapsto \phi (f^{\prime }({\phi }^{-1}(x_1),\dots ,{\phi }^{-1}(x_n)))\end{array}$$ Again, this simply means converting each integer into its binary representation, applying $f^{\prime }$ to the sequence, which means applying $f$ to each bit, and converting the resulting sequence to an integer again. Using our $\wedge$ example on 2-bit integers: $$3{\wedge }_{\ast }2=\phi ((1,1){\wedge }^{\prime }(1,0))=\phi (1\wedge 1,1\wedge 0)=\phi (1,0)=2$$ We can now formally define the meaning of bitwise functions. A function $g:{\mathbb{Z}}_{2^w}^n\to {\mathbb{Z}}_{2^w}$ is called a bitwise function, if there exists an $f:{\mathbb{Z}}_2^n\to {\mathbb{Z}}_2$ such that $g=f_{\ast }$.

More importantly, we are now ready to formally define linear MBA functions.

It is time for the most important theorem.

Proof of the "Fundamental Theorem"

To give a concrete example of how this is useful. Suppose we are given two linear MBA functions $f,g:{\mathbb{Z}}_{2^{32}}\times {\mathbb{Z}}_{2^{32}}\to {\mathbb{Z}}_{2^{32}}$. We only have to check the following equalities to conclude they are equal everywhere: $f(0,0)=g(0,0)$, $f(0,-1)=g(0,-1)$, $f(-1,0)=g(-1,0)$, $f(-1,-1)=g(-1,-1)$. A priori, we have to compare the values for all $2^{64}$ inputs. This is what allows us to reduce the size of the linear system when generating linear MBA expressions.

Proof: Note that 0 and -1 are the numbers that only have 0 or 1 in their binary representation. Thus an input $\mathbf{x}\in \{0,-1{\}}^n$ has the form that $x_i=\phi (b_i,b_i,\dots ,b_i)$, i.e. each input number $x_i$ consists only of the same bit $b_i$. We will define $b^w=\phi (b,\dots ,b)=-\beta (b)$ to be the $w$-bit integer whose binary representation is just $b$s. The notation is sort of overloaded because $b^w$ could also be interpreted as $b\cdot \dots \cdot b$, but we will need it just for this proof and we will never use the other interpretation.

$$\begin{array}{rl}g(b_1^w,\dots ,b_n^w)& =\sum _{i=1}^m{c}_i{f}_{i\ast }(b_1^w,\dots ,b_n^w)\\ & =\sum _{i=1}^m{c}_i\phi (f_i^{\prime }((b_1,\dots ,b_1),\dots ,(b_n,\dots ,b_n)))\\ & =\sum _{i=1}^m{c}_i\phi ((f_i(b_1,\dots ,b_n)),\dots ,(f_i(b_1,\dots ,b_n)))\\ & =\sum _{i=1}^m{c}_i\sum _{j=1}^w{2}^{j-1}\beta (f_i(b_1,\dots ,b_n))\\ & =\sum _{i=1}^m{c}_i\beta (f_i(b_1,\dots ,b_n))\sum _{j=1}^w{2}^{j-1}\\ & =\sum _{i=1}^m{c}_i\beta (f_i(b_1,\dots ,b_n))(-1)\\ & =-\sum _{i=1}^m{c}_i\beta (f_i(b_1,\dots ,b_n))\end{array}$$ So for inputs of that form, the result is just minus one times the sum of those $c_i$ where $f_i(b_1,\dots ,b_n)=1$. We will need this result in a second.

We will now consider an arbitrary input, i.e. $\phi (x_i)=(b_{i,1},\dots ,b_{i,w})$. $$\begin{array}{rl}g(x_1,\dots ,x_n)& =\sum _{i=1}^m{c}_i{f}_{i\ast }(x_1,\dots ,x_n)\\ & =\sum _{i=1}^m{c}_i\phi (f_i^{\prime }((b_{1,w},\dots ,b_{1,1}),\dots ,(b_{n,w},\dots ,b_{n,1})))\\ & =\sum _{i=1}^m{c}_i\phi ((f_i(b_{1,w},\dots ,b_{n,w})),\dots ,(f_i(b_{1,1},\dots ,b_{n,1})))\\ & =\sum _{i=1}^m{c}_i\sum _{j=1}^w{2}^{j-1}\beta (f_i(b_{1,j},\dots ,b_{n,j}))\\ & =\sum _{j=1}^w{2}^{j-1}\sum _{i=1}^m{c}_i\beta (f_i(b_{1,j},\dots ,b_{n,j}))\\ & =-\sum _{j=1}^w{2}^{j-1}g(b_{1,j}^w,\dots ,b_{n,j}^w)\end{array}$$

The last equality is the previous result. This means that the value of $g$ on any input depends only on the value of $g$ at inputs of the form discussed before.

In the original paper on MBA, the set $\{0,1{\}}^n$ was used. (Kinda, we will discuss this in a bit). Let us quickly prove that the values of the function on this set also uniquely determine the function. This idea is the same, the algebra only slightly more annoying. The inputs now have the form $x_i=\phi (0,\dots ,0,b_i)=\beta (b_i)$. The last equality stems from the fact that we view ${\mathbb{Z}}_2$ as a subset of ${\mathbb{Z}}_{2^w}$.

$$\begin{array}{rl}g(\beta (b_1),\dots ,\beta (b_n))& =\sum _{i=1}^m{c}_i{f}_{i\ast }(\beta (b_1),\dots ,\beta (b_n))\\ & =\sum _{i=1}^m{c}_i\phi (f_i^{\prime }((0,\dots ,b_1),\dots ,(0,\dots ,b_n)))\\ & =\sum _{i=1}^m{c}_i\phi ((f_i(0,\dots ,0)),\dots ,f_i(b_1,\dots ,b_n))\\ & =\sum _{i=1}^m{c}_i\left(f_i(b_1,\dots ,b_n)+\sum _{j=2}^w{2}^{j-1}{f}_i(0,\dots ,0)\right)\\ & =\sum _{i=1}^m{c}_i\left(f_i(b_1,\dots ,b_n)+f_i(0,\dots ,0)\sum _{j=2}^w{2}^{j-1}\right)\\ & =\sum _{i=1}^m{c}_i\left(f_i(b_1,\dots ,b_n)-2f_i(0,\dots ,0)\right)\\ & =-2\sum _{i=1}^m{c}_i{f}_i(0,\dots ,0)+\sum _{i=1}^m{c}_i{f}_i(b_1,\dots ,b_n)\\ & =2g(0,\dots ,0)+\sum _{i=1}^m{c}_i{f}_i(b_1,\dots ,b_n)\end{array}$$ Overall, we have $$\sum _{i=1}^m{c}_i{f}_i(b_1,\dots ,b_n)=g(b_1,\dots ,b_n)-2g(0,\dots ,0)$$

Now we will consider general inputs again, i.e. $x_i=\phi (b_{i,1},\dots ,b_{i,w})$. As we saw before $$\begin{array}{rl}g(x_1,\dots ,x_n)& =\sum _{j=1}^w{2}^{j-1}\sum _{i=1}^m{c}_i{f}_i(b_{1,j},\dots ,b_{n,j})\\ & =\sum _{j=1}^w{2}^{j-1}(g(b_{1,j},\dots ,b_{n,j})-2g(0,\dots ,0))\\ & =2g(0,\dots ,0)+\sum _{j=1}^w{2}^{j-1}g(b_{1,j},\dots ,b_{n,j})\end{array}$$ So again, $g$ at any input only depends on the values of $g$ with 0, 1 inputs.

Things that confused me

We now have the language to clarify some things that were confusing to me when I first started learning about MBA.

The linear system

The first thing is how to construct the matrix/table, because a lot of papers do it differently. There are basically three different ways, which we will compare with an example. Let's rewrite x + y using !x, !y, x & y and !(x | y) on 2-bit numbers.

The way I view the table is as a restriction of the full table, which just lists the values of all expressions for all inputs. Even for 2-bit numbers it has 16 rows (for 32-bit numbers it would have $2^{64}$ rows), so I have omitted some rows, but here is what it would look like.

These tables work for any functions, i.e. also x * y, because all inputs are present. (That is, if we find a linear combination of some columns that equals another column, then we made sure that the linear combination always equals the target for all inputs). It is not easy to see from this table, but I can tell you that x + y == !x + !y + 2 * (x & y) - 2 * !(x | y).

But if we restrict the operations to be bitwise expressions, then the fundamental theorem tells us that we only need to consider the inputs 0/-1 (or 0/1), because equality everywhere is guaranteed.

Restricting the table two the inputs 0/1, we get this:

To me this is a bit ugly, because e.g. $\neg 1=-2$, so if we had 8-bit numbers it would be 254. But this is (of course) correct and ultimately does not matter. In the example from Part 1, I intentionally chose rewrite operations without negation so we would not run into this.

I prefer and implement the method using the inputs 0/-1. The reason this is more beautiful is that all the bits have the same value. To illustrate, let me write 3 = -1 in the table.

We will call this the uniform table. This is not the version you will see in most papers (including the original one). They evaluate all the bitwise expression as if they were 1 bit or boolean expressions.

We will call this the truth table. This looks very cool, but it is not immediately clear why this should work. It is not like the other two, in that we don't just restrict the full table and prove that the restricted table is enough. The reason this truth table works is simple if you look at the uniform table. It is just the negated table, so we are essentially solving $-\mathbf{Ax}=-\mathbf{b}$, which, of course, has the same solutions. So while the table looks the best, it is conceptually a bit less clear (in my opinion) and the implementation perhaps not as nice.

The Number 1

We already encountered this problem when obfuscating constants in Part 1. Let's not be unnecessarily general and restrict ourselves to two variables. We will call the constant 1 function (on 1 bit) $1$: $$\begin{array}{rl}1:{\mathbb{Z}}_2\times {\mathbb{Z}}_2& \to {\mathbb{Z}}_2\\ x_1,x_2& \mapsto 1\end{array}$$ Extending this function to the $w$-bit integers ${\mathbb{Z}}_{2^w}$, we just apply the function at each bit, so the result will be a 1 in each bit which is the constant $-1=\phi (1,\dots ,1)$ (or $2^w-1$): $$\begin{array}{rl}{1}_{\ast }:{\mathbb{Z}}_{2^w}\times {\mathbb{Z}}_{2^w}& \to {\mathbb{Z}}_{2^w}\\ x_1,x_2& \mapsto -1\end{array}$$ If we write $-1$ for the constant function that returns -1, then we get $1_{\ast }=-1$, which is ultimately the root of all confusion and sign errors.

So suppose we want to obfuscate the constant 1 with the rewrite operations x ^ y and !(x ^ y). We will use the truth table because it looks the cutest.

And we read off the solution (x ^ y) + !(x ^ y) == 1, right? This actually isn't correct, can you see why? We actually have (x ^ y) + !(x ^ y) == -1. The problem is that we found a linear combination such that $$(x{\oplus }_{\ast }y)+\neg (x{\oplus }_{\ast }y)=1_{\ast }=-1$$

To avoid confusion, the function $1_{\ast }$ should be called something else. In my implementation, I called it Ones to suggest that there is a 1 in each bit, but you could also call it -1, because it returns the constant -1 for any integer width. Then the table would look the same except for the name of the function and produce the correct linear combination (for -1). (The table before also produced the correct linear combination, but we made the mistake when reading off the solution.)

Should we want to obfuscate any constant $c$, we just multiply $1_{\ast }=-1$ by $-c$, e.g. for $c=42$

In my opinion this looks much more natural in the uniform table:

I am repeating myself, but in this table all the columns contain values of the expressions that would actually be computed during execution. Since we want the result to be 42, the last column has to be 42.