Finding CWE-369: Divide By Zero bugs with Binary Ninja (Part 1)
In this short series of long articles we’re going to take a look at automating the process of finding CWE-369: Divide By Zero bugs in compiled binaries with Binary Ninja.
tl;dr
We’re building something that does this:
Analyzing file: cwe369A_x64
Function: main[ALERT 1]: Possible divide by zero detected.
Function: main
Index: 12
Address: 0x67a
Operation: MLIL_SET_VAR_SSA
Instruction: temp0#1 = divs.dp.d(temp4#1:temp5#1, var_10#3)
Variable: var_10#3
Chain: ['var_10#3', 'var_10#1', '0']
I know “divide by zero” bugs aren’t the sexiest around, but these are great bugs to illustrate the power of Binary Ninja’s Intermediate Language (BNIL) suite, how to work with it, model simple bug manifestations, and address some of the challenges involved in program analysis.
In the simplest cases, a constant zero can be passed to the denominator of a division operation, signaling a detection. In more complex cases, things like nested loops, user input, and return values from functions can rear their ugly heads making division by zero complicated to find.
We’ll start simple, by breaking down straight forward manifestations of CWE-369 and working our way towards more complex cases and methods of modeling these complexities.
The Importance of Lifting to an IL: You might be wondering why we use an IL at all. Why not just analyze the disassembly? Well, we can. But we would be reproducing all of our work when switching to a new architecture. Also, most ILs (like Binary Ninja’s ILs) perform some amazing simplifications for us — letting us get stright to work without having to reinvent the wheel.
A Contrived Example
When modeling bugs for program analysis I like to write “smoke tests” which act as a sort of sanity test to make sure my models make sense. They are simple and to the point, and I generally keep them around for regression testing as I refine my models. Let’s take a look at one such smoke test for CWE-369.
Do you see the issue here? Line 14 shows a division operation where the variable data is the denominator. The variable data, however, can take two values, 0 (initialized on line 8) or 10 (assigned on line 12).
Static analysis test sets: While the industry is rather lacking in complex static analysis test cases there are a few exceptional resources to test your models against; like the Juliet C/C++ set¹, the cb-multios set², and the Rode0day archive³. If you know of any good sets, please share them in a comment, thank you!
If this application is executed with no arguments (argc = 1) then a divide by zero will occur and the application will throw an exception (which isn’t handled) causing a crash.
If this application is executed with at least two arguments (which aren’t actually used anywhere) then argc will be greater than 2, triggering line 12 to execute, reassigning data from 0 to 10. In this case, the program will finish as expected.
Before we go any further, let’s take a look at the main function as disassembled by Binary Ninja v1.3.
One of my favorite “quality of life” features Binary Ninja provides is the instruction annotations. Since we lose variable names in the compilation process, we can easily see (knowing the actual source) that the variable value is var_10.
We can tell this because we see it is initialized to 0 in the first basic block, and in the middle basic block, it’s reassigned to 10 (0xa). Looking for var_10 is much easier for me than looking for rbp-0x8 (its stack location).
This smoke test is compiled as x86–64, which results in the C division operation becoming an idiv (signed divide) instruction.
First, 100 is placed in EAX, then converted to a quadword, and divided by the value in var_10. Here’s where the potential issue occurs depending on the path taken to the idiv instruction.
Now let’s take a look at this same function (main) in Binary Ninja’s MLIL SSA (medium level intermediate language, static single assignment) form.
Here we can see a few interesting aspects of MLIL SSA. First, the SSA form really helps us track how and where variables are reassigned. The infix notation and equals assignments just feel more natural than worrying about the source and destination order.
What we’re really interested in here are the φ (phi) function (read about phi functions here) entering the last basic block and the divs (signed division) operation.
If we were to manually analyze this for divide by zero bugs, we would be on the lookout for div and mod operations. As we locate them, we’ll look at the second argument (the denominator), then trace it back to any assignments through associated phi functions to determine possible values for the denominator.
When you see a phi function, you can think of it as a “choice”. The choice here depends on which path through the control flow graph execution takes. In the phi function above (var_10#3 = phi(var_10#1, var_10#2) ), the value of var_10#3 (the eventual denominator used in the div operation) can become either, var_10#1 or var_10#2.
The “choice” of using either var_10#1 or var_10#2 depends on specific program constraints (i.e. how many arguments are passed into our smoke test).
Using this information, we can trace multiple paths back to their source and determine if any of them result in a definite or possible zero value. In our case, we can clearly see a definite zero value through var_10#3 → var_10#1 → 0.
Enough Talk, Let’s Automate This
Perhaps the best thing about Binary Ninja is the IL suite and how easy it is to access everything through Python. This alone is worth the price of a license. Let’s see what I mean by enumerating the MLIL SSA instructions in our smoke test.
The output of this code is as follows.
Analyzing file: cwe369A_x64
Function: main
var_1c#1 = argc#0.edi
var_28#1 = argv#0
var_10#1 = 0
var_c#1 = 0
if (var_1c#1 s<= 2) then 5 else 6 @ 0x66d
goto 8 @ 0x679
var_10#2 = 0xa
goto 8 @ 0x679
var_10#3 = ϕ(var_10#1, var_10#2)
temp2#1:temp3#1 = 0x64
temp4#1 = 0
temp5#1 = 0x64
temp0#1 = divs.dp.d(temp4#1:temp5#1, var_10#3)
temp6#1 = 0
temp7#1 = 0x64
temp1#1 = mods.dp.d(temp6#1:temp7#1, var_10#3)
rax#1 = zx.q(temp0#1)
rdx#1 = zx.q(temp1#1)
var_c_1#2 = rax#1.eax
rax_1#2 = zx.q(var_c_1#2)
rsi#1 = zx.q(rax_1#2.eax)
rax_2#3 = 0
mem#1 = 0x520(0x724, rsi#1, rdx#1) @ mem#0
rax_3#4 = 0
return 0Each MediumLevelILInstruction has associated MediumLevelILOperation. We can check these types to determine if we’ve found a division operation for a given instruction. In the case of CWE-369, division operations are a sink of interest to us.
Let’s see how to can enumerate MLIL SSA instructions to find various division operations. First, for each MLIL SSA instruction, we’ll print out all operands it’s made up of.
The relevant output of this script is shown below.
... snip ...
temp0#1 = divs.dp.d(temp4#1:temp5#1, var_10#3)
<ssa <var int32_t temp0> version 1>
<ssa <var int32_t temp4> version 1>
<ssa <var int32_t temp5> version 1>
<MLIL_VAR_SPLIT_SSA 4>
<ssa <var int32_t var_10> version 3>
<MLIL_VAR_SSA 4>
<MLIL_DIVS_DP 4>
<MLIL_SET_VAR_SSA 4>
... snip ...Notice the MLIL_DIVS_DP. This indicates a double-precision, signed division. But that’s not the only division type we’re interested in. If we review the MLIL documentation, we’ll see a total of five MLIL division operations.
binaryninja.MediumLevelILOperation.MLIL_DIVS
binaryninja.MediumLevelILOperation.MLIL_DIVS_DP
binaryninja.MediumLevelILOperation.MLIL_DIVU
binaryninja.MediumLevelILOperation.MLIL_DIVU_DP
binaryninja.MediumLevelILOperation.MLIL_FDIVSo let’s check for all of these when enumerating operands of MLIL instructions.
The output of this script is shown below.
Analyzing file: cwe369A_x64
Function: main
Div: temp0#1 = divs.dp.d(temp4#1:temp5#1, var_10#3)Now that we are able to cycle through functions, basic blocks, and instructions to hunt for sinks to analyze, we need to consider how to can trace the denominator variables back to interesting sources. Namely, something that may produce a zero value.
There are a few ways to do this, from repeatedly analyzing a function to determine variable reassignments as needed (an inefficient method), to adjacency lists (which fall apart relatively quickly as complexity increases), to evaluating transitive closures of variable reassignments.
A reasonable compromise among various approaches is to build a directed graph for each function containing a sink of interest and caching it until we’re finished running all of our analyzers. This means we perform extra work (creating our graph) only when it seems reasonable to do so (in the presence of a potentially vulnerable sink), and we retain that graph for additional use should we need it again.
Graphs provide a great structure for collecting data and processing it to uncover interesting relationships. This includes how variables might be reassigned from one value to another which is very useful in our simple test case. We’ll see additional useful features of graphs in future articles that help us uncover more complex manifestations of this bug and others.
In order to build a graph, we’ll use NetworkX. It’s a “Python package for the creation, manipulation, and study of the structure, dynamics, and functions of complex networks.” Using it, we can easily take advantage of complex algorithms designed to work on graphs.
First, we’ll build a digraph (directed graph) containing information from all MLIL_SET_VAR_SSA and MLIL_VAR_PHI operations. We do this because they represent the highest level of variable assignments we care about for this smoke test. The work is done in the build_symbol_graph function.
The (truncated) output of this script is shown below.
Analyzing file: cwe369A_x64
Function: main
Nodes:
['rax#0', 'rax#2', 'rax#1', '0', 'var_8#1', 'var_10#1', 'rbp#1', 'arg3#0', 'r9#1', '__return_addr#0', ...]Edges:
[('rax#0', 'rax#2'), ('rax#1', 'rax#2'), ('rax#1', 'var_c_1#2'), ('0', 'var_8#1'), ('0', 'var_10#1'), ('0', 'rbp#1'), ('0', 'var_c#1'), ('0', 'temp4#1'), ('0', 'temp6#1'), ...]
Now that we have a digraph representing variable assignment and potential assignments via phi functions, we’re ready to check for paths leading from our denominator variable to a zero (we’ll look at more complex cases in Part 2).
In the following code, we’ve added a find_all_paths_from function. It’s responsible for pathfinding a variable to root nodes using the NetworkX function, all_simple_paths.
We then check each path for a root node with a value of zero. If this happens, there exists a path from a zero directly to the denominator used in a division. Here’s the output when we run this script against our smoke test.
Analyzing file: cwe369A_x64
Function: main[ALERT 1]: Possible divide by zero detected.
Function: main
Index: 12
Address: 0x67a
Operation: MLIL_SET_VAR_SSA
Instruction: temp0#1 = divs.dp.d(temp4#1:temp5#1, var_10#3)
Variable: var_10#3
Chain: ['var_10#3', 'var_10#1', '0']
If you compare this output to the MLIL, you can see the “chain” reported, index, address, and instruction accurately describe the issue. Here’s the MLIL SSA image again so you don’t have to scroll back up to compare.
With that, we’ve successfully modeled a simple CWE-369 manifestation. There are many like it, but this is probably the simplest case you’ll ever see.
Next week (or, maybe even now if you’re in the future) I’ll publish Part 2 covering some interesting cases that arise when we compile this smoke test for ARM which leads to an interesting false negative. Then we’ll add that to our model and explore additional sources of zero values, like atoi and other common functions.
From there, we’ll slowly build up complexity in Part 3 to address computations in loops and make our way into interprocedural data flow analysis in Part 4. I’ll aim for a weekly cadence to finish off this series on program analysis to find CWE-369.
After that, who knows, maybe we’ll look at bugs people actually care about. ;) Thanks for reading, you’re amazing!
Series Links
Please use this handy set of links to navigate this series on finding CWE-369: Divide By Zero bugs with Binary Ninja.
Part 1: Mapping constant 0 values to denominators
Part 2: Zero values stemming from well-known functions, new sinks
Part 3: Considering reachability by evaluating path constraints
Part 4: Tracking operations occurring in loops
Part 5: Interprocedural data flow
Footnotes
1: The Juliet C/C++ corpus is developed by NSA Center for Assured Software. Version 1.3 contains 64,099 test cases covering numerous manifestations of 119 CWEs.
2. The cb-multios corpus originated from the DARPA Cyber Grand Challenge program. This corpus of challenge binaries (cb) was built by many organizations including; AFRL, Cromulence, Kaprica Security, Lunge Technology, Narf Industries, Naval Postgraduate School, Thought Networks, and West Point Military Academy. Trail of Bits put in significant effort to modify these challenges and build system for multiple operating systems.
3. Rode0day is a collaboration between researchers at MIT, MIT Lincoln Laboratory, Northeastern University, and NYU. It’s a bug finding competition featuring applications with injected vulnerabilities via LAVA (PDF). They maintain an archive of previous challenge sets for public use.
About the author
John Toterhi is a security researcher at Battelle Memorial Institute where he specializes in reverse engineering, vulnerability research, and tool development. When he’s not being a computer nerd, he’s probably picking up a new hobby or telling bad dad jokes. You can connect with John on LinkedIn, GitHub, Twitter, and Medium.
