Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL

Ever since the Spectre and Meltdown attacks proved Transient Execution Side Channels to be a fundamental vulnerability of modern processors, secure microarchitecture design is a challenge considered urgent by chipmakers. Various countermeasures against these threats were proposed on the electronic system level. However, addressing all possible attack scenarios requires the design and analysis of bit- and cycle-accurate implementations.

In our paper Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL[^1], we present a novel secure-by-construction RTL design methodology based on a generic information flow tracking infrastructure. The methodology uses formal verification to systematically detect possible leakage paths and to customize the generic infrastructure accordingly for the design. We propose an iterative flow that semi-automatically leads to an RTL design that is guaranteed to be secure w.r.t. transient execution attacks. A case study for the methodology is conducted on BOOMv3, an open-source RISC-V processor with a deep out-of-order pipeline, and the resulting secure RTL design is benchmarked on an FPGA setup. Our design outperforms a design based on conservative countermeasures, improving the incurred overhead by 3X / 4X (depending on the threat model) while maintaining the same level of security.

The Berkeley Out-of-Order RISC-V Processor

The Berkeley Out-of-Order Machine (BOOM) is an open-source superscalar out-of-order core, designed and maintained by UC Berkeley Architecture Research. The core's third major release, implements the RV64GC variant of the RISC-V ISA. The current version of the BOOM microarchitecture (SonicBOOM, or BOOMv3) is performance competitive with commercial high-performance out-of-order cores, achieving 6.2 CoreMarks/MHz.

Spectre-style attacks are possible in BOOMv3 and no mitigation has been implemented yet. With respect to Meltdown, measures have been taken in BOOMv2 to prevent this kind of attack, but have been reintroduced to the microarchitecture as we could show in the course of this work.

Threat Model

Our approach is based on the commonly used threat model for transient execution side channels. The security target is preventing any transient execution side channel from leaking the content of data memory.

This threat model assumes an attacker that can measure the timing of instruction execution with clock cycle accuracy, including the timing of the victim software execution. The victim process has sufficient privilege to access secret data and may transiently execute any instruction outside its correct program flow and later discard the results. The attacker can poison the predictors in order to trick the victim process into executing a specific gadget. This threat model includes any TES attack based on any microarchitectural side channel such as cache side channels, port contention, and data-dependent timing in functional units.

For this threat model, we may assume that the victim does not leak its protected data in the correct program flow under sequential semantics. Hence, preventing attacks enabled by classical side channel analysis, e.g., monitoring the instruction cache footprint of square-and-multiply exponentiation in RSA is not considered in this paper.

Our threat model protects data that resides in the data memory (\emph{data-at-rest}), while any information in general-purpose or control status registers is considered non-confidential. Storing confidential information in the architectural registers must be handled responsibly by the software developer. Physical side channels, such as power or electromagnetic side channels, are also out of the scope of this paper.

To allow for a trade-off between performance and security, we distinguish between two different threat models: spectre and futuristic. The spectre model covers timing side channels caused by control-flow mispredictions, i.e., it only considers instructions after unresolved branch or jump instructions and neglects any other form of transient execution. The futuristic model extends this to all kinds of transient execution and includes prior exceptions, memory consistency model violations, and load/store ordering failures. Such a distinction is helpful for the designer since the spectre model already covers the majority of known Spectre variants and prevents universal read gadgets. Additionally, it allows the microarchitecture to benefit more from out-of-order execution.

SecureBOOM

In this work, we address the challenge of designing secure microarchitectures by a new hardware framework with a generic control infrastructure which is systematically customized in a secure-by-construction design flow to achieve the defined security targets. The proposed flow is an iterative procedure that interleaves design steps with formal verification to create security countermeasures against TES attacks in a semi-automated way. Our design and verification flow pinpoints security issues at the design phase and enables the designer to implement targeted security countermeasures rather than conservative and expensive blanket fixes.

The proposed approach utilizes a generic dynamic information flow tracking infrastructure to detect the flow of information from transiently accessed data, similar to secure speculation approaches such as Speculative Taint Tracking [^5] and DOLMA [^6]. The information flow policy, i.e., when to block the propagation of tainted information is determined based on a formal analysis of the microarchitecture. It replaces the error-prone manual analysis required to implement the existing secure speculation schemes. The formal analysis at the core of the design flow is performed by Unique Program Execution Checking (UPEC) [^2] which identifies TES vulnerabilities in the RTL design. The proposed systematic design flow provides an end product with a well-defined formal security guarantee. More importantly, the formal guarantee enables the designer to adopt more aggressive optimizations without the risk of compromising security because any security violation is guaranteed to be detected in the design flow.

Generic Control Infrastructure for Security

The figure shows how our methodology augments a standard out-of-order execution pipeline with a generic control infrastructure for security. It consists of a generic tainting infrastructure and an information flow controller (IFC).

Generic Tainting Infrastructure

Every register in the general-purpose register file is instrumented with an additional field for taint information. In-flight instructions in the execute stage have an additional attribute for the taint information regarding their destination register. This information includes a single bit denoting the taint which is set and cleared based on taint and untaint rules. These rules rely on the visibility point in the ROB, which is defined as the youngest non-speculative instruction, depending on the threat model.

An unsafe load instruction, i.e., a load instruction that lies between the visibility point and the Re-Order Buffer (ROB) tail, taints its destination register in the register file. Subsequently, any instruction that has a tainted operand sets the taint bit for its destination register. Based on the taint rules, the effect of speculatively accessed data is tracked across the pipeline over the course of instruction execution. For minimum performance penalty, the output of speculative load instructions must be untainted as soon as they are proven non-transient, i.e., when they pass the visibility point in the ROB. This can be challenging to implement, as retracing instruction dependencies through the ROB is difficult. Tracking the youngest root of taint (YRoT), i.e., the youngest instruction that initiated the taint bit, simplifies this problem by removing the chaining of dependencies.

Therefore, the taint information of the register file and of in-flight instructions also have a field that stores an identifier pointing to the YRoT. This identifier, for example, can be the index of the ROB entry for the corresponding instruction. In the case of a load instruction, the YRoT of the destination register is set to the identifier of the load instruction itself. For any other instruction, the YRoT of the destination register is set as the youngest YRoT among the tainted operands. Using the YRoTs, the register file clears the taint bit of any register as soon as its YRoT points to a safe instruction. It should be noted that in this paradigm, the data memory does not need to be tainted manually since any transient memory access is considered confidential information until the load instruction becomes non-transient.

Information Flow Controller

The proposed information flow controller (IFC) selectively inhibits the execution of certain in-flight instructions without stalling the entire pipeline. Its generic structure enables the designer to implement it without any security knowledge. Our iterative design methodology (described in the following section) utilizes the IFC to implement information flow policies in a semi-automated way. This completely relieves the designer from having an in-depth understanding of TES and their microarchitectural implications.

The IFC receives the opcode, ROB index, and taint information of the in-flight instruction in every functional unit. It is equipped with a list of transmitters, i.e., instructions capable of forming a side channel. During runtime, if there is any tainted in-flight transmit instruction, the IFC sends a