CVE-2025-4919: Corruption via Math Space in Mozilla Firefox

The Ion JIT compiler uses a function called ExtractLinearSum at multiple places to convert a value node into a linear sum expression. The purpose is to be able to reason about subexpressions containing exclusively additions and subtractions. For example, consider the graph of value nodes representing an expression like (x+(2+3)) − (−3). This will always be equal to x+8 which is much easier to reason about in contexts like bounds-check elimination or hoisting. ExtractLinearSum function extracts this simplified form. To understand the details of this function let’s consider its declaration in jit/IonAnalysis.h:

The return type would be struct SimpleLinearSum which is also declared in IonAnalysis.h:

As the comment explains only very simple linear expressions like 𝑥 + 𝑛 with 𝑥 as an arbitrary value node and 𝑛 as an integer constant are supported. A pure constant can also be expressed by setting the term pointer to a NULL pointer. It is important to note that any (integer) expression val can be converted to a SimpleLinearSum. In a trivial case that the expression is not itself an addition or subtraction ExtractLinearSum can simply return a SimpleLinearSum with term set to val and constant set to 0.

The ExtractLinearSum function takes three arguments. The first is simply the expression ins to analyze which should be a value node of integer type. The third is a simple recursion counter (as ExtractLinearSum function can call itself recursively to analyze i.e. the two sides of an addition seperately) which simply keeps track of the recursion depth to prevent stack exhaustion. This parameter will always be left at its default value 0 by callers. The most subtle parameter is however the second one describing as so-called MathSpace. This enum is also declared in IonAnalysis.h:

As the comment explains, this is done to separate two different possible behaviors of the MAdd/Msub nodes: They can optionally have an overflow check that leads to bailout if the operation would overflow the 32-bit signed integer range. If this check is enabled, the semantics of the operation correspond to the actual (infinite) integers. The usage of 32-bits as a representation are merely a speculative assumption possibly leading to bailout if violated. These semantics are represented by the Infinite MathSpace. On the other hand, the compiler can also generate unchecked additions or subtractions. These purposefully truncate the output to the 32-bit integer range as the usage site might perform such a truncation anyways (for example in a pattern like (x+5)|0 the bitwise OR would truncate its operands to 32-bit integers). This corresponds to doing arithmetic modulo 232 and thus is represented by the Modulo MathSpace. Finally, the Unknown MathSpace is simply a default value that can be passed into a ExtractLinearSum call. The meaning of this default value is that both of the described math spaces are acceptable and the function will simply pick the appropriate one based on the outermost operation. It will still however make sure to only allow a consistent MathSpace for all involved operations by passing the chosen space to the recursive calls instead of Unknown.

Root Cause

The ExtractLinearSum function is used in a few places in the Ion compiler. The most direct usage happens in jit/FoldLinearArithConstants.cpp where the compiler simply folds complicated linear expressions of mostly constants into one single Madd node. This direct usage will not concern us for the purposes of the vulnerability. The use that leads to the vulnerability is located in the TryEliminateBoundsCheck function inside jit/IonAnalysis.cpp:

The purpose of this function is to merge subsequent bounds check on the same object. For example, consider the following JavaScript operations:

These will generate two separate bounds checks with indices 𝑖 + 4 and 𝑖 + 7. Nodes of type MboundsCheck can check a whole range of indices at once. For this purpose, they store two integer offsets: minimum and maximum. When the bounds check is run the actual indices that are checked correspond to index + minimum and index + maximum where index is the actual input value into the node. In this case, the existing checks will have minimum and maximum both set to 0 (Actually it is possible that for these exact two bounds checks with index 𝑖 and both minimum/ maximum set to 4 (for the first check) and 7 (for the second check) are generated but we will ignore this for the sake of simplicity for now). The above bounds-check elimination pass will now try to merge these two bounds checks into one. To do this, first it is checked that both index expressions are linear sums corresponding to the same term (in this case the variable i). Instead of generating a new MboundsCheck node with index i, the compiler will simply reuse the first bounds-check and adjust the minimum and maximum fields. In this case as the index value of the seconds bounds check is larger by 3 the maximum field would be set to 3, while the minimum remains 0, and the actual index value stays i+4. While creating a clean conceptual difference between wrapping and infinite addition (and subtraction) semantics is a good design choice in SimpleLinearSum it seems like less care was taking at the call sites to make sure only appropriate semantics can be used. For example, bounds checks have inherently infinite semantics. If an array has length 20, then 10 is a valid index, but 232 + 10 is not. This means that using the wrapping Modulo math space could lead to wrong results. This becomes quite apparent with an actual bounds-check elimination. Consider an array being indexed at indices i and i+10. Normally i+10 should always be larger by exactly 10 than i so extending the maximum of the first check by 10 would cover it. But if the addition has unchecked Modulo semantics, this no longer holds true as i+10 might then potentially overflow if i is itself a large 32-bit integer like 232 − 5. The basic construct to trigger this bug is somewhat simple:

