Analyze OpenBSD’s Kernel with Domain-Specific Knowledge

In this article I want to show how we can analyze the OpenBSD kernel with domain-specific knowledge of spl(9) locking primitives, to find programming errors.

This work was sponsored by Genua GmbH. Genua uses OpenBSD as a basis of many of their products. They allow developers to have a retreat twice a year for one week to hack on their own projects. This work is a result of it.

Background

The OpenBSD kernel is written in the C programming language. That means programmers have to take care of resource usage all by themselves. For example, if you take a lock in one function, it has to be released in all conditions where the function returns. The C compiler already inspects the code, so why not make it aware of locking primitives? That way it can emit a warning when a lock has been taken by a function, but has not been released at any one function return.

For example, consider the following function:

void function(void) {
        lock();
        perform_work();
        unlock();
}

Now imagine that we need to check a precondition first, before performing the work. The code could be changed to the following:

void function(void) {
        lock();
        if (!precondition)
                return;
        perform_work();
        unlock();
}

You can see that we miss an unlock operation when the precondition is not met. It might be obvious in the example above, but when you have a large and complicated block of code running under a lock, a missing unlock operation might not be visible right away.

Idea

OpenBSD uses LLVM/clang for some time now. This compiler suite allows the use of plugins to extend the compiler and make it learn new tricks. We can use this mechanism to make the compiler aware of the locking primitives used in the OpenBSD kernel specifically. The easiest lock to analyze is spl(9). There is only a lock and an unlock operation on a single, global, lock. That means, we do not need to distinguish between different lock objects. Also, there is no try-to-lock operation, which would make analysis more complicated. So let’s start out by checking spl(9). As a rudimentary first step, we only need to count the number of lock operations and the number of unlock operations in any conditional branch of all functions. If they are the same, lock operations are evenly balanced and there is no locking error.

Ok, that’s a pretty naïve view of the world. In reality, code is much more complex. But let’s see how far it gets us.

Implementation

LLVM/clang supports writing plugins in C++. There are also bindings to other languages, most notable is Python. OpenBSD’s base version of clang even seems to support plugins. There are also examples imported from upstream LLVM. However, the documentation on how to write a plugin is rather sparse. And I do not expect OpenBSD to even ship language bindings.

But there is a Python module that implements a C language parser, which can be used to parse C source files into an abstract syntax tree (AST) for inspection. It’s called pycparser, and it’s description states:

pycparser is a complete parser of the C language, written in pure Python using the PLY parsing library. It parses C code into an AST and can serve as a front-end for C compilers or analysis tools.

While pycparser implements standard C99 features, for some code in the OpenBSD kernel this is not enough. The pycparser library does not handle some C attributes, or some builtins like __typeof. Furthermore, the DRM subsystem makes good use of GNU extensions, as it is imported from Linux. Luckily there is pycparserext, extending the original pycparser. It’s description says:

Extended functionality for Eli Bendersky’s pycparser, in particular support for parsing GNU extensions and OpenCL.

Looks like what we want. I have written a tool around pycparserext to analyze the OpenBSD kernel. It is called Lock Balancing Checker (lbc). The following is a write-up on the peculiarities of the implementation and lessons learned.

Lock Balancing Checker

The pycparserext library cannot handle plain source files directly. It would need to know about include paths and preprocessor defines to properly build an AST. Therefore, a patch to the OpenBSD source tree exists that changes config(8) and the kernel Makefile (for AMD64) to emit preprocessed source files. These files are self-contained — there are no external dependencies. These can be fed to lbc for analysis.

After reading the file, lbc needs to preprocess it some more to get rid of some C code constructs that pycparserext does not understand. They get replaced by something unobtrusive. The only thing missing so far is support for a GNU extension to the ternary operator. Statements like foo = foo ?: bar; can not be parsed correctly. This operator is used in the DRM code, taken from Linux. After processing the input, pycparserext builds an AST of the file and lbc starts analyzing every function in it. The pycparserext library implements a visitor pattern. lbc only implements functions for AST nodes that are interesting. These include function call nodes to check if any of the locking primitives is called.

The generated AST is a tree that gets walked depth-first. Walking the tree, or visiting each node in pycparser’s terms, can be viewed as a simple iteration over each source code line. The lbc analyzer notes interesting things when they fly by, like the locking state. But when the code flow splits, the internal analyzer state needs to split, too. In lbc, this is realized by forking the current process. One program continues to analyzes one part, while the other analyzes the split-out part., This is useful for switch cases. When lbc reaches a break or continue statement, it needs to stop iterating over the current sub-tree and come back to a previous place. This is realized with exceptions. Every analysis of a loop body or switch statement has a point where these exceptions are caught and the analysis can continue from there.

