Your browser does not support JavaScript!

By Jerry McGoveran, Senior Security Applications Engineer, Tortuga Logic

This is the second post in a two-part series on how Radix can be used to detect and discover microarchitectural vulnerabilities such as Meltdown and Spectre. The prior post, Detecting Meltdown Using Radix, written by Nicole Fern, discussed the Meltdown vulnerability, formulated Meltdown as a hardware information flow property violation, and provided details on how Tortuga Logic’s Radix solution can be used to ensure future generations of processors are not vulnerable to Meltdown.

In this second post, we will do the same for the Spectre vulnerability. Tortuga Logic in collaboration with a processor vendor has developed and implemented a novel methodology for tracking data manipulated by squashed CPU instructions in order to determine if leakage through microarchitectural side-channels is possible.

What is Spectre?

Spectre is a sophisticated vulnerability in which the memory isolation boundaries in a modern processor are violated using speculative execution and branch prediction to send privileged data to the CPU cache. The privileged data can then be extracted via a cache timing side channel attack.  For more information, the paper Spectre Attacks: Exploiting Speculative Execution provides a background discussion of these extraction methods.

Spectre has over a dozen variants but the two most prominent are Variant 1 (CVE-2017-5753) and Variant 2 (CVE-2017-5715).  This post will use Spectre Variant 1 to illustrate a method we used with one of our customers to identify this vulnerability in their design.

Spectre V1 exploits conditional branching scenarios, such as bounds checking on an array index, to force speculative execution of certain instructions.  This involves the attacker training the branch prediction logic to expect to branch one way, then taking the opposite branch so that the mispredicted branch instructions are speculatively executed.  If those speculative instructions illegally access secure memory, privileged data may be leaked to the cache before the branch resolution catches up and squashes the illegal access.  Architecturally, the squashed illegal instructions have no effect, but the cache state has already been updated and will remain so until it is overwritten or the cache is flushed.  This information in the cache can then be exfiltrated by the attacker using known methods.

Spectre V2 is a similar vulnerability in indirect branching and is not addressed in this post but the general techniques presented here could be equally applied to this variant.

Figure 1 illustrates the functional processor blocks and operations involved in the Spectre V1 vulnerability.  An attacker, having already primed the cache and trained the branch predictor, offers the branch an out of bounds index (Step 0 in Figure 1) which will cause the branch prediction to be incorrect.  Because the branch predictor has been conditioned (poisoned) to expect an in bounds index, the attacker can exploit a race condition where data is speculatively read from the memory subsystem (red path in Figure 1) in parallel with the branch condition resolution (green path in Figure 1).  Due to out-of-order execution, the attacker’s illegal read from memory (Step 2) can be used in subsequent transient instructions (Steps 3 and 4) even though the branch condition check eventually fails (Step 5).

What makes this so difficult to detect, is that the speculative illegal instructions don’t cause an exception unless they are ultimately committed.  A squashed instruction cannot cause an exception, so it leaves no trace of its illegal activity for security measures to detect.

A key point to note is that transient (squashed speculative) instructions don’t affect the architectural state, i.e. intended interactions between hardware and software. However, in devices vulnerable to Spectre and other microarchitectural side-channels, transient instructions can alter the state of microarchitectural structures, such as caches, in a way that is detectable by malicious programs. Leaking the value of the speculatively loaded data through a cache timing side-channel only requires transiently executing one or two additional instructions before the branch check failure is handled (Step 6).

How does Spectre differ from Meltdown?

Both Meltdown and Spectre exploit race conditions in order to access secure information.  Meltdown races against a hardware permissions check that will result in an exception.  The attacker code accesses data that it is not permitted to read, but while the hardware checks the permissions, the data is conditionally loaded.  In the time it takes to check permissions and execute an exception, the cache state has been altered and the data leaked.  This is entirely a hardware problem, and no privileged execution of code is required for this exploit.

Spectre races against a branch prediction resolution in the speculative execution logic.  The attacker code manipulates the architecture into speculatively executing code that will expose secure data.  The attacker does not attempt to read secure data directly but instead tricks the secure system into leaking it for them via speculation.  Because the illegal instructions end up being squashed, permission checks are bypassed and no exception fault occurs.  From an architectural perspective, everything is executed legally.  When the branching condition is finally resolved, the speculatively executed instructions are squashed, but the secure data has already altered the state of the cache.  There is no indication in the architecture that anything untoward has occurred.  This makes Spectre especially difficult to detect and mitigate.

In short, Meltdown attempts to circumvent hardware-enforced permission checks but Spectre attempts to exploit speculatively executed illegal instructions due to branch misprediction to manipulate the exposure of secure data.  With Spectre, the instructions violating security never happen from an architectural point of view.

Example code

