MindShaRE: Automated Bug Hunting by Modeling Vulnerable CodeJuly 16, 2019 | Jasiel Spelman
During the week I took the training, but completely unrelated to it, Nico Waisman tweeted about a bug class he was modeling at the source code level using Semmle's QL. For those not familiar with it, QL is a query language used to analyze source code. The gist of Nico’s tweet is fairly simple: look for a call to
sscanf function where the return value is not properly checked, which indicates a potential vulnerability. Applying what you’ve learned is a great way of cementing knowledge. Given the timing of Nico’s tweet, it seemed like a perfect pattern to try and model. As opposed to the source-level approach that Nico showed, however, we will model the bug pattern at the binary level.
Here are two examples of this bug class:
The return value of
sscanf is either
EOF or is the number of arguments filled. In the first example, there's no checking whatsoever of the return value of
sscanf. In the second example, it only checks that the return value is non-zero, so an input failure or just parsing and filling one or two of the items could all result in hitting the success path, which potentially results in uninitialized variables being used.
For completeness, let’s look at what it might look like to do things correctly:
In this example, all three arguments have been initialized, and the return value of
sscanf is checked to ensure that it actually parsed and filled all three variables.
Now that we have an understanding of a pattern to look at, we can try to model it. We want to find calls to
sscanf and then see if the return value is used in a comparison. We also want to get the number of arguments to the
sscanf call. Although I won’t discuss it in this blog, it could be useful to walk through the definitions of all the
sscanf arguments to see if they were initialized, because even if the return value isn’t checked, that would make a particular match less interesting.
Binary Ninja supports multiple architectures and has several intermediate forms as well as a decently documented API. One of the types of intermediate forms they support is static single assignment (SSA) form. By analyzing a function based on its SSA form, we can use the API to find calls to
sscanf and trace the return value to anywhere it might be used.
The script starts off by looking up the symbol name for
sscanf and verifying that it is an imported function. After that, the script iterates through the Medium Level Intermediate Language (MLIL) SSA form, filtering on function calls where the callee address is
Once we have a call to
sscanf, we iterate through uses of the return value. We try to follow through where the return value is assigned to a variable until we see it being used within a conditional, and then try to grab the value that it is being compared against. For the sake of simplicity, all comparisons are treated equally, which means our output can be invalid. For example, a less-than comparison is treated the same as an equality comparison.
Running our script against the toy binary produces the following output:
Using the IDA API
For IDA, I opted to use the Hex-Rays decompiler API. This was partially because I have a license, but mostly because otherwise I’d have to implement architecture-specific code, either to directly perform analysis on, or to lift it to an intermediate representation of my own. I could also have outsourced this task to another tool, but at that point, I wouldn’t really be using IDA. The biggest hurdle in writing the tool for IDA was that the documentation is incredibly lacking. On the other hand, a benefit of using IDA over the others is that FLIRT signatures have a chance of finding any
sscanf functions built-in to the library being analyzed, so we don’t have to depend on an import table.
Similar to Binary Ninja, we start off by looking for
sscanf and then look at the callers.
For each caller, we get a
citem_t node corresponding to the assembly-level call, then look at the parent. If the parent node’s operation is
cit_if, then we know a comparison of some sort is occurring. Note that we’re ignoring other types of conditionals, such as less-than. If the parent node is a
cit_expr operation and the grandparent node is a
cit_block operation, then the value is not being used at all. If we’re looking at a
cot_eq operation, we can try to extract the value it is compared against.
Here’s the output when we run this against the toy binary:
Using the Ghidra API
Of the three disassemblers, Ghidra is the one I’m the least familiar with. The API is documented but voluminous. I ended up spending more time getting started with Ghidra than with Binary Ninja or IDA. It would have been a little easier to write the Ghidra tool in Java, but to stay consistent with the other two, I wrote it in Python after seeing this example from 0xAlexei and 0xJeremy’s INFILTRATE 2019 presentation.
Unlike the other examples, we have to set up the decompiler first. After that, we search the symbol table for
sscanf, find any references, and then decompile the function that contains the reference. We then hand things off to the function responsible for checking for vulnerabilities.
Just as before, we filter on calls to
sscanf. Ghidra refers to variable uses as
descendants, so we iterate through each descendant looking for when the use is within an equality operation. When we find one, if it’s against a constant, we’ll save it off for reporting.
Ghidra’s headless mode is incredibly verbose, so I removed the initial messages, resulting in the following:
Note that these are just examples, and running them on actual binaries will take some modification. For example, outside of the Binary Ninja, we’re disregarding any comparisons that aren’t an equality check and we’re not properly looking at when the return value is saved to a local variable before being checked. Even for the Binary Ninja example, we’re not properly checking things, as all comparisons are treated the same. The example scripts as well as a binary to run them against can be found here.
The scripts shown above represent just one approach to vulnerability modeling. Another technique would be to use a Visitor pattern. In fact, not using a Visitor pattern made the IDA script slightly more difficult to write, as I did not see a way of seeing a variable’s uses without employing a Visitor. For an example using that pattern, check out this blog from Trail of Bits. As a bonus, they’re also showing how you might use Z3 to aid in modeling bugs.
Modeling of vulnerabilities can be an incredibly powerful way of finding areas of a binary to audit. All three disassemblers have their own merits and hopefully these examples offer a good starting point regardless of where one chooses to focus their time. If you find any vulnerabilities using these methods, consider submitting it to our program.