The most cumbersome part is handlinggoto statements. The way pycparser handles labels is by putting the statement after the label as sub-tree below the label node. That means we cannot simply “jump” to a label node, we would only analyze one instruction that was attached to it. As a workaround, lbc collects all labels when they fly by and evaluates them in the goto visitor. For backwards jumps, the label has been visited already. Following the label again would potentially lead to an infinite loop. If the loop has break-outs, other flows will follow them. lbc stops processing this flow altogether. In case of a jump forward, lbc ignores all subsequent AST nodes during its visit, until it has reached the label. Then it continues normally. The whole thing this is particularly hairy when labels are nested in loops or switch cases.

Finally, the code analysis either stops at the end of a function, or at a return statement. In both cases the locking primitives should have been called in a balanced manner. There should be the same number of calls to locking functions as to unlocking functions. If this is not the case, lbc complains. The panic() function is handled in a special way. When this function is called, the programmer has given up anyway, indicating that the system is busted. That also means we cannot make any reasonable judgement on the lock balancing state and abort processing the flow.

Limitations and Optimizations

Given the humble assumptions we started out with, the Lock Balancing Checker is far from perfect. There are a lot of false-positives. For example, all wrapper functions around spl(9) get flagged. These include mtx_enter_try() and mtx_enter_leave(), which are used for another class of locks and rely on spl(9). The emitted messages read:

kern_lock.i: mtx_enter_try(): Error: Unbalanced lock status at return statement. LockStatus(spl=1)
                                                                                  
kern_lock.i: mtx_leave(): Error: Unbalanced lock status at end of function. LockStatus(spl=-1)

That means lbc has found a branch where it visits a return statement in mtx_enter_try() where the spl(9) was raised, but not lowered again (the count is positive). Conversely, in mtx_leave() the function finishes with the spl(9) lock unlocked one too many (the count is negative). That is sign that these functions are used as a wrappers. It is obvious that mutex(9) functions are wrappers. With other functions, it is less obvious, at least for me. E.g. sleep_setup() and sleep_finish().

The biggest source of false positives is the Fast Filesystem. It has a lot of functions that lock the spl(9), but then call another function or unlock it again. Because lbc only analyzes each function individually, it cannot analyze this code properly and flags false positives.

One current limitation of the analyzer is with code like the following:

void
do_somthing(needs_lock) {
        int s;
        if (needs_lock)
                s = splhigh();
        [ ... ]
        if (needs_lock)
                splx(s);
}

The analyzer splits the flow at each branch in the function. One part analyzes the if-condition branch, the other one the else-condition branch, which is empty in these cases. That results in four different flows.

+-----+-------------+-------------+
| Nr. |   top-if    |  bottom-if  |
+-----+-------------+-------------+
|   1 | if-branch   | if-branch   |
|   2 | if-branch   | else-branch |
|   3 | else-branch | if-branch   |
|   4 | else-branch | else-branch |
+-----+-------------+-------------+

There is no problem in flow 1 and 4. Both flows either take the branch or they don’t. In both cases the lock is balanced at the end of the function. The other two cases analyze the code with only one of the branches taken. The result is an unbalanced lock status at the end of the function. Although, when looking at the code, it is clear that only flows 1 and 4 are valid. One way around this is to collect all if conditions and note if they were taken previously. This, of course, only works if the exact same conditions re-appears, like in our simple example above.

I also did not handle spl0(), which is used after fork() or during cpu_configure() to re-enable interrupts from whatever level it was previously. This function is used, because the previous level was saved on another stack. From the perspective of the analyzer this is an unlock operation, without a matching locking call.

Despite the shortcomings, there were legitimate bugs found with that tool. They are covered in the next section.

Results

The Lock Balancing Checker found some genuine bugs in the OpenBSD code base. None of them are earth-shattering, though.

A missing return statement in an error path was found for the for the igc(4) network interface driver, which leads to a double-unlock. Admittedly, that does not do any harm. In theory the spl(9) lock can be unlocked multiple times without problems. But it still remains a semantic error.

if_igc.i: igc_init(): Error: Unbalanced lock status at end of function. LockStatus(spl=-1)

A missing call to the splx() unlock operation in an error path was found in the urtwn(4) wireless network interface driver. This is more serious. That may lead to certain interrupts being blocked, potentially preventing the system from making progress. The end result is a hanging machine.

if_urtwn.i: urtwn_rx_frame(): Error: Unbalanced lock status at return statement. LockStatus(spl=1)

A similar problem has been identified for uaq(4) and mcx(4).

Conclusion

Unfortunately, I did not manage to write an LLVM/clang plugin, as outlined in the beginning. If we could manage to do that and hook it into the kernel build, it would give more confidence in the code. Ok, that would also mean to get rid of the false-positives first. But that remains an exercise for the reader. :)

I have shown that static analysis of the OpenBSD kernel with domain-specific knowledge yields in bugs being found. A tool exists that maybe even can be extended to different types of locks. The MP-Lock comes to mind with a similar API interface.

Thanks again to Genua for allowing me to hack on such a cool project during working hours, wich benefits their products and the OpenBSD community alike.