< BACK / JavaScript

Better Mixed Boolean Arithmetic in JavaScript

Ciarán - antibot / obfuscation / JavaScript / Mixed-Boolean-Arithmetic

Mixed boolean arithmetic (MBA) is great for obfuscation. It’s hard to read, obscures algorithms very well, and for years it really had no good solution.

In recent years, tooling such as CoBRA building on the long-established Z3 Theorem Prover have helped mitigate this challenge greatly.

In JavaScript, one of the hard parts is mapping your expression to a tool like CoBRA before you can simplify the expression and understand the algorithm its obfuscating.

Sadly, in the world of JavaScript obfuscation this hasn’t been done that well. Any obfuscators & antibots that choose to incorporate MBA do so sparingly and in a way which is trivially undone.

JavaScript MBA is powerful

I’m going to make an argument for why MBA is incredibly interesting (and arguably better) in the world of JavaScript obfuscation despite having barely been touched.

All MBA I have seen in-the-wild mirrors the patterns used in binary-obfuscation. However, JavaScript is weird. We can use this weirdness to great effect.

Numbers in JavaScript are floats until they’re not

Internally the number datatype in JavaScript is actually a float64. This is the IEEE 754 double-precision format. In this, it packs a number into 64 bits split across 3 fields: Source: Wikipedias Double-precision floating-point format article

  • The first bit is allocated to the sign. This is used to represent if the number is positive or negative.
  • The next 11 bits are the exponent bits (scale: a power of 2): 1026 = 1023 + 3 - multiply by 2^3 (the 1023 is the fixed “bias”).
  • The final bits are the precision bits. This is known as the Mantissa, this contains the significant digits.

You may already be well versed with this. It’s a frequently asked question: “Why cant computers get floating point arithmetic right?” and the internal structure of the float64 representation is widely understood.

One interesting thing you may not know though. When you do any bitwise operation (excluding >>>) on a float64 in JavaScript, internally gets recast into int32.

That means that if we do:

const x = 2;
const y = 5;
console.log(x ^ y);

The JavaScript runtime is defining the x and y values as float64 and then re-casting them as int32 before it XORs them both, the result is then returned back as a float64.

How can this be abused?

MBA solvers (and humans) make the reasonable assumption that the program they are analysing will only contain numbers which are going to have a static bitwidth.

However, as JavaScript has this implicit coercion, we can generate expressions which have fluctuating bitwidths “invisibly”. This means we can create expressions which when passed to a solver like CoBRA will produce totally incorrect simplifications compared to their true value in the JavaScript runtime.

2^53: The Max Safe Integer

A float64 can store every integer up to 2^53 (Number.MAX_SAFE_INTEGER is 2^53 - 1). Past that the mantissa runs out of bits, so the representable integers start to spread apart: between 2^53 and 2^54 only even numbers exist, between 2^62 and 2^63 the gap between neighbours (the ULP) is 1024, and so on. If you add a small number to a large one up there and the result just rounds to the nearest representable value, and the low bits drop off the end.

A solver like CoBRA (reasonably) doesnt model this. It reasons integers are fixed-width; modulo 2^n, where (M + a) - M is always going to be a, no matter how big M is. As a result we can abuse this.

Variants

Here are 2 simple variants I have constructed:

  1. Runtime evaluates to x & 255, CoBRA simplifies to y & 255:
(x & 0xff) + ((0x9E3779B1 * 0x85EBCA77 + (y & 0xff)) - 0x9E3779B1 * 0x85EBCA77) - ((0x9E3779B1 * 0x85EBCA77 + (x & 0xff)) - 0x9E3779B1 * 0x85EBCA77)
  1. Runtime evaluates to x & 255, CoBRA simplifies to 0
(x & 0xff) - ((0x9E3779B1 * 0x85EBCA77 + (x & 0xff)) - 0x9E3779B1 * 0x85EBCA77)

Lets explore #1.

A “ghost” term

const g = (M, a) => (M + a) - M;

To CoBRA and to anyone reading it as plain integer math g(M, a) is just a; the Ms cancel. But if M is far enough past 2^53, the addition M + a rounds straight back to M, and JavaScript hands you back 0, for example:

const M = 6e18;
g(M, 123);

This would result in 0 in JavaScript. So g is a ghost 👻: it equals a in every model a solver knows about, and 0 at runtime. We now have a term we can make appear or disappear depending on who’s looking at it.

Hiding the constants

const M = 0x9E3779B1 * 0x85EBCA77;

0x9E3779B1 is xxHash’s PRIME32_1 and 0x85EBCA77 is xxHashes PRIME32_2.

I picked these as there are many applications where these values could be re-used to add to confusion while contributing to your MBA.

Their product is 5964046043053701959. JavaScript numbers can’t represent this, evaluating to 5964046043053702000.

The deception

We want an expression that is x & 0xff at runtime but y & 0xff to the solver. Use one ghost to smuggle in y and another to delete x:

function f(x, y) {
  const M = 0x9E3779B1 * 0x85EBCA77;   // ~2^62.4
  return (x & 0xff) + 
        ((M + (y & 0xff)) - M) - // a = (y & 0xff)
        ((M + (x & 0xff)) - M); // a = (x & 0xff)
}
  • In V8: every (M + a) - M rounds away to 0, so f returns (x & 0xff) + 0 - 0 = x & 0xff.
  • To a solver: every (M + a) - M is a, so f returns (x & 0xff) + (y & 0xff) - (x & 0xff) = y & 0xff.

Hand the expression to CoBRA:

$ cobra-cli --mba "(x & 0xff) + ((0x9E3779B1 * 0x85EBCA77 + (y & 0xff)) - 0x9E3779B1 * 0x85EBCA77) - ((0x9E3779B1 * 0x85EBCA77 + (x & 0xff)) - 0x9E3779B1 * 0x85EBCA77)" --verbose
Variables: x, y
Classification: kSemilinear
  Flags: bitwise, arithmetic, arith-over-bitwise
Evaluating signature vector...
Signature vector (2 vars): [0, 0, 1, 1]
Simplifying...
Running spot-check... passed
Verifying full-width equivalence... passed
y & 255

It returns that the masked byte comes from y. We know at runtime it comes from x. f really is y & 255 as a fixed-width integer expression, and its check confirms that. The answer is right for it’s own integer model, there’s correctly no float64 anywhere in that pipeline, so nothing in it can see that V8 does the + and * in float64 and never reaches y.

Tell the solver it’s bitwidth?

This doesnt help. (M + a) - M is a in every modular ring 2^n, so the solver prints y & 255 at anything. Our runtime’s x & 255 isn’t reachable at any width, because V8 isn’t doing modular arithmetic. A JavaScript expression doesn’t have a bitwidth: arithmetic runs ~53-bit-exact-then-floats, bitwise ops are exactly 32, and they alternate. Any single modulus a solver commits to, it’s wrong in one of the two phases.

An int32 past 2^53 comes back one of three ways:

  • exact: float64 didn’t round, so there’s no divergence to exploit.
  • corrupted: it rounded, so it’s now wrong for some input and your function is broken.
  • destroyed: it was below the local ULP, so it rounded to 0 (we use this in our “ghost” case).

Do a float64-aware pass first?

With our specific example the divergence we used is only (M + a) - M. Any deobfuscator that recognises the shape a constant M whose ULP/2 exceeds the range of a and rewrites it to 0 strips the ghost in a few lines. However, this doesnt need to be the only representation, that’s part of what MBA is.

Practical attacks

The attacker must be first aware this is even possible. When adversarially testing using Claude Opus 4.8, given a hardened implementation of a loop-unrolled RC4 PRGA implementation with the KSA array constants embedded, generated at request-time. The agent took a combined 3 hours (with slight redirection) to correctly dump the KSA array over 10/10 requests using Python. It’s interesting to observe how unqiue techniques slow-down LLMs when tasked with less-common reverse engineering goals.

1. Z3 with proper mapping

If youre willing to take a on average a ~2126.8% slowdown compared to CoBRA, Z3 has full IEEE-754 theory and can model this if you encode float + ToInt32 at the bitwise boundary.

2. Building a state machine

Another approach could be building a state-machine which at runtime resolves the data/algorithm obfuscated via this technique. Features such as SWC’s JsNumber could make this a bit easier.

3. Sandboxing

Easiest approach attack-wise, but also the worst, if a defender cannot prevent someone determined enough to solve their challenge (which you never can), this is really what they want to force an attacker to do. If an antibot can “encourage” this, attack volume has been mitigated significatnly.

Other interesting notes

Z3 can be “attacked” without any float64 tricks

Z3 is incredibly expensive on dense linear MBA. It cannot prove equivalence for either of the following cases in 5 minutes at 64-bit. CoBRA would give the answer in ~10ms:

  • 11*~(x&~y) - 9*~(x|y) + 2*(x&~y) which is just 9*y - 2
  • -8*~y*(x&y) - 8*~y*(x&~y) + 10*~y*x + 3*~y*~(x|y) + 8*(x^y)*(x&y) + 8*(x^y)*(x&~y) - 10*(x^y)*x - 3*(x^y)*~(x|y) - 3*~y*(x|~y) - 1*~y*~x + 3*(x^y)*(x|~y) + 1*(x^y)*~x which is ~y - (x^y)

Create difficult static expressions

In the case where its necessary for an attacker to have opaque predicates resolved at runtime. This technique could likely be used to break dead code elimination (DCE) by both; improperly having important functionality removed, and/or making DCE exceptionally difficult. It could also be speculated that this could effectively be used to flood the context window of LLM-assisted reverse engineering attempts.

Smuggling coefficients through the float64 multiply

You can achieve a similar goal by smuggling a coefficient:

((F1*F2|0)+OFF) * basis

This will “fool” CoBRA in the exact same way but the divergence is a constant subexpression, so a float64 const-folder evaluates it away. This could be hardened by better-deriving these subexpressions.

JavaScript’s coercion is highly effective

Take for example the expression: a | b = (a ^ b) + (a & b)
XOR holds the differing bits, AND holds the common bits, and they’re bit-disjoint so + reconstructs OR.

You could just gate the carry term with x: (a ^ b) + x * (a & b)

  • x = 0: (a ^ b) + 0 = XOR
  • x = 1: (a ^ b) + (a & b) = OR (the + is exact because the two terms touch disjoint bits) Virtually all datatypes in JavaScript are coercible, it’s ugly and beautiful. So undefined when used in an expression such as this, can be used to gate an expression. Empty array accesses can be used to represent undefined. This can create some cool logic:
const G = []; // Each expression is identical but produces divergent results:
console.log((()=>(G[0]^G[1])+(G[3]|(G[3]=1,0))*(G[0]&G[1]))(G[0]=0x78,G[1]=0xff).toString(16));  // "87"  - XOR
console.log((()=>(G[0]^G[1])+(G[3]|(G[3]=1,0))*(G[0]&G[1]))(G[0]=0x78,G[1]=0xff).toString(16));  // "ff"  - OR
Read More