Log in

No account? Create an account

Previous Entry | Next Entry

There was a time when I felt that Linux-kernel RCU was too low-level to possibly be the subject of a security exploit, but Rowhammer put paid to that naive notion. And it finally happened earlier this year. Now, I could claim that I did nothing wrong. After all, RCU worked as advertised. The issue was instead that RCU has multiple flavors:


  1. RCU-bh for code that is subject to network-based denial-of-service attacks.
  2. RCU-sched for code that must interact with interrupt/NMI handlers or with preemption-disabled regions of code, and for general-purpose use in CONFIG_PREEMPT=n kernels.
  3. RCU-preempt for general-purpose use in CONFIG_PREEMPT=y kernels.

The real problem was that someone used one flavor in one part of their RCU algorithm, and another flavor in another part. This has roughly the same effect on your kernel's health and well-being as does acquiring the wrong lock. And, as luck would have it, the resulting bug proved to be exploitable. To his credit, Linus Torvalds noted that having multiple RCU flavors was a root cause, and so he asked that I do something to prevent future similar security-exploitable confusion. After some discussion, it was decided that I try to merge the three flavors of RCU into “one flavor to rule them all”.

Which I have now done in the relative privacy of my -rcu git tree (as in “git clone https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git” followed by “git checkout dev”).

So what has this got to do with validation in general or formal verification in particular?

Just this: Over the past few months, I have taken a meataxe to Linux-kernel RCU, which implies the injection of any number of bugs. If you would like your formal-verification tool/methodology to be the first to find a bug in Linux-kernel RCU that I don't already know about, this would be an excellent time to give it a try. And yes, all those qualifiers are necessary, as several groups have used formal-verification tools to find bugs in Linux-kernel RCU that I did already know about.

More generally, given the large number of swings I took with said meataxe, if your formal verification tool cannot find bugs in the current dev version of RCU, you might need to entertain the possibility that your formal verification tool cannot find bugs!