What happens here is that the bitwise OR with 0 will force a truncation to 32-bit integers, so that both the additions become unchecked wrapping additions. By the time that Bounds-Check Elimination phase will run, the bitwise ORs will have been eliminated because or-ing with 0 is a NOP. This leads to two array indices with i + 5 and i + 10 respectively as indices, where both additions are now wrapping. This means that ExtractLinearSum will be able to analyze those expressions, choosing the Modulo MathSpace, returning a SimpleLinearSum with term set to i for both. This in turn leads TryEliminateBoundsCheck to believe that the index of the second bounds check will always be larger by 5 than the first and eliminate it by increasing the first check’s maximum by 5. However, this is clearly incorrect already. If, for example, we set i to 231−7 as an index then the first index will be equal to 231 – 2 but the second one will be equal to −231 + 3, which is not a value covered by the corresponding range. This would not lead to an immediate problem if the involved bounds checks were of the 32-bit integer kind as they would bailout when encountering an index that added to the maximum offset exceeds 231 − 1. However, for a bounds check of IntPtr type, this is no problem as long as the length is large enough. We thus need an array with length greater than 231 to hit this bug as the bounds check will check up to the actual index (231 - 7) + 10 = 231 + 3 in the above example. This is probably impossible using normal JavaScript Arrays. Fortunately, Firefox's memory limits are large enough to allow for the creation of some rather huge typed arrays. Therefore we can simply create a Uint8Array of the size we need. As the bug is fundamentally about the confusion between an integer and its 32-bit wrapped version it can only ever be used to access an index off by exactly 232 from a valid index. For an addition that is barely overflowing like in the above example an index close to −231 can be achieved. This would not be very easy to exploit as it would result in a read and write primitive about 231 bytes in memory before the typed array. Therefore, it makes sense to use an even larger array of size 232. This will allow any bounds-check to pass as long as index value minimum and maximum are all non-negative signed 32-bit integers.

Triggering the Bug for Out-of-Bounds Read and Write

A simple out-of-bounds read POC might look something like the following:

Here, the bounds checks for the array accesses will again be merged into one. This single bounds check will have index equal to idx1 + 100 but maximum is set to 231 – 101 as this is what TryEliminateBoundsCheck computes to be the difference of the two indices again due to ignoring the possibility of wrap-arounds. The training iterations in the loop that are (partially) evaluated by the interpreter instead of JIT-compiled will simply access the indices (−50) + 100 = 50 and (−50) + (231 − 10) = 231 – 60 which are both in-bounds. For the final evaluation however idx1 will be equal to (231 − 200) + 100 = 231 − 100, but idx2 will be equal to (231 − 200) + (231 − 1) − 231 = −201 due to the wrap-around behavior. However, the merged bounds-check will still be passed as it will only check that there is a range of 231 − 99 valid indices starting from 231 – 100 which is true. This leads to the acceptance of a negative index and access to bytes before its start. In this case an out-of-bounds read is performed but the exploit logic is the same for a write primitive. The only thing left to explain is the role of the out object in the code. This is a technical neccessity due to the behavior of the MInt32ToIntPtr node. This node is inserted to convert our 32-bit value idx2 into an actual 64-bit array index. However there are some logics in jit/Lowering.cpp during visiting Int32ToIntPtr node that checks if a sign-extension is needed at all:

If the only use is as the index of the load then it is assumed that the value cannot be negative at all (as this could only result from a broken bounds check as in our case) and a simple zero-extension is performed instead of the usual sign extension. However, converting the value into a BigInt also uses the Int32ToIntPtr node as an intermediate leading to another use and disabling this optimization. Returning this BigInt using the out object prevents it from being optimized away.

Possibility of Related Bugs

Like mentioned above TryEliminateBoundsCheck is not the only place where ExtractLinearSum is used. Notably, it is also used in multiple places during the bounds check hoisting in jit/RangeAnalysis.cpp (sometimes also via the related function ExtractLinearInequality). Here, the function is again used with its default second argument of MathSpace::Unknown. Again, this choice seems incorrect. Consider a loop like for (let i = 0; i + 3 < 10 − 2; i = i+1) {...}. Here the loop analysis will basically conclude (by extracting various linear sums) that maximum 5 iterations will take place. This information is then used to hoist bounds checks which may depend linearly on some loop variables. However, if any of these additions are replaced by unchecked wrapping ones then these invariants could no longer hold. For example, the loop for (let i = 2**31− 5; i <= 2**31-1; i = (i+1)|0) {...} will run forever. There is one hurdle that however seems to make this harder (maybe impossible) to exploit and it is the compilation stage responsible for getting rid of the unneccessary bitwise OR happens after the bounds check hoisting (though before bounds check elimination). WebAssembly can also not be used as this optimization is disabled in that compilation mode.

Exploitation

As always, controlled out-of-bounds read and write primitives are quite powerful tools for further exploitation. The only slight difficulty is that the access is from a very large-typed array instead of the more usual smal heap object, meaning that it won’t be allocated in e.g. the nursery heap. Experimentally what works well is gaining access into large Map objects. Allocating a few of them will nearly always result in one map being right in front of the huge-typed array. This map object will contain tagged pointers to its values. Reading out such a pointer directly results in an addrOf primitive. Conversely overwriting a tagged pointer results in a fakeObj primitive. Once these two primitives are obtained exploitation becomes fairly standard. Some fake structures in the fixed inline storage of some (small) array buffers are crafted which are a fixed offset from the object location determined via addrOf. Using this a complete fake object crafted whose elements are also fake with a huge length. This object is not fully valid as there are some pointers to e.g. the object class that are hard to fake but it is good enough to temporarily get another out-of-bounds access this time into another overlapping ArrayBuffer. This can finally be used to overwrite the data address of this array buffer resulting in arbitrary read and write primitives. By embedding shellcode into float constants of a WASM function it would be possible to put the shellcode into executable memory. Finally all that remains is to overwrite the entry point offset of the WASM function to execute the shellcode. A demo of exploitation is available at https://www.youtube.com/watch?v=TG029NAGKs0

Final Notes

Despite fuzzing JavaScript engines at scale for a long time there are still high-quality bugs present yet to be found. It is notable that the bug described here could be challenging to be found using a fuzzer as it needs large allocations which may trigger performance penalties. This yet again proves the importance of source code review to find high quality bugs. You can also read more on what Mozilla has to say about this Pwn2Own entry in this post.