Finding Spectre vulnerabilities with smatch

Spectre variant 1 is the result of the processor incorrectly predicting the results of a bounds check; it then speculatively executes code with a parameter (such as an array index) that falls outside of its allowed range. This problem can be mitigated by disabling speculative execution in situations where an array index is under the control of a potential attacker. In the kernel, that is done by replacing code like:

    value = array[index];

with:

    index = array_index_nospec(index, ARRAY_SIZE);
    value = array[index];

That's the easy part; the hard part is finding the places in the kernel where the array_index_nospec() macro should be used. Until now, the only tool available has been the proprietary Coverity checker, which is not accessible to everybody and produces a fair number of false positives. As a result, there are only a handful of array_index_nospec() calls in current kernels.

Carpenter's addition to smatch changes that situation by providing a free tool that can search for potential Spectre variant-1 vulnerabilities. The algorithm is simple enough in concept:

This test returns a list of about 800 places where array_index_nospec() should be used. Carpenter assumes that a large percentage of these are false positives, and has asked for suggestions on how the test could be made more accurate. Instead of offering suggestions, though, both Thomas Gleixner and Peter Zijlstra confirmed that a number of the reports were accurate; Zijlstra said "I fear that many are actually things we want to fix". He followed up with a patch series fixing seven of them — nearly doubling the number of array_index_nospec() calls in the kernel.

Once the low-hanging fruit has been tackled, there probably will be a focus on improving the tests in smatch to filter out the inevitable false positives and to be sure that vulnerable sites are not slipping through. But, now that there is a free tool to do this checking, progress in this area can be expected to accelerate. Perhaps it will be possible to find — and fix — many of the existing Spectre vulnerabilities before the attackers get there.

static struct tm6000_fmt format[] = {
	{
		.name     = "4:2:2, packed, YVY2",
		.fourcc   = V4L2_PIX_FMT_YUYV,
		.depth    = 16,
	}, {
		.name     = "4:2:2, packed, UYVY",
		.fourcc   = V4L2_PIX_FMT_UYVY,
		.depth    = 16,
	}, {
		.name     = "A/V + VBI mux packet",
		.fourcc   = V4L2_PIX_FMT_TM6000,
		.depth    = 16,
	}
};

$ v4l2-ctl --list-formats

$ v4l2-ctl --list-formats
ioctl: VIDIOC_ENUM_FMT
	Index       : 0
	Type        : Video Capture
	Pixel Format: 'YUYV'
	Name        : YUYV 4:2:2

	Index       : 1
	Type        : Video Capture
	Pixel Format: 'UYVY'
	Name        : UYVY 4:2:2

	Index       : 2
	Type        : Video Capture
	Pixel Format: 'TM60'
	Name        : A/V + VBI Mux Packet