Spectre checker keeps up with the latest exploits
In a recent blog post, Detecting Spectre vulnerability exploits with static analysis, we showed how developers can use static analysis to help protect their applications from the Spectre variant 1 vulnerability (bounds check bypass). Synopsys Software Integrity Group released a checker for Coverity (AUDIT.SPECULATIVE_EXECUTION_DATA_LEAK) that helps developers identify vulnerable code. The result is increased protection against Spectre without the performance cost of completely forgoing speculative execution.
Turns out it’s called Spectre for a reason. Because speculative execution is at the core of modern computing, the security community is still trying to grasp the full security implications of the vulnerability. So Spectre could haunt us indefinitely, manifesting over and over in new forms and variations. Researchers continue to discover new ways that the Spectre vulnerability can be used to exploit code that was previously thought to be out of reach.
To stay relevant, a Spectre checker must keep up with the latest developments.
The variants of Spectre variant 1
For code to be vulnerable to Spectre variant 1, it must have a very specific structure:
if (x < array1_size) {
v = array2[array1[x]*256]
}
If attackers can control x, and assuming the right cache configuration, they can trick the CPU into speculatively executing the memory access and reading array1[x] even when x is out of bounds. In doing so, the CPU might expose sensitive information that can later be retrieved by side-channel attacks.
But because there are many ways to write equivalent code, there are many variations on the above pattern. Paul Koch, the author of the original Spectre white paper, has published several of them in a follow-up post. The following examples are his.
Some variants differ syntactically but are semantically equivalent to the original. One such example uses the ternary choice operator instead of an if-statement for the bounds check:
void victim_function_v08(size_t x) {
temp &= array2[array1[x < array1_size ? (x + 1) : 0] * 512];
}
Other patterns generalize what it means to have a safety check. The check does not have to be an inequality check; it just has to guard against an unsafe memory access. For example, the code below compares against a last known good value to ensure a safe memory access:
void victim_function_v07(size_t x) {
static size_t last_x = 0;
if (x == last_x)
temp &= array2[array1[x] * 512];
if (x < array1_size)
last_x = x;
}
Yet other patterns depend on attackers being able to control more than one value. In the example below, if attackers can also control the value of k, they can use side-channel attacks to access the sensitive data in array1[x]:
void victim_function_v10(size_t x, uint8_t k) {
if (x < array1_size) {
if (array1[x] == k)
temp &= array2[0];
}
}
In response to these new patterns, we have extended our original Spectre checker, AUDIT.SPECULATIVE_EXECUTION_DATA_LEAK, to handle 12 out of the 15 patterns. For the 3 remaining, we cover variations (e.g., parameter vs. global) and are in the process of expanding support.
Identifying new Spectre variants
Of course, the saga continues. Just recently, a brand-new variant of the Spectre vulnerability called speculative store bypass was made public. Here, speculative execution occurs during data load and can allow a memory read to occur before an older write. Thus, the store could read stale data from memory. Some of the code patterns vulnerable to speculative store bypass overlap with those vulnerable to variant 1, but others are new (see the developer guidance from Microsoft for examples). We are actively working on extending our current checker to address these additional patterns.
Recognizing remediation
Finding vulnerable code is only the first step in escaping Spectre. Fixing it is the second. The checker must be able to detect when the vulnerable code has been appropriately patched. For this reason, we have extended the AUDIT.SPECULATIVE_EXECUTION_DATA_LEAK checker with the capability to identify serialization instructions. We support the lfence and mfence instructions (and the _mm_lfence() and _mm_mfence() intrinsics) for x86, and the DMB (data memory barrier) and DSB (data synchronization barrier) instructions for ARM.
Configuring the Spectre checker
As we have seen, protecting against the Spectre vulnerability is a moving target. Static analysis will never be able to detect all possible patterns, especially as new variations are discovered. For this reason, we designed our checker to be configurable in terms of what patterns it considers vulnerable. This means Coverity users can tweak the sensitivity of the checker to match their specific application security needs. And at the extreme, the Spectre checker can report defects on all nested memory accesses.
Eliminate common software security vulnerabilities in your source code at any depth.