Let’s visualize the attack from the code level.  The essence of the attack is shown by the pseudo code below.  (See the paper for full details on the Spectre attack.)  When the code is executed, it reveals the value of array1[index] due to the speculative execution of the conditional branch. The attacker structures the attack such that array1[index] returns information from the victim then recovers it through a cache timing side channel.

  • Line 1: shows the attacker loading register R25 with a value which is in the address space of the victim.
  • Line 3: compares the index value (R25) to the array size.
  • Line 4: branches if the index is greater than or equal to the array size. Due to the attacker’s training of the branch predictor, the BGE branch will be predicted to not be taken and the next set of instructions will be executed and eventually squashed.
  • Line 5: the LOAD instruction (shaded in red) loads register R3 using the attacker’s index value in register R25.
  • Lines 5-8: The last four instructions will be speculatively executed and subsequently squashed. However, this still causes a change in the cache state, notably the cache tag. This tag can then be exfiltrated by the attacker using a cache timing side channel.

Formulating Spectre as an Information Flow Property

Detecting vulnerabilities like Spectre is challenging because the illegal loading of the data and transmission through the timing side-channel occurs during transient or speculative execution, which is invisible to the programmer’s view of the processor. The behavior of processors during speculation or out-of-order execution must be analyzed in a security context before tapeout to avoid similar vulnerabilities in next generation CPUs. Spectre is a violation of the following security requirement:

Data manipulated by squashed instructions in the victim context that are influenced by the attacker context should not affect cache state.

If a verifiable security property can be written for a processor RTL design, then Spectre-like vulnerabilities can be detected and mitigated pre-silicon.

Determining the effect of squashed instructions on cache allocation is extremely difficult without analysis tools that understand the concept of information flow.  As discussed above, the ambiguity of speculatively executed, apparently legal instructions in a Spectre exploit makes Spectre detection quite difficult, if not impossible, for traditional verification methods.  We need to understand the software context in order to identify the violation.  This is made much easier using hardware information flow tracking tools such as Tortuga Logic’s Radix.

Radix dynamically tracks information flows in RTL designs during simulation or emulation. Radix security rules control what design information should be tracked, when it should be tracked, and where in the design it should not propagate to.

The basic syntax of a Radix Security Rule is:

{ source } when ( condition ) =/=> { destination }

where “=/=>” is the no-flow operator. The rule will fail if information from the source signal set propagates to any signal in the destination signal set. Both the source and destination consist of a set of RTL design signals. The “when” keyword specifies conditions which must hold to start tracking information from the source, and consists of an RTL signal or a boolean expression using one or more RTL signals.

Below is the high-level structure of the Radix Security Rule we created to detect Spectre for one of our customers:

Instruction Operands when (Influenced by unprivileged process && Instruction will be squashed) =/=> Cache State

Figure 3 shows where in a typical processor design the source and destination signals are located. The red dotted line emanating from the source shows the information flow tracked by the security rule.  In this case, the source (red dashed box) is the Register Bank where the attacker stores a value used to index an array that loads data from privileged memory.  The information flows from the memory through the indexed Load instructions to the destination (blue dashed box) in the Tag RAM for the L1 data cache.  The green dashed boxes show the conditions necessary for tagging the source data for information flow tracking: the operand in the Register Bank must be attacker-influenced, and the instruction using it must be a speculative instruction that will be squashed.

General Application of Radix for Microarchitectural Side Channels

In cooperation with one of our customers, Tortuga Logic wrote this security rule and verified its ability to detect a known vulnerability to Spectre V1 on one of their commercial CPUs.  We have since demonstrated that the rule is portable to other CPUs as well, which allows quick assessment of whether Spectre-class vulnerabilities are present.

In addition to detecting known or suspected vulnerabilities, the rule provides significant additional value over a directed test case approach.  First, it speeds up the development of mitigations by providing a quick method to verify their effectiveness.  Second, information flow technology can illuminate additional microarchitectural structures that may leak data through other covert channels.

Software mitigations for Spectre are very costly in terms of performance, but there may be no alternatives for vulnerable CPUs already deployed in the field. CPU designs under active development have the opportunity to use the Spectre Radix Security Rule during RTL simulation and emulation to examine the hardware and verify that data is not leaked to unprivileged contexts during speculative execution due to poisoned branch predictors.

Mitigations that successfully block such leaks can be further analyzed using Radix analysis tools to explore other places where the secure information flows making this a powerful method for finding currently unknown vulnerabilities.  You can learn more about how these analysis tools can assist your security verification efforts in our Solutions page.

Other Applications

The Radix security rule that we defined in this post to detect Spectre V1 is general enough to detect other known vulnerabilities with no modifications.  For example, this rule will also detect the following:

This shows how Radix is a powerful force multiplier for your security team’s productivity and effectiveness.