μCFI: Formal Verification of Microarchitectural Control-flow Integrity

2024. 3 citations.

Authors

• Katharina Ceesay-Seitz (ETH Zurich): h-index 3; 24 citations; corresponding author
• Flavien Solt (ETH Zurich): h-index 4; 138 citations
• Kaveh Razavi (ETH Zurich): h-index 30; 3,128 citations

Topics

Security and Verification in Computing, Physical Unclonable Functions (PUFs) and Hardware Security, Radiation Effects in Electronics, Computer science, Operand

---

CFI: Formal Verification of Microarchitectural Control-flow Integrity

Flavien Solt ETH Zurich Zurich, Switzerland flsolt@ethz.ch

Kaveh Razavi ETH Zurich Zurich, Switzerland kaveh@ethz.ch

Abstract

Formal verification of hardware often requires the creation of clock cycle accurate properties that need tedious and error-prone adapta tions for each design. Property violations further require attention from verification engineers to identify affected instructions. This oftentimes manual effort hinders the adoption of formal verifica tion at scale. This paper introduces Microarchitectural Control Flow Integrity ( CFI), a new general security property that can capture multiple classes of vulnerabilities under different threat models, most notably the microarchitectural violation of constant time execution and (micro-)architectural vulnerabilities that allow an attacker to hijack the (architectural) control flow. We show a novel approach for the verification of CFI using a single property that checks for information flows from instruction operands to the program counter by injecting taint at appropriate clock cycles. To check arbitrary sequences of instructions and associate property violations to a specific Instruction Under Verification (IUV), we propose techniques for declassifying tainted data when it is being written to registers and forwarded from the IUV through architec turally known paths. We show that our verification approach is low effort (e.g., requires tagging six signals) while capturing all interac tions between unbounded sequences of instructions in the extended threat model of CFI. We verify four RISC-V CPUs against CFI and prove that CFI is satisfied in many cases while detecting five new security vulnerabilities (4 CVEs), three of which are in Ibex, which has already been checked by state-of-the-art verification approaches.

CCS Concepts • Security and privacy → Logic and verification.

Keywords Hardware security; formal hardware verification; side-channels

ACM Reference Format: Katharina Ceesay-Seitz, Flavien Solt, and Kaveh Razavi. 2024. CFI: Formal Verification of Microarchitectural Control-flow Integrity. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS ’24), October 14–18, 2024, Salt Lake City, UT, USA. ACM, New York, NY, USA, 15 pages. https://doi.org/10.1145/3658644.3690344 Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA © 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 979-8-4007-0636-3/24/10 https://doi.org/10.1145/3658644.3690344 1 Introduction With the increasing cost of compromising software due to the plethora of mitigations and security analysis techniques [1, 2, 4, 8, 11, 30, 45, 62, 65, 92, 106, 110], the focus is shifting towards hardware vulnerabilities, highlighting the need for better hardware security analysis [21, 42, 44, 56, 58, 60, 67, 68, 78, 89, 95, 97, 102, 103, 104]. While there are recent advances in the area of hardware fuzzing [16, 17, 19, 26, 48, 54, 55, 59, 87, 94], unlike formal verifica tion, these fuzzers are not complete by design. Formal verification, however, requires significant per-design human effort due to the lack of generic security properties and simple verification meth ods that apply to various hardware designs. This paper introduces Microarchitectural Control-Flow Integrity ( CFI), a generic security property that captures constant-time and control-flow violations at the microarchitectural level and builds a novel approach for for mally verifying this new security property on existing open-source RISC-V CPUs. Hardware verification. To formally verify a hardware design at the Register Transfer Level (RTL), verification engineers often need to specify design-specific (security) properties which can then be evaluated with a model checker. According to a recent study [86], more than half of the human effort in the development of new hardware designs is dedicated to verification, with debugging being the largest effort (47%) during verification. With the increasing pop ularity of open-source RISC-V CPUs, their fast community-driven development cycles, and the increasing number of hardware vul nerabilities, reducing the verification effort is of utmost importance for ensuring reliable and secure CPUs in the future. New security properties that generalize to existing designs have the potential to capture different classes of security vulnerabilities while reducing the verification effort through automation. CFI. We define the microarchitectural control flow as the Pro gram Counter (PC) values at each clock cycle and make a key observation that a single generic security property can capture multiple classes of hardware vulnerabilities, such as constant-time violations or control-flow hijacks. This new property, which we call Microarchitectural Control-Flow Integrity ( CFI), enforces that the microarchitectural control flow is only influenced by instructions for which the Instruction Set Architecture (ISA) explicitly allows a control or data path from their operands to the PC. Data-dependent execution timing of a given instruction causes the PC to have dif ferent values at certain clock cycles, violating CFI. Furthermore, (micro-)architectural vulnerabilities that allow an attacker’s input to directly control the PC also violate CFI. Hence, the verification of CFI captures both classes of security vulnerabilities. CFI verification. Previous approaches that aim to verify the constant-time subset of CFI either require manual extraction of design conditions and specification of candidate invariants [33, 34, 100], or cannot verify the interaction between secure and insecure instructions [33, 34, 35], and neither can provide security classi fications per instruction for unconstrained instruction sequences. Our verification approach aims to address these challenges in the broader threat model of CFI. We make a key observation that CFI can be verified using a single property that checks for all informa tion flows from critical input data, encompassing secret or attacker controlled data, to the PC. By declassifying valid flows through instruction writeback and forwarding paths, CFI can capture in formation flows from instructions to in-flight or future instructions as well. The CFI property can attribute property violations to specific instructions and can check arbitrary and unbounded se quences of instructions, where instructions may operate on any combination of public, secret, or attacker-controlled data. Formal verification of Information Flow Tracking (IFT) proper ties using taint logic has so far been limited to individual modules and properties expressed over interface signals [5, 47, 113]. Leverag ing and extending the state-of-the-art IFT logic, CellIFT [88], com bined with a state-of-the-art model checker [18], we formally verify CFI expressed over CPU internal signals spanning the entire CPU pipeline. We evaluate CFI against four open-source in-order RISC V processors: Kronos [57], PicoRV32 [75], Ibex [49], and Scarv [84]. We automatically (dis-)prove CFI for an unbounded number of clock cycles, and find five new vulnerabilities: two in Kronos that had previously undergone fuzz testing [87] and three in Ibex that had already been extensively verified [34, 35, 50, 100]. Contributions. We make the following contributions:

• We introduce CFI, a generic security property, which enforces that cycle-accurate values of the PC are not influenced by mi croarchitectural data dependencies, except via explicitly ISA specified control or data paths. • We formally define CFI as a generic information flow property. • We develop the first generic and automated verification method for formally proving the CFI property using SystemVerilog Assertions and an existing open-source IFT mechanism [88], reusable across in-order RISC-V CPU designs, and capable of verifying arbitrary and unbounded instruction sequences. • We show that formal verification of cell-level taint tracking can scale to in-order RISC-V CPU designs. We prove CFI or find counterexamples by verifying four RISC-V CPUs. In particular, we find five new vulnerabilities: three in Kronos that had pre viously undergone fuzz testing [87] and two in Ibex that had already been extensively verified [34, 35, 50, 100]. Open sourcing. To the extent that commercial licenses permit, we open-source our toolchain. https://comsec.ethz.ch/research/ha rdware-design-security/mucfi/. The extended version of this paper, including appendices, can be found in [25].

2. Background

We discuss CT and CFI, two generic software security properties (Section 2.1) before providing background on hardware IFT and formal property verification (Section 2.2). We then motivate why microarchitectural security could similarly benefit from generic hardware security properties and their verification (Section 2.3).

2.1 General software security properties General software security properties can protect software against various classes of software vulnerabilities like memory safety [10, 27, 82, 99, 101] and Control-Flow Integrity (CFI) [1, 14, 37, 83]. Some properties like constant-time (CT) programming [2, 3, 43, 70] define guidelines for implementing software that is secure against information leakage through software and hardware. CFI. Control-flow hijacking attacks like ROP [76] or JOP [12] abuse software vulnerabilities like buffer overflows to divert the Control Flow (CF) of programs to carefully picked gadgets that enable attackers to gain complete control over systems [20, 64, 104]. CFI aims to protect systems by enforcing the integrity of the CF of a potentially vulnerable program at runtime [1, 107]. Software CFI mechanisms check the validity of a program’s CF at the ISA level and detect variations when an attacker input influences the CF [64]. Like all software security techniques, CFI assumes hardware to be ISA-compliant. However, the continuous discovery of security vulnerabilities in hardware designs demonstrates the need for hardware-level security verification [44, 64, 68, 87, 89, 95]. CT. Timing side-channel attacks observe secret-dependent pro gram execution times to infer secrets. To prevent such leakages, the CT programming principle states that secret data must not (a) in fluence the control flow of a program, (b) control memory accesses, and (c) be passed to arithmetic instructions with data-dependent execution latencies [53, 61, 69]. A large body of research on for mal verification methods attempts to guarantee CT at the software level [2, 3, 7, 21, 31]. These methods rely on abstract models of the hardware, with the ISA being the formal contract between software and hardware. Intel’s recent announcement of the DOIT mode [52], RISC-V’s Data-Independent Execution Latency (DIEL) mode [81], as well as already-implemented data-dependent optimizations [72, 98] highlight the need for reliable methods for classifying instructions with respect to their CT property at the microarchitectural level.

2.2 Verification of hardware designs Two known techniques for verifying hardware designs against security vulnerabilities are Information Flow Tracking (IFT) and Formal Property Verification (FPV). Information Flow Tracking (IFT). Dynamic IFT, also known as taint tracking, was initially designed for following the propagation of information from (typically) user-defined taint sources to taint sinks through a software program [91]. IFT has been adapted to hardware and used in static and dynamic settings [46]. GLIFT [93] proposes to instrument each logic gate with additional shadow logic, which propagates labels that carry information about whether a signal is affected by the value of a taint source, i.e., if the signal is tainted. RTLIFT [6] operates on the Hardware Description Language (HDL). CellIFT [88] operates at the (macro-)cell level, is open-source, and has been shown to scale to the simulation of complex open source CPUs. Formal Property Verification. Dynamic testing can usually not guarantee the absence of security vulnerabilities because the set of simulated stimuli is rarely exhaustive. Modern model check ers can exhaustively verify a property expressed over hardware design signals, considering all possible input sequences [85] over unbounded clock cycles, using methods like interpolants [66] or in ductive invariants [15]. Logic abstraction can be used to disconnect an internal signal from its driving logic, effectively making it an in put. Design inputs and abstracted signals may be left unconstrained to consider arbitrary values, or constrained to specific sequences via formal assumptions [22, 85]. Scalability remains a challenge, which techniques like abstraction, modularization, and the addition of invariants help to overcome [41, 79]. Model checking can effi ciently find property violations and present counterexamples that demonstrate an input trace that leads to a violation [28]. The state of-the-art SystemVerilog Assertions (SVA) language can express Linear Temporal Logic (LTL) properties, enhanced with sequential regular expressions, but does not define an information flow op erator [51]. Information flow properties are hyperproperties [29] specified over sets of traces. Such properties can be verified with IFT logic [5], miter circuits [33, 34] or self-composition [100]. Man ually writing properties is time-consuming and error-prone. One wrongly specified bit or clock cycle delay could lead to a false proof, leading to wrong confidence in the design’s correctness [23, 24]. Generic and automated formal verification methods can alleviate some of these burdens [73, 74, 80].

2.3 Motivation Software properties like CT and CFI abstract away hardware details and, therefore, cannot consider clock-cycle accurate control flow variations caused by data dependencies. A program may be proven to comply with software security concepts on an ISA-abstracted hardware, while actual processor implementations might under mine these guarantees in many ways [89]. Hence, cycle-granular dependencies must be verified at the hardware level. While formal methods have a long history in hardware verification, completely proving all functional and non-functional (e.g., security) aspects of CPU implementations is often infeasible due to the complexity of the verification problem and the required human effort [38, 79, 85]. Targeted security properties capturing different classes of security vulnerabilities have the potential to increase trust in a hardware de sign even though it is not completely formally verified, e.g., due to high cost. Generic CPU properties make their application practical and low effort. With the ISA being the interface between HW and SW, such properties can provide microarchitectural guarantees at the instruction level. We define one such property and show how it enables automated verification of hardware against microarchi tectural constant-time and control-flow hijacking vulnerabilities.

3 Microarchitectural Control-flow Integrity The (architectural) control flow of a program is defined as the sequence of architecturally-visible program addresses. Given this, we define the microarchitectural CF as follows: Definition 1 ( CF). A Microarchitectural control flow ( CF) is the clock-cycle accurate sequence of program counter values. The difference between architectural and microarchitectural con trol flow is the granularity of Program Counter (PC) changes. The CF affects the clock-cycle-accurate PC valuation, while the archi tectural CF affects the PC value only at the instruction granularity. We posit that the CF can capture behavior relevant to various classes of microarchitectural vulnerabilities. As an example, the Constant Time (CT) programming principle selects a group of instructions from the ISA that a program may use add

CT-veri fi ed program xor add sub or xor sub or clock

Data leak div add or sub div xor jal

Manipulated control fl ow sub

a b

Architectural control fl ow

Microarchitectural view

Architectural view

Figure 1: Examples of vulnerabilities only captured in the microar chitectural view. a Data leak via instruction timing and b an attacker diverted control flow. when operating on secret data [61, 69]. Their timing must be inde pendent of their operand values. In other words, a CT instruction must never influence a program’s execution time depending on its operand values. From the perspective of the CF, the PC values dur ing instruction execution always follow the same pattern for a CT instruction in a given pipeline context, and its operand values do not influence the PC values of any in-flight or future instructions. Fig ure 1- a depicts an instruction sequence that is executed with two different data values for instruction sub. Architecturally, both exe cution sequences satisfy the CT programming principle. However, if the microarchitecture implements data-dependent optimizations (i.e., violating the CT principle), the CF of two executions of the same instruction may differ in a data-dependent manner. Another example is a vulnerability that enables an attacker to hijack program execution in the absence of software vulnerabilities. Figure 1- b shows two instruction sequences, where the div instruc tion takes different values in each of them. In an ISA that specifies no arithmetic exceptions, like RISC-V, a div instruction must never trap, and execution should continue with the instruction at the next program address. A vulnerable processor implementation may trap in case of a division-by-zero and manipulate the trap return address based on an attacker-provided input. In this case, the div instruction may follow a different CF depending on its operand values, leading to a different architectural CF. As we show in Sec tion 7, issues exist in CPU designs that allow an attacker to hijack the architectural CF even if the software is implemented correctly. To capture these differences in the CF, we define a new property called Microarchitectural Control-Flow Integrity ( CFI): Definition 2 ( CFI). Microarchitectural control-flow integrity ( CFI) enforces that the microarchitectural control flow is only influenced by instructions for which the ISA explicitly allows a control or data path from their operands to the program counter. A hardware implementation that satisfies CFI guarantees that attacker-controlled data never manipulates the CF via paths that the ISA does not explicitly allow. Figure 2 shows how CFI relates to existing software security mechanisms. The CT programming model enforces that the architectural CF of the program should not be secret-dependent. If this property is violated on microarchitec tural level, then valid architectural control flows in the program can leak information. The architectural CFI property enforces that the architectural CF of the program should not be manipulated by an attacker outside the valid control flows. Its violation can lead

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA Katharina Ceesay-Seitz, Flavien Solt, and Kaveh Razavi Architectural control fl ow Microarchitectural control fl ow

CF: valid CF: manipulated Information leakage

Code execution

Information leakage

Code execution

CT CFI CFI

CF: manipulated μCF: manipulated CF: manipulated μCF: manipulated

CF: valid

Figure 2: Relating CFI to CT and CFI. CFI provides similar security guarantees for the microarchitecture as CT and CFI do for software. Vio lations of CFI signal timing violations with valid architectural Control Flow (CF) as well as cases where the architectural CF can be hijacked by an attacker due to microarchitectural vulnerabilities. Table 1: Information flows verified by CFI cover four types of infor mation flows and different classes of hardware vulnerabilities. Architectural Control Flow

Input Secret Attacker-controlled Invalid (data flow) Data leak Control-flow hijack Valid (timing flow) CT violation Delay injection to control flow hijacking by an attacker. CFI captures both these properties for a given hardware design at the same time. Note that while CFI does not capture architectural control-flow issues at the functional level (e.g., invalid branch or jump target calculations), it does capture cases where the architectural CF gets compromised via unspecified microarchitectural control or data paths. Further more, violating CFI does not necessarily lead to an architectural control-flow violation (e.g., operand-dependent instruction timing). In the rest of this paper, we present a novel formal verification method that detects the violations of CFI or formally proves their absence automatically by addressing a number of challenges.

4 Threat Model We assume in-order RISC-V CPUs that have not necessarily under gone full formal verification, as is the case for all RISC-V CPUs that we consider [49, 57, 75, 84]. CFI verification considers four types of information flows, each leading to a different class of hardware vulnerabilities, as shown in Table 1. A CF violation occurs when the CPU executes an invalid architec tural control flow due to a vulnerability (first row of Table 1). These violations are the result of functional bugs with severe security im plications. If a CPU bug triggers an invalid CF that depends on secret data, then the attacker can potentially leak the secret data [109]. For example, imagine that a CPU only triggers a spurious exception if an instruction has a certain operand value. Observing the exception allows the attacker to leak the operand value (Data leak). If the invalid CF is caused by attacker-controlled data, then the CPU bug allows the attacker to hijack the architectural control flow, provid ing them with arbitrary code execution (Control-flow hijack). Timing flows can happen even if the architectural CF remains valid (second row of Table 1). In these cases, the information flows are due to timing variations caused by a given instruction provided with different operand values. If the operand is based on secret data, then the information flow through timing results in a CT violation that leaks all or part of the operand value. Alternatively, if the operand value is attacker-controlled, then the attacker can perform Delay injections attacks, potentially compromising real-time systems or causing instruction re-ordering with architecturally-visible side effects [9].

5. Formalizing CFI

We now formalize the CFI property as a Register Transfer Level (RTL) verification problem. Architecturally, the execution time of a program can be measured in instruction retirement counts and in processor clock cycles per instruction [39]. Timing variabilities in the CF caused by structural hazards, external events, immediate values, and data hazards are not data-dependent and, hence, do not reveal information. However, when the actual number of clock cycles taken by an instruction depends on the data values that are or were being operated on, the timing of the instruction, reflected in when the architectural PC is updated, leaks information about that data. Furthermore, if attacker-chosen data is directly involved in the calculation of the next PC, the attacker can influence and potentially hijack the program’s CF [12, 76]. Observation 1. The information flows from instruction’s operands to the PC can capture clock-cycle accurate data dependent timings of instructions, as well as the influence of data on the microarchitectural control flow. We refer to secret or attacker-controlled data as critical data. This observation leads us to define the CFI property as an information flow property from critical data to the PC. There are different cate gories of instructions that may operate on critical data and some may legitimately influence the PC, which we discuss next. Instruction categories. We define instructions as non influencing (ni) when the ISA does not explicitly specify an operand-dependent (architectural) CF manipulation. Arithmetic or logic operations are in this category. We define instructions as control-influencing (ci) instructions if they may only influence the PC via a microarchitectural control path; thus, their operands may only participate in the choice of PC values from a set of otherwise operand-independent targets. For example, operands of branch instructions control whether the branch is taken but are not allowed to change the possible targets, or a load may allow a control-flow transfer to a pre-defined exception handler when its operand is a misaligned address. We define instructions as value-influencing (vi) if the ISA explicitly allows the instruction to manipulate the PC. For example, jump instructions are specified to set the PC to a target depending on its operand and the architec turally known immediate. Therefore, the data dependencies of the PC on these instructions’ operands are not violating CFI. When software deliberately allows attacker-controlled data to reach vi-instructions, it explicitly allows an attacker to influence the CF. Furthermore, under the CT threat model, compliant software must not pass secret data to ci- or vi-instructions, as this would violate CT on architectural level. Observation 2. Instructions can be categorized based on the (dis-)allowed microarchitectural data and control influences of their operands on the PC. ni-instructions must not influence the CF and ci-instruction may only influence the CF via control flows. vi-instructions are allowed to influence the CF via their operands.

arbitrary program length add sub add xor sub or add bne add sub bne add bne sub sub add reset a r b i t r a r y p r o g r a m s

Figure 3: Exhaustively verifying in struction sequences with multiple criti cal ( ) operands. Any instruction can be come the IUV ( ) at any possible clock cycle in which it could read data from the register file.

SRC SINK

SINK

SRC

a b

Figure 4: Handling non causal correlations a by dis connecting SRC to discover a potential information flow b . Arbitrary and interacting instructions. We aim to provide a security classification per instruction with respect to the threat models discussed in Section 4. Classification results should be valid for any program, potentially infinitely long, where any instruction may operate on public, secret, or attacker-controlled data. As shown in Figure 3, we let every instruction become the Instruction Under Verification (IUV) in any position of any instruction sequence start ing from the CPU’s reset state. Attributing property violations to a specific instruction is challenging [35, 100] due to the inherent parallelism of a pipelined CPU and potential data dependencies of the microarchitectural state. Previous work that studied CT vio lations proposed excluding insecure instructions (e.g., branches), which violate the CT property, from the instruction stream, pro viding security guarantees only for programs composed of secure instructions [33, 35]. Real-world programs may interleave secure instructions with insecure instructions that only operate on pub lic data. This seems secure from a software perspective, but due to microarchitectural interactions, an allegedly secure instruction might illegitimately influence an insecure one, even if the latter did not operate on critical data. For example, the add in the first row in Figure 3 may influence the timing or target of a younger ’branch if not equal’, bne, microarchitecturally, hence add is in secure when composed with branches. To obtain guarantees for arbitrary contexts, such interactions must also be verified. To solve this problem, in Section 5.1, we define the CFI prop erty per instruction and operand, where information flows can be verified in isolation, and each violation can be precisely attributed to one instruction in a specific position in the sequence. However, instructions can interact through architecturally known paths, such as the register file and register-address controlled forwarding paths, which should not be flagged as property violations. UPEC-DIT and ConjunCT avoid this problem by excluding CT-violating in structions from the instruction stream, which reduces the security guarantees [33, 34, 35]. CFI solves this problem by formalizing generic rules for declassifying legal information flows between instructions, as discussed in Section 5.2.

5.1 The CFI property We now define a flow operator and then formalize the CFI property. Information flow operator. Equation 1 defines an information flow operator over RTL circuits, which are deterministic finite state machines. Let be a number of clock cycles, with = 0 the cycle in which the design is in its reset state. Intuitively, an information flow from a source (SRC) to a sink (SINK) signal in a logic circuit exists iff there exists a sequence of values of SRC, := ( , ) ≥0 where a change in at least one bit of a value , of SRC values causes a change of at least one bit of the corresponding sequence of SINK values, := ( , ′ ) ′≥0. To exclude non-causal correlations between SRC and SINK, as illustrated in Figure 4 (a), where a change in input would affect both SRC and SINK, we disconnect SRC from its driving logic as shown in Figure 4 (b).

Let I := ({0, 1} ) N be the set of infinite input sequences to the design, where is the sum of the bit widths of all design inputs, except for SRC, and N are the natural numbers. There is an infor mation flow for a set S ⊆ I, denoted by , if there exists a sequence := ( ) ≥0 in S, and two (distinct) source sequences := ( , ) ≥0, := ( , ) ≥0 ∈ U that yield different value sequences of as expressed in Equation 1. Like for S, we define U as a subset of ({0, 1} ) N, where is the bitwidth of SRC. We define ( , ) as the sequence of values of SINK given the inputs ∈ S and the SRC values ∈ U. Precise information flow operator: S,U : ∃ ∈ S, , ∈ U | ( , ) ≠ ( , ) (1) For being able to express data flows only, we define a data flow operator in the same way as , but with the restriction that information flows via control wires of the RTL circuit are excluded. We define control wires as the ones that either control whether (time dimension) or via which path (spatial dimension) another signal is updated. As we will discuss in Section 6, an existing IFT method can implement the operator, and we build a new data flow tracking method for implementing the operator.

Preliminary definitions. We define CFI for in-order load-store architecture CPUs with any number of pipeline stages, that load data from memory or a Control and Status Register (CSR) into a General-Purpose Registers (GPR), before an instruction operates on the GPR. We define IW to be a microarchitectural signal that holds the instruction word from which the CPU reads the register addresses O _ 0≤ < needed to read the instruction’s operands from the register file. K is the number of operands of the instruction, e.g., = 2 for a branch. We further define as the signal through which operand ’s data transitions from the architectural state (the register file) into the microarchitecture. Finally, the microarchitec tural PC refers to a register within a logic circuit that fulfills the clock-cycle accurate property ( ) ≥0 = ( ) ≥0, where PA refers to the program address of the currently executing instruction.

Defining the CFI property. Following Definition 1 (Section 3), we define the microarchitectural control flow CF as a potentially infinite sequence of PC values: CF := ( ) ≥0. Intuitively, the CFI property states that an ( ) never influences the PC via its operands , and that a ( ) only influences the PC via control flows. Following Definition 2, CFI does not consider instructions given ISA-specified data flow from their operands to the PC. A CPU implementation satisfies CFI if it satisfies the CFI property for all instructions that it supports, and for all microarchitectural states : or xor sub decode instr. execute instr. xor blt blt

Ok

A

Ok

B 1 5 6 8 2 2 7 7 PCA 80 84 88 20

or xor sub xor blt blt

Ok A =

Ok B 80 84 88 20 add

a b

add add add

PC 80 84 88 24 80 84 88 20 B

add 1, 2 blt 6, 20, label xor 2, 4 sub 7, 3

Ok

A add 5, 2 blt 8, 20, label xor 2, 4 sub 7, 3

Ok

B

Assembly example for a time

Figure 5: Precise taint injection. a : Wrong classification: Both add and blt read different values (purple background) in sequences and .

Information flow ( ) to the PC is wrongly attributed to the add (the IUV ( ) in this example, marked with a bold border). b : Correct classification: Input sequences to are constrained ( ) to be equal between any two sequences compared in one proof whenever is not read by the IUV.

CFI property:

∀ , ∀ :

( ( ) =⇒ ¬({ } ∈ V,O )) ∧ ( ( ) =⇒ ¬({ } ∈ V,O )) (2) where V ⊆ I is the set of input sequences that lead to IW equaling IUV’s type at a given clock cycle, and O is the set of source value sequences passed to . Precise taint injection. By the definition of and , must be disconnected from its driving logic, allowing all value sequences to be considered. If two different sequences of can lead to a different value of the PC, then there exists an information flow. Considering the example instruction sequence in Figure 5, if verify the CFI property without further constraints for , any instruction in that sequence that can read from could potentially cause a property violation. Branch instructions, for example, by definition, influence the PC. When considering unconstrained and infinite input sequences, every possible sequence may be extended by a branch and thus, an information flow from to the PC would be detected. However, in Figure 5, our current IUV is the add, so we are not interested in detecting the flow originating from the subsequent ’branch if less than’, blt. Therefore, while verifying the add, instead of excluding branches from the instruction sequence, as done by [33, 34, 35], we constrain the proofs to only consider dif ferences among any two considered sequences to when the add can read from , while verifying every possible input sequence. In Figure 5, case a exemplifies two differing input sequences to , where both add and blt read unconstrained data. They cause a different PC value afterthe blt is executed. However, in this example, we were verifying the add and would, therefore, wrongly associate the blt’s information flow with the add instruction. For precise instruction classification, we constrain O per proof as described in Definition 3 and depicted in b . No change in input sequences to causes a different PC value when verifying the add. When, in a separate proof, the blt is the IUV, a difference at the PC can be observed, and it must have been caused by the blt’s operands. Taint injection constraint. To associate a register access with an IUV, we leverage the fact that the register address is part of the instruction word and that it must be read no later than its use to access the register. We define as a clock cycle in which the register address O _ is read from the instruction word register input forwarded input destination address forwarded input instruction result register input destination address without declassification

20

IW

2 3 4 a instruction result 10 15 5 x x x 1 2 3 20

add div

O2 addr. O2 sub

PC 80 88 92

2 3 4 d 10 15 5 20 10 x x x 15 1 2 3 20 10 15 sub add div

80 88 92

2 10 20 x

1 20 sub

80

3 4 15 5 10 x x 15 2 3 10 15 div

88 92 add

b 2 3 4 10 15 5 20 10 x x x 15 1 2 3 20 10 15 sub add div

80 88 92

-x 15

7 5 bne μ

20 with declassification

c

time

IW

O2 addr. O2

PC

15

10 10 15

Figure 6: Same instruction sequence, different IUVs ( ). a : Informa tion propagates between instructions through architecturally legal paths (instruction result to 2, which reads from register or forwarded input). b - c : With legal paths declassified, flows can be associated with the caus ing instruction. d : Unexpected flows from add to a bne (here with public operands) are not declassified and thus detected.

IW. Next, we define | ≤ as the next clock cycle in which is read from the register file. Finally, we define | < as the next clock cycle in which is overwritten. Intuitively, Equation 3 states that O and O may only differ when the IUV can read from . Instruction Operand Constraint (IOC):

V, O := { , , | = ∧ ∀ ∉ [ , ) , O , = O , }

(3)

The IOC isolatesthe verification of information flowsso that only one instruction type can operate on secret data in any sequence. Section 6 shows how our verification method captures information flows from multiple instructions when verifying them individually. Note that when the IOC forces the SRC ( ) signals to be equal in some cycles, we do not consider reconvergent flows to the SRC in these cycles. However, when the SRC signals only read from declassified paths (see next) we do not need to check these flows.

5.2 Declassification of legal flows By definition, information propagatesfrom an instruction’s operand to its outputs, i.e., the destination register and register address controlled forwarding paths. Information furhter propagates to a subsequent instruction that operates on the previous instruction’s destination register, which is an architecturally known path. For example, in Figure 6- a , the IUV is a sub. This instruction does not influence the PC, but it passes its result to the subsequent add (via ‘register input’), which passes its result to the div (via ‘forwarded in put‘). Without declassification, the div’s potential influence on the PC would be detected when verifying the sub. When considering un constrained instruction sequences, any sequence could be extended with an insecure instruction that receives information from previ ous instructions via such paths. This architecturally expected inter action between secure and insecure instructions complicates the 0 PC

1

S0 fmuxlk

0 1 S0

mux

PC+4 forwarding condition

frlk filk instr. result fom

REG Writeback stage

Execution stage Decode stage declassification x

Ok

Figure 7: Declassification and detection via forwarding paths. When only monitoring information flows from (cyan), flows from forwarded input, , to the ’th forwarding multiplexer, , for operand (red), are missed due to the declassification of forwarded results ( ).

association of an information flow with a specific instruction. Previ ous CT verification methods avoid false classifications by restricting the verified instruction sequences by excluding CT-violating in struction types [33, 35], which limits their guarantees to programs composed of secure instructions only (e.g., containing no branches). In our threat model, the software is responsible for architectural information flows, e.g., from an instruction’s input operands to its results. Hence, we declassify information flows via architecturally specified paths during verification, and prove CFI per instruction type. The IOC constrains the input sequences to pass differing inputs to only one IUV per verified sequence, while it can be sur rounded by arbitrary instructions of the same or different types. b and c show the same instruction sequence as a , but with architec tural paths (through registers and forwarding paths) declassified. Thus, the div’s CT violation does not get detected when verifying sub ( b ), but when verifying div ( c ). Unexpected paths between instructions, like depicted in d , are not declassified and are de tected. Since the CFI property (Equation (2)) is proven for every IUV and every microarchitectural context , every instruction in every sequence is considered as IUV in some proof scenario. Declassification Precondition. Declassification is sound if no unexpected information flows to the PC could have been missed when CFI is proven. This is guaranteed iff the following precondi tion is proven on a design: all outgoing paths from a declassified signal converge either into another declassified signal or one of the SRC inputs to instructions before reaching the PC. This precondi tion ensures that there are no unconsidered information flows in the fanout of declassified signals. Declassification of register writes. We declassify data written to the destination register of an instruction by disconnecting the register data write signal from its driving logic and adding it to the input sequences in V, allowing the signal to take on arbitrary values that are never influenced by a change in . Declassification of forwarding paths. CPU implementations can forward instruction results to younger instructions in vari ous pipeline stages. As depicted in Figure 7, we define forwarding multiplexers as the ones that arbitrate between forwarded data inputs and register data , selected by a condition over matching dependent register addresses between instructions (forwarding condition). is the number of forwarded inputs per operand (typically present at the input of the execution stage).

Processor design CellIFT

IFT/DFT instrumented processor designs

Signal names

Formal testbench General properties, assumptions, tasks

Taint Condition

Formal model checker Proof Counter-example

CellDFT

Taint conditions

Yosys Passes

New Existing CPU specific

User input

Figure 8: CPU-specific formal verification flow.

Forwarded output data are the signals that convey instruc tion results via forwarding paths. is the number of forwarding outputs, e.g., in the execution or writeback stage. To avoid falsely attributing a property violation to an insecure instruction that reads an older instruction’s result via forwarding paths, we declassify forwarding output signals, , by disconnect ing them from their driving logic and adding them to the input sequences V. Since an IUV can operate on forwarded data inputs , forwarded data must not influence the CF in unexpected ways. It is possible (although unexpected) that an instruction’s operand only influences the PC if the instruction operates on for warded data , and not if it operates on register data , e.g., as exemplified in Figure 7. When only monitoring data coming from the register, REG, the information flow from to the PC would be missed in the scenario shown on the left. Therefore, we add inputs to the SRC signals by disconnecting them from their driving logic and extending the IOC constraint as follows, with F being input sequences to :

V, O , F := { , , , , | ∧ ∀ ∉ [ , ) , , = , }

(4) 6 Verifying CFI We now present how to express CFI as RTL design properties using SystemVerilog Assertions (SVAs), logic abstractions, and the bit-precise cell-level IFT [88]. These properties can be verified with any standard model checker that can obtain unbounded proofs for SVAs [18]. First, we prove that cell-level IFT equals the information flow described by the operator defined in Section 5.1 (Sec tion 6.1). We then introduce a new IFT mechanism that only tracks data flows, called CellDFT (Section 6.2). Finally, we describe how to construct the CFI property in an SVA testbench (Section 6.3) and how to declassify legal flows (Section 6.4). Our tool flow, depicted in Figure 8, starts with processing a CPU design with three Yosys [105] passes: (i) obtaining the taint condi tions (Appendix A.3 in [25]), (ii) cell-level IFT (CellIFT) based on previous work [88], and (iii) CellDFT. The IFT and DFT instrumen tations add shadow taint logic to the design. The flow generates a CPU-specific testbench connecting generic SVA assumptions and assertions with the generated CPU-specific logic conditions. Names of the following signals, which can be identified based on their properties (see Section 5.1), must be user-provided: PC, IW (and register address), signals connected to the read/write port of the register file, and forwarding outputs.

6.1 Modelling information flows with CellIFT CellIFT [88] defines IFT logic on the cell level but does not specify information flows over spatial and temporal compositions of cells. We prove that if there is an information flow from a source to sink according to Definition 1, CellIFT will propagate taints from the source to the sink. The cell-level information flow rule [88] is given as ( , ) = 1 ⇐⇒ ∃

˜ | ( ⊕ ˜ ) ∧ = 0 and (

˜ ) = () , where I is a cell’s input, its corresponding taint input, C(I) the cell’s output, and () its corresponding taint output vector. refers to the -th bit of the (taint) output vector. CellIFT instruments designs by adding a so-called shadow logic. Each state bit in the original design is augmented by one state bit in the shadow logic. The shadow logic is designed to convey information flows, i.e., to propagate taints if changes in the tainted input bit values can provoke changes in the output bit values. If there is an information flow from a SRC to a SINK as defined in Section 5.1, then CellIFT propagates the taint from SRC to SINK, as expressed by Theorem 6.1 proved in Appendix Bin [25], where I and I are the sets of input sequences to bits of which the corresponding bits are 1 and 0, respectively and Y is a cell’s output. Theorem 6.1. Single-cell CellIFT equivalence. = 0 and I ,I ⇐⇒ ( , ) ≠ 0 (5) Oberg et al. [71] showed that taint tracking methods detect tim ing dependencies. We prove in Appendix Bin [25] that CellIFT covers all information flows at design level, i.e., that CellIFT has no false negatives. However, false positives are theoretically possi ble [88].

6.2 Data flow tracking with CellDFT Implementing the operator requires distinguishing data and control flows. CellIFT is incapable of it. Yet we observe that the macrocell abstraction level (used by CellIFT) is suitable for making this distinction. We introduce CellDFT, a variant of CellIFT that propagates information via data flows only. It expresses data flows by blocking taint propagation via control paths, which we define as paths from a cell’s input to its output, that do not perform direct assignments or data-manipulating operations. Control paths are for example paths through comparison results, multiplexer select signals or enable bits, which all control state changes or data flows. CellDFT is a more restrictive variant of CellIFT in the sense that any signal tainted by CellDFT would also be tainted by CellIFT. In the following, we describe the variations from CellIFT that describe CellDFT, which we define in Table 2 and describe below. We have implemented CellDFT as a modified version of the CellIFT Yosys pass and will release it as open source. State elements with enable condition. We let ( )0≤ < denote the enable condition expanded to the bitwidth of the output vector of the cell, where ∀ ∈ (0 ≤ < ) holds = . is the input data vector. Intuitively, there is no data flow coming from the enable signal. 2-input multiplexers and aldff cells [105]. Let S be the bit expanded select signal (like EN above), with same bit length as Y. Let A and B the selected signals when S is 0 or 1, respectively. Intuitively, there is no data flow coming from S.

Table 2: Cell definitions for CellDFT CellDFT’s version of CellIFT rules (where modified), specified over Yosys’ cell port names. EN, D, A, B and S are cell inputs, is a state cell output at clock cycle n, is a combinational cell output, ◦ represents shift operators. Cell Name Definition

State elems. with enable ( ) = ( ∧ ) ∨ (¬ ∧ −1)2-input mux, aldff cells [105] = (¬ ∧ ) ∨ ( ∧ )pmux cells [105] = [ ]Comparison/reduction cells = 0 Shift cells = ◦ pmux cells [105]. Yosys implements multiplexers with multiple inputs [0] , . . . , [ − 1] as pmux cells. The output taint corre sponds to the taint of the selected input. Comparison and reduction cells. This rule describes the fol lowing single-output-bit cells: eq_ne, ge, gt, le, lt, logic_and, logic_or, logic_not, reduce_and, reduce_xor. None of them propagates data. Shift cells. We let A denote the data input and B the shift amount. Let ◦ denote the cell’s operator. Intuitively, the shift amount is not part of the data flow, but controls A’s data flow.

6.3 CFI expressed over taint logic We now formulate the CFI property stated in Equation 2 as SVAs [51, 85] over a CellIFT-/CellDFT- instrumented design. Formal setup overview. A SystemVerilog bind statement inserts SVA assumptions and assertions into the CPU’s top module. We abstract [85] the memory so that the CPU receives unconstrained and infinitely long instruction sequences (including illegal ones) via its instruction word input. We leave all original design inputs un constrained, which models arbitrary external interrupts, bus errors, etc [22]. Definition 1 requires that the information source (SRC, i.e., ) is disconnected from its driving logic. Using the taint tracking logic, we only abstract the taint signal of , while leaving the de sign signal untouched. This models unconstrained inputs, because taint propagation is symbolic, i.e., design bit values, of which the corresponding taint bits are set, are not influencing the taint propa gation [88]. Furthermore, we constrain all taint input signals at the top level to constant zero during the whole proof. This guarantees that the operand data is the sole taint source. We constrain the taint source as described in Section 5.1, for automatic identification of a specific instruction and operand combination as root cause of the CFI property violation, without needing further analysis or hu man interpretation as is often the case [34, 35, 100]. We implement declassification of valid flows as defined in Section 5.2 and state the CFI property as an SVA assertion regarding the PC’s taint. In the following we detail these steps. Taint injection location In Section 5.1, we defined as the signal through which register data passes first when entering the microarchitecture ( could be the same for all operands). Figure 9 categorizes cases of interfacing with the register file (REG). In 1 , is a microarchitectural state element that is directly connected to the REG’s read port, but is updated only when its enable condition is true. 2 refers to all cases where may read from REG via some logic cell. Here, may be a wire or a state element. Finally, 3 refers to cases where reads from REG unconditionally, i.e.,

REG Ok

0 1 S0

mux Ok

REG

S/fom

REG Ok reg. read

3 1 reg. read Figure 9: Taint injection through . In 1 , reads from REG condi tionally. In 2 , reads from REG via some cell, e.g., via a multiplexer that arbitrates between REG and any other signal "S" (e.g. ). In 3 , reads from REG unconditionally.

bne bne clock

IW reg. read

Signal names add xor taint start taint stop

op1 data A B I 0 I op1 addr. 1 2 3 add1 xor A B I 0 I 1 2 2

add1

A B I I 1 2 2

bne xor

1 2 3

Figure 10: Taint injection examples. Corresponding taint start and stop cycles are drawn in equal line color. Taint injection windows start (e.g., blue taint start) in every clock cycle in which IW matches IUV’s ( ) type and IUV reads (reg. read high) from the register file (blue/green background) through (op1 data), and stop (e.g., blue taint stop) with the next clock cycle after taint start in which may change. 1 : Two reads per IUV, 2nd one e.g., due to writeback (green background). 2 : is invalidated (orange background) after the read. 3 : Since every clock cycle where IW=xor is a taint start and stop condition, there is one taint window per clock cycle. either continuously if it is a wire or in every clock cycle if it is a state element. Temporal aspects of taint injection. Following the formaliza tion in Section 5.1, and in particular the IOC defined in Equations (3) and (4), we verify CFI per instruction and operand and let any instruction become the IUV at any possible clock cycle in which it could read data from the register file. In the formal testbench, we sample the instruction word signal IW in the same condition in which the CPU reads the register address from it. This condition models , and we can extract it automatically as discussed in Appendix A.3 in [25]. We associate any register read with the latest sampled instruction. Whenever at the same time a register reading condition happens, and IW holds an instruction of the currently examined type, this instruction turns into the IUV, and the reading cycle becomes (i.e., a taint start signal is set), taint is injected into the abstracted taint signal of . A register reading condition is any condition in which can read the latest value of REG. Note that the register reading condition does not depend on the actual value change of , i.e., a new taint window also starts in case an instruction reads from the same register address as the previous one or if the values in two consecutive instruction’s input registers match coincidentally. Figure 9, cases 1 and 2 have a dedicated read enable signal. In case 3 , the reading condition is always true when IW matches the IUV’s type, as reads from REG unconditionally. We stop taint injection any time ’s value may change again, i.e., in any clock cycle in which is not updated with its own previous value. Note that the taint stop condition is also true when a signal is overwritten with the same value as its previous one, e.g., if a register is updated to an instruction’s result that coincidentally matches the previous register value. This taint stop condition models . Examples of taint injection. Figure 10 shows an example of taint injection for each of the three cases when reading registers. Taint start and stop signals of one injection window are shown in matching line colors. Example 1 shows an add that reads from register 1 two times. The second read (green background) could happen if the add was stalled and register 1 is updated due to a writeback. The IOC constraint considers both reading conditions, each being a taint start condition for an individual taint injec tion window. Hence, the first read’s taint stop condition overlaps with the second read’s taint start condition. In Example 2 , is overwritten with non-register values (orange background) after the first read. In this case, the taint stop condition is true, but no new taint start condition happens. In case 3 , the taint start (and taint stop) condition is true in every clock cycle in which IW matches the current IUV’s type, meaning that a taint flow originating from all of these cycles is verified (individually). Discussion. In Figure 9, case 2 , unexpected taint flowing to S cannot propagate further, because ’s taint signal is abstracted, which means that the logic between S and is ignored in the proof. To avoid missing flows, we check that is only driven by declassified flows by either choosing the REG’s output port as or by ensuring that the only cell between REG’s output and is a forwarding multiplexer through which we inject taint as well (Section 6.4). If an instruction mistakenly would not read any data (e.g., due to a pipeline flush) the CFI property would trivially hold. Automated taint injection. We control the taint source with a generic set of SVA assumptions detailed in Appendix A.2 in [25], to which we pass the signal names, the register reading condition and the taint stop condition. In Appendix A.3 in [25], we detail how we automatically extract these conditions from CPU designs via static design analysis. That way, we do not rely on fully verified CPU functionality as previous work [100], or detailed design knowledge as [33, 100], but rather track data whenever the CPU under verifi cation in its current state of implementation can let architectural data enter the microarchitectural world. Information flow detection. A CPU design can store the PC in multiple pipeline registers. An appropriate taint sink is one that holds the current PC for every instruction, e.g., one passed to the execution stage. Since tainted data must never reach the PC, we can prove the absence of information flow unconditionally by asserting that the taint signal of the PC is always zero. Since the property is proven in an isolated environment per instruction and operand with the operand as the only taint source, a violation is directly attributable to this instruction and operand combination. A proof of this property guarantees CFI for the same combination. From individual to full proofs. In Appendix A.1 in [25], we prove that if a set of inputs and input taints results in some output bit being tainted, then all but one tainted input bit can be untainted while preserving the output bit taint, given a well-chosen valuation of the design bits of which the corresponding taint bits were previ ously tainted. Given this property of CellIFT, it is sufficient to prove CFI for all sequences in which one IUV could have read tainted data to guarantee CFI for all other sequences in which the IUV may be interleaved with any other instructions that may operate on untainted (public), or tainted (secret or attacker-controlled) data.

6.4 Declassification of legal flows In Section 5.2, we defined which information flows are legal within our threat models and explained why they need to be declassified. In the formal verification setup, we declassify flows by abstracting the taint signal of a chosen design signal and constraining it to zero with an SVA assumption. As mentioned in Section 5, the declassification precondition must be satisifed per verified CPU design. Register file. We declassify data written to the register via a signal REG_WRITE_DATA that is directly connected to the register write port. Checking the functional correctness of register writes is out of the scope of CFI verification. The declassification precondi tion is guaranteed if register write data can only propagate to the signal connected to the register read port, which is our taint source. Forwarding paths. Recall that the forwarding outputs for ward instruction results to earlier pipeline stages, and are the forwarded and register inputs to an instruction, respectively, and selects between the two. Our tool takes user-provided signals for declassification and checks that all of their fanout logic feeds into or REG_WRITE_DATA signals. If we then consider all as additional taint sources to the IUV, the declassi fication precondition is fulfilled. Constraining taint of forwarded inputs. To avoid having to identify all clock cycles in which an instruction can operate on in different pipeline stages and to keep our method generic across CPU designs, we let the IUV operate on in the forwarding cases by abstracting and unconstraining the ’ select signals, while the corresponding taint signal remains unchanged, and keep as the only taint sources. However, although register data can reach when the forwarding condition is false, it might not reach it in the forwarding case. Therefore, we extend the IOC (Equation (4)) with the following: V,O , F := { , , , , | (6) ∧ ∀ ∈ [ , ) | , ≠ , =⇒ , ≠ , } Intuitively, this equation states that whenever an instruction can read from , if is tainted, also is tainted. Taint reachability condition: This is guaranteed, as we show in Appendix D.1 in [25], if we can prove per verified CPU that is an unconditional and undelayed assignment from , or, if there is a cell on the path from to , it is another that fulfills the same condition. Lastly, if we inject taint not directly into the register reading port but into (to account for potential conditional reads), the declassi fication of the shown in example 2 of Figure 9 would happen (structurally) before . Therefore, if there is an between and REG, where equals REG, the taint start condition has to be extended by the case where reads from . Automated declassification. Our Yosys pass automatically ex tracts select signals via static design analysis, based on the user provided signals. It verifies the declassification pre condition by traversing all outgoing cell connections of until reaching an , or a declassified signal, and checking that the user provided PC signal has not been passed. It further checks the taint reachability condition and informs the taint condition gen eration about additional before .

Table 3: Design complexity comparison of the uninstrumented (U), CellDFT- (D), and CellIFT (I)-instrumented design considering nets, gates, and register (R.) bits. All values in thousands (k). Design Nets [k] Gates [k] R. Bits [k] U D I U D I U D I Kronos 1.4 3.0 6.8 13.0 43.4 77.1 2.0 3.9 3.9 PicoRV32 1.6 3.8 9.5 27.0 67.6 114.3 3.2 5.1 5.3 Scarv 6.7 11.5 30.1 58.7 176.6 309.3 2.3 4.6 4.6 Ibex (small) 4.5 8.0 17.5 39.9 82.5 160.5 2.4 4.7 4.7 Ibex (custom) 4.6 8.5 18.3 40.7 86.2 166.7 2.5 4.9 5.0 7 Evaluation We evaluate the proposed CFI verification method in terms of runtime and verification results for four open-source RISC-V de signs. PicoRV32 [75] (f00a88c3) is a size-optimized CPU written almost entirely in one Verilog module. Kronos [57] (a41629d) is a CPU designed for FPGA applications, written in SystemVerilog. For PicoRV32 and Kronos we verify CPU versions with fixes for bugs found by the state-of-the-art Cascade CPU fuzzer [87]. We also include Scarv [84] (bb52627) which is a side-channel hardened CPU implementing the RISC-V scalar cryptography extensions [81], and Ibex [49] (bbb91c56, opentitan fork), an extensively verified CPU [34, 35, 50, 100, 112] used in real-world designs such as the OpenTitan root of trust [63]. Testbed. We formally verified the SVAs with Cadence’s Jasper Formal Property Verification (FPV) App, v2022.09 [18], configured to provide proofs for an unbounded number of cycles, executed on a server with the following configuration: Intel Xeon, 3.4 GHz, 60 logical cores, 1.25 TB RAM. Cost of instrumentation. While CellIFT is designed to have a small performance and area overhead [88], its overhead in terms of netlist composition has not yet been extensively studied. Table 3 reports design complexity statistics. The instrumentation multiplies the number of nets by a factor 4.0 (Ibex small, secure) to 5.9 (Pi coRV32). The number of gates is multiplied by a factor of 4.1 (Ibex small, secure) to 5.9 (Kronos). CellDFT only adds a net and gate overhead of max. 2.4x (PicoRV32) and 3.4x (Kronos) respectively. The instrumentation serves verification purposes only and is absent in physical CPU implementations; hence, area overheads are not relevant in the verification context. CellIFT logic added a larger gate overhead to Scarv despite similar state bit counts to Ibex, which explains the larger proof runtime on Scarv. Annotation burden. 6 signals need to be manually extracted from all CPU designs, based on their mentioned properties in Sec tion 5.1 and Section 6.3: IW, one register address, signals connected to the register read and write ports and the PC. Forwarding output annotations depend on the number of pipeline stages that forward results: 0 for PicoRV32, 1 for Ibex and 0 for Kronos, because it reuses the register write signal. Scarv has wider outputs for cryptogra phy instructions, which adds 5 annotations. For the forwarding declassification precondition check the name of the register file is needed.

7.1 Verification runtime The generation of taint conditions, discovery of multiplexer select signals and the declassification precondition check are implemented

Table 4: Verification runtime (MM:HH:SS) for all four considered RISC V CPUs. (I = CellIFT, D = CellDFT, t. = time, c = custom, s = small). Ibex configurations: secure + slow multiplier. ↰Method / Design → Kronos PicoRV32 Ibex (s) Ibex (c) Scarv I Mean t. FAIL 0:00:37 1:05:47 2:25:22 3:18:06 0:10:56 Mean t. PROVE 0:16:29 16:55:43 6:14:33 8:46:12 14:16:56 Max. t. PROVE 0:29:19 21:42:28 7:15:27 11:01:26 23:58:31 Peak memory [GB] 22.9 126.9 63.0 64.0 77.3 D Mean t. FAIL 0:00:15 0:08:29 0:03:04 0:06:14 0:34:20 Mean t. PROVE 0:00:30 0:08:22 0:04:35 0:10:05 0:50:50 Max. t. PROVE 0:00:58 0:19:07 0:09:01 0:15:30 1:27:31 Peak memory [GB] 4.6 37.6 12.0 20.7 36.7 as Yosys passes and Python scripts, which complete in less than 5 minutes per verified CPU. Table 4 summarizes the verification runtimes with CellIFT and CellDFT. For a fair comparison, we verify all RV32I instructions for both versions and report the mean time over all assertion failures, as well as the mean and maximum time over all instructions that were proven. Aggregated runtime and peak memory usage numbers are based on the reports produced by Jasper FPV. The results are for unbounded proofs over unrestricted instruction sequences. All other top level inputs are unconstrained as well, except on Kronos (see below). CellDFT is significantly faster than CellIFT, due to the lower instrumentation cost. Due parallelization the actual total runtime was much lower than the aggregated one. Initially, for Scarv, the Jasper FPV did not produce results after 24 hours. We then chose Jasper’s engine modes M, N, AM and Mp, because they can exchange proof results. For Scarv we also included Ht. For each taint logic state we added a helper assertion stating that the state never gets tainted. The formal tool may use their results as invariants [24]. Together with these assertions, the CFI property could be proven in the reported time. We extended our tool flow to generate these supportive assertions automatically with a Python script after obtaining the taint state signal names from the Yosys CellIFT pass [88]. For a fair comparison, we add these assertions to all cores. However, they do not always improve the runtime.

7.2 CFI violations in existing hardware designs Table 5 shows satisfaction (✓) and violation (✗) of CFI per CPU and instruction, which we will discuss in detail next. Instructions are grouped per category defined in Section 5. Non-influencing (ni) instructions are verified using CellIFT. Control-influencing (ci) instructions are verified using CellDFT. vi instructions are specified to influence the PC, thus their information flows do not violate CFI. However, our toolchain is able to check for their operand’s information flows and confirms a data flow to the PC using CellDFT. Most instructions provably satisfy CFI. We also show CellDFT results for instructions that fail using CellIFT. If proven with CellDFT, these instructions are not causing CF violations. While we are the first to study CFI violations, Scarv and Ibex (in small configuration) were previously verified for CT violations. Besides confirming known vulnerabilities, we discovered five new vulnera bilities. In the following we discuss our newly discovered security vulnerabilities and reference the corresponding GitHub issues and newly assigned CVE numbers.

Table 5: CFI results per instruction grouped by instruction category (ni, ci). CFI satisfactions are marked with ✓, violations with ✗. Ibex (custom config.) results are for non-secure / secure mode with IUV started in data independent timing mode and slow multiplier. ni instructions that violate CFI with CellIFT (I) are checked with CellDFT (D) as well. ci instructions are only verified with CellDFT. = operand k. Instruction Kronos PicoRV32 Scarv Ibex ni I add, and(I), or(I), slli, slt(u), srli, srai, sub, xor(I)

✓ ✓ ✓ ✓

I sll, sra, srl ✓ ✗ ✓ ✓ D sll, sra, srl ✓ ✓ ✓ ✓ I slti(u), addi ✗ ✓ ✓ ✓ D slti(u), addi ✗ ✓ ✓ ✓ I O1: div(u), mul(h), mulhsu, mulhu, remu – ✓ ✓ ✓/ ✓ I O1: rem – ✓ ✓ ✗/ ✗ D O1: rem – ✓ ✓ ✓/ ✓ I O2: div(u), mul(h), mulh(s)u, rem(u)

– ✓ ✓ ✗/ ✗ D O2: div(u), mul(h), mulh(s)u, rem(u) – ✓ ✓ ✓

I lb(u), sb ✓ ✓ ✗ ✓ D lb(u), sb ✓ ✓ ✓ ✓ I Scalar crypto – – ✓ – ci D lh, lhu, lw, sh, sw ✓ ✓ ✓ ✓ D beq, bge(u), blt(u), bne ✓ ✓ ✓ ✗ Listing 1: CFI violation through data dependency.

load program address into general-purpose register x8 0 x800001F8 : lui x8 , 0 x80000 0 x800001FC : addi x8 , x8 , 0 x400 0 x80000200 : csrrw x0 , mtval ,x3 # legal instruction 0 x80000204 : (il) legal instr # arbitrary instruction 0 x80000208 : addi x6 , x8 , 0 x3050 # CFI tracks data operand 0 x8000020C : (il) legal instr ... # trap can steer the control flow to attacker-chosen value 0 x80000400 <trap_handler >: 0 x80000400 : ...

7.2.1 Kronos: Kronos does not implement the RISC-V M exten sions; therefore, these instructions are marked with ’-’. Kronos: Control-flow hijack (CVE-2024-44927) - Issue 17. If Kronos is integrated with a memory that does not always acknowl edge requests in the next clock cycle, there are cases where a ’jalr’ or branch instruction reads from the previous instruction’s input regis ter. If the previous instruction was operating on attacker-controlled data, an attacker can hijack the CF. If that data was secret, it would be leaked by the data-dependent CF deviation. Therefore, without input constraints, CFI was violated for all instructions. Kronos: Control-flow hijack (CVE-2023-51973) - Issue 12. We further verified a setup with ’data_ack’ and ’instr_ack’ inputs constrained to be always high. Table 4 and Table 5 show results with this setup. These constraints model fault injections on the bus, or a memory that does not comply with the pipelined Wishbone protocol. We discovered a control-flow hijack vulnerability, where a data operand of an addi, slti or sltiu could be directly copied into the mtvec CSR, which is the machine trap-vector base address. On RISC-V, by default, all traps are handled in machine mode. Such vul nerabilities allow attackers with only user-mode access to influence the architectural CF in machine mode.

Listing 1 shows assembly code replicating a counterexample re turned by Jasper FPV for the addi instruction. The two instructions load a program address into GPR x8. Then, a legal csrrw instruction is decoded, followed by an arbitrary instruction. Then follows an addi, of which the CFI property tracked the data operand. Due to a CPU bug, an internal CSR write enable signal is high when the addi instruction is executed. That signal depends on a CSR decode signal that was earlier set due to the legal CSR instruction. In the example shown, the higher-order bits of the immediate with value 0x305 are interpreted as the address of the mtvec CSR. The value stored in x8 gets stored into mtvec. A subsequent trap can steer the CF to the value chosen by an attacker. Execution will continue at this address in machine mode. This enables, for example, powerful code-reuse attacks [12, 76, 104]. Constraining the formal tool allows obtaining diverse violation traces. When forbidding CSR instruc tions, the bug was not revealed, which confirms the necessity for a legal csrrw instruction to be used together with the malicious addi. UPEC-DIT [34] and ConjunCT [35] could not have found this bug. Kronos: Constant time violation (CVE-2023-51974) - Issue 13. In the same setup with unexpected bus behavior we further discov ered a timing flow from addi, slti, and sltiu instructions, violating the CT principle if the immediate value matched a performance counter address. The performance counter increase takes one clock cycle longer whenever the upper word of the counter needs an increment. When using input assumptions to model one specific scenario where a memory always responds within one clock cycle, all instructions satisfy CFI on Kronos. If these memory interface assumptions can be proven in the integration setup, Kronos can be trusted to be free from CFI violations. 7.2.2 Ibex: Table 5 shows results for a custom Ibex configuration with writeback stage and branch predictor enabled (see Appendix C.1 in [25]). On Ibex, multiplications and divisons were known to be non-CT in its small, non-secure configuration [34, 35, 100]. However, previous methods did not discover the CT violations caused by div/mul-type instructions that we discuss below, even though they affected the small configuration. Table 5 shows results for a custom Ibex configuration (see Appendix C.1 in [25]). None of the earlier methods tracked data flows; hence, none of them could have detected the control flow violation caused by branches. Ibex: Data leakage (CVE-2024-28365) - Issue 2144. Ibex reacts to an external memory data error signal, even if it has not started a memory operation. This caused CFI to fail for rem, operand 1. While investigating, we discovered a data leakage to arbitrary architectural registers. The underlying bug in the multiplication and division state-machine was fixed by the maintainers of Ibex. Ibex: CT violation - Issue 2144. Operand 2 of div/mul-type in structions that were executed in Ibex’ data-independent timing (dit) mode can influence the timing of younger instructions, which are executed after data-independent timing mode is disabled via a csrrw. UPEC-DIT [34] and ConjunCT [35] cannot find such violations be cause a csrrw is required to trigger them, which is an instruction that these methods exclude. LeaVe did not scale to the full uncon strained pipeline of Ibex [100]. Thus, these methods cannot reason over instruction sequences that alter the dit-mode configuration. The fix for CVE-2024-28365 also resolved this violation and another where all instructions were affected in the Ibex small configuration in case of unexpected errors on the data bus. Ibex: Control-flow hijack - Issue 2169. Using CellDFT, we discovered a control-flow violation in Ibex in our custom configura tion. The operands of branches can direct the PC to arbitrary values (instead of the branch targets only), which can allow attackers to execute arbitrary code. According to Ibex maintainers, our configu ration (writeback stage without branch target ALU) is unsupported. However, this was nowhere documented and thus poses a hidden risk. 7.2.3 PicoRV32 and Scarv: PicoRV32 implements (and documents) data-dependent shift durations in its default configuration. Apart from that, it satisfies CFI. Our results confirm a known violation in Scarv, where byte-wise memory accesses leak whether a memory-mapped IO address is accessed [34]. Scarv additionally implements the RISC-V scalar cryptography extension [81], which has not been verified against CT before. We provide results for single and multi-cycle versions in Appendix C in [25]. All cryptography instructions satisfy CFI.

8 Discussion Scope of CFI verification. Because ci and vi instructions are allowed to influence the PC in some ways, we cannot verify their CT property. However, in the CT threat model this is of little interest, since these instructions are not CT-secure at architectural level. There could be bugs where a CT-violating instruction influences the timing of younger instructions other than through its own variable latency. None of the state-of-the-art CT verification methods [33, 35, 100], including CFI, can detect these. While irrelevant under CT, these cases could be of interest if software is protected by time balancing [77]. To ensure the functional correctness of the CF, functional verification methods [79] for ci and vi instructions can be applied. State of functional verification. CFI verification does not re quire as precondition that a CPU has undergone complete formal functional verification, which is rarely the case in practice [79, 86]. Naturally, as for any verification method, there remains the possi bility that bugs mask other bugs until the CPU has been completely formally verified. For example, because we associate every read with an instruction, if a CPU contains faults in its register reading logic, in the worst case, we could potentially associate a CFI viola tion with a wrong instruction. Violations of CFI on functionally verified designs are either of timing or CF violation nature. If a CPU has undergone a complete formal functional verification, CFI violations will always be related to timing. Verifying larger CPUs. Advanced optimizations (e.g., macro-op fusions, speculative execution, or data-dependent prefetch) could cause CFI violations if they are value- and not register address dependent. Developing declassification rules for these optimizations is an interesting direction for future work. Our current implementa tion does not track data loaded from memory into a GPR. This can be addressed by identifying the memory data ports and tainting in coming data like for GPRs. In the cores we studied, memories were abstracted. Including caches into the verification would require further declassification rules, which we leave for future work, or memory instrumentation [71, 90]. We obtained unbounded proofs

Table 6: Verified threat models and automation support in CFI and related work. We compare our four considered threat models (see Section 4) and support for automation, instruction classification (Instr. class.), and arbitrary instructions (Arb. instrs.). Threat model

Method

Data leak

CF hijack

CT viol.

Delay inj.

Auto mation

Instr. class. Arb. instrs. CFI ConjunCT [35] LeaVe [100] UPEC-DIT [33, 34] on the studied cores. However, for larger cores, typical abstrac tion techniques will be required [85], which opens future research directions for applying CFI.

9 Related Work Table 6 compares different aspects of CFI with related work: Threat model: Related methods focus on timing varieties only [35, 40, 96], explicitly disregarding data flows [33, 34, 100]. UPEC-DIT and ConjunCT determine a set of instructions that produce CT secure programs when only these instructions are combined [33, 34, 35]. Automation: LeaVe [100] and UPEC-DIT [33] require man ual extraction of design conditions and specification of candidate invariants to exclude known or discovered (or in case of UPEC also spurious) violations. While LeaVe can manually declassify data used by a CT-violating instruction via contract specification, it is not able to generate these non-trivial contract statements auto matically [100]. UPEC needs the verification engineer to decide about the validity of information flows in multiple iterations before obtaining a proof [33, 34]. ConjunCT [35] learns invariants and requires only the annotation of a few signals, in the same order as CFI. Instruction classification: LeaVe [100] can precisely find the root cause of a violation, but requires manual relation of the resulting design condition to instructions. UPEC-DIT [33] and ConjunCT [35] provide results per instruction, but with limita tions. UPEC-DIT excludes violating instructions from the proof [33], leading to a reduced threat model. ConjunCT may misclassify in structions in certain cases [35]. CFI precisely relates a violation to an instruction by design. Arbitrary instructions: UPEC-DIT and ConjunCT cannot detect cases where CT instructions interact with non-CT instructions, because the non-CT instructions need to be removed from the proof [33, 35]. Most importantly, these two methods cannot detect cases where an instruction that is CT in itself influences the timing of a younger instruction. For exam ple, in Kronos we found that an add instruction that satisfies CFI on its own can cause a CFI violation only if it is followed by a csrrw. Using an approach like ConjunCT or UPEC-DIT, the csrrw would have to be excluded from the verified instructions due to its own influence on the PC and therefore the violation would not be detected. While LeaVe can detect such case (related to CT), it requires manual association of the result to a specific instruction. LeaVe declassifies CT violations by adding relational constraints to the contract. CFI leverages a property of CellIFT’s taint tracking logic that allows the individual verification of instructions (see A.1 in [25]). Therefore, the instruction sequence does not need to be restricted for both methods. [36] verifies the CT property of a small custom CPU without forwarding. Verification automation. Zeng et al. [111] proposed a method to generate update functions from an RTL design. This function captures the data a signal is updated to, whereas we capture the condition under which it is updated. Some RISC-V cores implement the riscv-formal interface [108]. Being an observational circuit, it cannot be used for taint injection. Furthermore, the connection of signals to this interface is a manual effort and most signals are bulk updated in the last pipeline stage [108], making it difficult to check intermediate states. Borkar et al. [13] propose a fuzzer for finding timing violations. Being a simulation-based method, it cannot provide guarantees of absences. IFT verification. Kastner et al. [32] presented a tool to mine information flow properties from simulation traces to test them with a proprietary tool. Information flow properties that are specified allow taint flows under certain conditions. The method we propose can be extended in the same manner. Since the condition would always be true in case of the CFI property, we let our IFT property unconditioned. Ardeshiricham et al. [5] proposed a timing flow logic implemented in a proprietary tool. Such a logic could be used to distinguish between timing and control dependencies.

10 Conclusion We presented the CFI property that ensures that instructions are data oblivious and do not influence the control flow unless explicitly specified by the ISA. We developed the first automated and reusable method for formally verifying CFI based on detecting information flows from instruction’s operands to the PC. Our taint injection and flow declassification mechanisms allow us to verify interac tions between arbitrary instruction combinations in unbounded sequences, where each of them may operate on public, secret or attacker-controlled data. Leveraging taint logic based IFT verifica tion of the entire pipeline, CFI verification requires tagging only a few signals and can associate the violation of CFI to an offending instruction, simplifying verification and triaging. Applying CFI verification to four in-order RISC-V cores, we proved the CFI prop erty in many cases and found five new security vulnerabilities, including in previously verified CPUs. Ethical considerations. We have reported the property viola tions to the maintainers of the respective repositories.

Acknowledgments

The authors would like to thank the anonymous reviewers for their valuable feedback, Patrick Jattke for his help in formatting the pa per, and the maintainers of the designs we verified for their support in understanding and fixing some of the bugs. This work was sup ported by the Swiss State Secretariat for Education, Research and In novation under contract number MB22.00057 (ERC-StG PROMISE).

References

[1] Martin Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. 2009. Control flow integrity principles, implementations, and applications. ACM TOPS ’09, 13, 1, Article 4, (Nov. 2009). https://doi.org/10.1145/1609956.1609960.

[2] Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. [n. d.] Verifying Constant-Time Implementations. In USENIX Security 2016.

[3] Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, and Tiago Oliveira. [n. d.] Certified compilation for cryptography: Extended x86 instructions and constant-time verification. In INDOCRYPT 2020. Springer.

[4] Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, and Deian Stefan. [n. d.] Towards verified, constant-time floating point operations. In ACM SIGSAC 2018.

[5] Armaiti Ardeshiricham, Wei Hu, and Ryan Kastner. [n. d.] Clepsydra: Model ing timing flows in hardware designs. In IEEE/ACM ICCAD 2017.

[6] Armaiti Ardeshiricham, Wei Hu, Joshua Marxen, and Ryan Kastner. [n. d.] Register transfer level information flow tracking for provably secure hardware design. In IEEE DATE 2017.

[7] Gilles Barthe, Gustavo Betarte, Juan Campo, Carlos Luna, and David Pichardie. [n. d.] System-level non-interference for constant-time cryptography. In ACM SIGSAC 2014.

[8] Gilles Barthe, Sandrine Blazy, Benjamin Gregoire, Remi Hutin, Vincent La porte, David Pichardie, and Alix Trieu. [n. d.] Formal verification of a constant time preserving C compiler. In ACM POPL 2019.

[9] Mohammad Behnia et al. 2021. Speculative interference attacks: breaking invisible speculation schemes. In ASPLOS 2022.

[10] Emery D. Berger and Benjamin G. Zorn. [n. d.] DieHard: Probabilistic memory safety for unsafe languages. In ACM PLDI ’06.

[11] Sandrine Blazy, David Pichardie, and Alix Trieu. 2019. Verifying constant-time implementations by abstract interpretation. Journal of Computer Security, 27.

[12] Tyler Bletsch, Xuxian Jiang, Vince W Freeh, and Zhenkai Liang. [n. d.] Jump oriented programming: a new class of code-reuse attack. In ASIACCS 2011.

[13] Pallavi Borkar, Chen Chen, Mohamadreza Rostami, Nikhilesh Singh, Rahul Kande, Ahmad-Reza Sadeghi, Chester Rebeiro, and Jeyavijayan Rajendran. WhisperFuzz: White-box fuzzing for detecting and locating timing vulnera bilities in processors. ().

[14] Jay Bosamiya, Wen Shih Lim, and Bryan Parno. [n. d.] Provably-Safe Multi lingual Software Sandboxing Using Webassembly. In USENIX Security 2022.

[15] Aaron R. Bradley. 2011. Sat-based model checking without unrolling. In Springer Berlin Heidelberg.

[16] N. Bruns, V. Herdt, D. Große, and R. Drechsler. [n. d.] Efficient cross-level processor verification using coverage-guided fuzzing. In VLSI 2022.

[17] N. Bruns, V. Herdt, E. Jentzsch, and R. Drechsler. [n. d.] Cross-level proces sor verification via endless randomized instruction stream generation with coverage-guided aging. In DATE 2022.

[18] [n. d.] Cadence jasper formal property verification (fpv) app. Accessed: 2024-07-10. https://www.cadence.com/en_US/home/tools/system-design-and-ve rification/formal-and-static-verification/jasper-gold-verification-platform /formal-property-verification-app.html.

[19] S. Canakci, C. Rajapaksha, L. Delshadtehrani, A. Nataraja, M. B. Taylor, M. Egele, and A. Joshi. [n. d.] ProcessorFuzz: Processor fuzzing with control and status registers guidance. In HOST 2023.

[20] Nicholas Carlini, Antonio Barresi, Mathias Payer, David Wagner, and Thomas R Gross. [n. d.] Control-Flow Bending: On the Effectiveness of Control-Flow Integrity. In USENIX Security 2015.

[21] Sunjay Cauligi, Craig Disselkoen, Klaus v Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. [n. d.] Constant-time foundations for the new spectre era. In ACM SIGPLAN 2020.

[22] Katharina Ceesay-Seitz, Hamza Boukabache, and Daniel Perrin. 2020. A func tional verification methodology for highly parametrizable, continuously oper ating safety-critical fpga designs: applied to the cern radiation monitoring elec tronics (crome). In Computer Safety, Reliability, and Security. António Casimiro, Frank Ortmeier, Friedemann Bitsch, and Pedro Ferreira, (Eds.) Springer Inter national Publishing, Cham, 67–81. isbn: 978-3-030-54549-9.

[23] Katharina Ceesay-Seitz, Hamza Boukabache, and Daniel Perrin. [n. d.] Semi formal reformulation of requirements for formal property verification. In accellera DVCON EUROPE 2019.

[24] Katharina Ceesay-Seitz, Sarath Kundumattathil Mohanan, Hamza Bouk abache, and Daniel Perrin. [n. d.] Formal property verification of the digital section of an ultra-low current digitizer asic. In accellera DVCON EUROPE 2021.

[25] Katharina Ceesay-Seitz, Flavien Solt, and Kaveh Razavi. 2024. CFI: formal verification of microarchitectural control-flow integrity. In Extended version of this paper. https://comsec.ethz.ch/wp-content/files/mucfi_ccs24.pdf.

[26] C. Chen, R. Kande, N. Nyugen, F. Andersen, A. Tyagi, A. R. Sadeghi, and J. Rajendran. HyPFuzz: Formal-assisted processor fuzzing. ().

[27] Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. [n. d.] Code-Level Model Checking in the Software Devel opment Workflow. In ACM/IEEE ICSE 2020 (Icse-Seip 2020).

[28] Edmund M. Clarke, Thomas A. Henzinger, and Helmut Veith. 2018. Handbook of Model Checking. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, (Eds.) Springer International Publishing, Cham. https: //doi.org/10.1007/978-3-319-10575-8.

[29] Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties. Journal of Computer Security, 18, 6.

[30] John Criswell, Nathan Dautenhahn, and Vikram Adve. [n. d.] KCoFI: Complete control-flow integrity for commodity operating system kernels. In IEEE S&P 2014.

[31] Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. [n. d.] Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. In IEEE S&P 2020.

[32] Calvin Deutschbein, Andres Meza, Francesco Restuccia, Ryan Kastner, and Cynthia Sturton. [n. d.] Isadora: Automated information flow property gener ation for hardware designs. In ACM ASHES 2021.

[33] Lucas Deutschmann, Johannes Müller, Mohammad R. Fadiheh, Dominik Stof fel, and Wolfgang Kunz. 2024. A scalable formal verification methodology for data-oblivious hardware. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1–1. doi: 10.1109/TCAD.2024.3374249.

[34] Lucas Deutschmann, Johannes Müller, Mohammad R. Fadiheh, Dominik Stof fel, and Wolfgang Kunz. [n. d.] Towards a formally verified hardware root-of trust for data-oblivious computing. In ACM/IEEE DAC 2022.

[35] S. Dinesh, M. Parthasarathy, and C. Fletcher. [n. d.] ConjunCT: Learning inductive invariants to prove unbounded instruction safety against microar chitectural timing attacks. In IEEE S&P 2024.

[36] Ning Dong, Roberto Guanciale, Mads Dam, and Andreas Lööw. [n. d.] Formal verification of correctness and information flow security for an in-order pipelined processor. In FMCAD 2023.

[37] Yufei Du, Zhuojia Shen, Komail Dharsee, Jie Zhou, Robert J Walls, and John Criswell. [n. d.] Holistic control-flow protection on real-time embedded sys tems with kage. In USENIX Security 2022.

[38] Limor Fix. 2008. Fifteen Years of Formal Property Verification in Intel. In 25 Years of Model Checking: History, Achievements, Perspectives. Orna Grumberg and Helmut Veith, (Eds.) Springer Berlin Heidelberg, 139–144. https://doi.org /10.1007/978-3-540-69850-0_8.

[39] Lukas Gerlach, Daniel Weber, Ruiyi Zhang, and Michael Schwarz. [n. d.] A security RISC: Microarchitectural attacks on hardware RISC-v cpus. In IEEE S&P 2023.

[40] Klaus v Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, and Ranjit Jhala. [n. d.] IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security 2019.

[41] Aman Goel and Karem Sakallah. [n. d.] Model checking of verilog rtl using ic3 with syntax-guided abstraction. In NFM 2019. Springer.

[42] Ben Gras, Kaveh Razavi, Erik Bosman, Herbert Bos, and Cristiano Giuffrida. [n. d.] ASLR on the line: Practical cache attacks on the MMU. In NDSS 2017.

[43] Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. [n. d.] Hardware software contracts for secure speculation. In IEEE S&P 2021.

[44] Lorenz Hetterich and Michael Schwarz. [n. d.] Branch different-spectre attacks on apple silicon. In DIMVA 2022. Springer.

[45] Karine Heydemann, Jean-François Lalande, and Pascal Berthome. 2019. For mally verified software countermeasures for control-flow integrity of smart card C code. Computers & Security, 85.

[46] Wei Hu, Armaiti Ardeshiricham, and Ryan Kastner. 2021. Hardware informa tion flow tracking. ACM Comput. Surv., 54, 4, Article 83, (May 2021), 39 pages. doi: 10.1145/3447867.

[47] Wei Hu, Lingjuan Wu, Yu Tai, Jing Tan, and Jiliang Zhang. 2020. A unified formal model for proving security and reliability properties. In 2020 IEEE 29th Asian Test Symposium (ATS), 1–6. doi: 10.1109/ATS49688.2020.9301533.

[48] J. Hur, S. Song, D. Kwon, E. Baek, J. Kim, and B. Lee. [n. d.] Difuzzrtl: Differ ential fuzz testing to find cpu bugs. In IEEE S&P 2021.

[49] [n. d.] Ibex CPU. Accessed: 2024-04-16. https://github.com/lowRISC/opentitan.

[50] [n. d.] Ibex documentation - verification stages. Accessed: 2024-04-16. https: //ibex-core.readthedocs.io/en/latest/03_reference/verification_stages.html.

[51] 2018. IEEE standard for SystemVerilog–unified hardware design, specification, and verification language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012).

[52] Intel Corporation. [n. d.] Data Operand Independent Timing ISA Guidance. [Updated 13-February-2023]. https://www.intel.com/content/www/us/en/dev eloper/articles/technical/sof tware-security-guidance/best-practices/data-o perand-independent-timing-isa-guidance.html.

[53] Jan Jancar, Marcel Fourne, Daniel De Almeida Braga, Mohamed Sabt, Pe ter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. [n. d.] “They’re not that hard to mitigate”: What cryptographic library developers think about timing attacks. In IEEE S&P 2022.

[54] N. Kabylkas, T. Thorn, S. Srinath, P. Xekalakis, and J. Renau. [n. d.] Effective processor verification with logic fuzzer enhanced co-simulation. In IEEE/ACM MICRO 2021.

[55] R. Kande, A. Crump, G. Persyn, P. Jauernig, A. R. Sadeghi, A. Tyagi, and J. Rajendran. [n. d.] TheHuzz: Instruction Fuzzing of Processors Using Golden Reference Models for Finding Software-Exploitable Vulnerabilities. In USENIX Security 2022.

[56] Paul Kocher et al. [n. d.] Spectre attacks: Exploiting speculative execution. In IEEE S&P 2019.

[57] [n. d.] Kronos RISC-v (all cascade fixes integrated). Accessed: 2024-07-10. https://github.com/cascade-artifacts-designs/cascade-kronos.

[58] Michael Kurth, Ben Gras, Dennis Andriesse, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. [n. d.] NetCAT: Practical cache attacks from the network. In IEEE S&P 2020.

[59] K. Laeufer, J. Koenig, D. Kim, J. Bachrach, and K. Sen. [n. d.] RFUZZ: Coverage directed fuzz testing of RTL on fpgas. In ICCAD 2018.

[60] Moritz Lipp et al. [n. d.] Meltdown: Reading kernel memory from user space. In USENIX Security 2018.

[61] Chang Liu, Michael Hicks, and Elaine Shi. [n. d.] Memory Trace Oblivious Program Execution. In IEEE CSF 2013.

[62] Arthur Costa Lopes and Diego F Aranha. 2017. Benchmarking tools for verifi cation of constant-time execution. SBSEG. Bento Goncalves, Brazil: SBC.

[63] lowRISC contributors. [n. d.] OpenTitan root of trust. Accessed: 2024-07-10. https://opentitan.org/.

[64] Andrea Mambretti, Alexandra Sandulescu, Alessandro Sorniotti, William Robertson, Engin Kirda, and Anil Kurmus. [n. d.] Bypassing memory safety mechanisms through speculative control flow hijacks. In IEEE EuroS&P 2021.

[65] Ali Jose Mashtizadeh, Andrea Bittau, Dan Boneh, and David Mazieres. [n. d.] CCFI: Cryptographically enforced control flow integrity. In ACM SIGSAC 2015.

[66] K. L. McMillan. [n. d.] Interpolation and sat-based model checking. In CAV 2003.

[67] Ahmad Moghimi, Jan Wichelmann, Thomas Eisenbarth, and Berk Sunar. 2019. MemJam: a false dependency attack against constant-time crypto implemen tations. IJPP 2019, 47, 4, (Aug. 2019), 538–570.

[68] Daniel Moghimi. [n. d.] Downfall: Exploiting speculative data gathering. In USENIX Security 2023.

[69] David Molnar, Matt Piotrowski, David Schultz, and David Wagner. [n. d.] The program counter security model: Automatic detection and removal of control-flow side channel attacks. In USENIX Security 2005.

[70] Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. [n. d.] Axiomatic hardware-software contracts for security. In ACM ISCA 2022.

[71] Jason Oberg, Sarah Meiklejohn, Timothy Sherwood, and Ryan Kastner. 2014. Leveraging gate-level properties to identify hardware timing channels. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 33, 9, 1288–1301.

[72] Oleksii Oleksenko, Christof Fetzer, Boris Köpf, and Mark Silberstein. [n. d.] Revizor: Testing black-box CPUs against speculation contracts. In ASPLOS 2022.

[73] Marcelo Orenes-Vera, Aninda Manocha, David Wentzlaff, and Margaret Martonosi. [n. d.] AutoSVA: Democratizing formal verification of RTL module interactions. In ACM/IEEE DAC 2021.

[74] Marcelo Orenes-Vera, Hyunsung Yun, Nils Wistoff, Gernot Heiser, Luca Benini, David Wentzlaff, and Margaret Martonosi. [n. d.] AutoCC: Automatic discov ery of covert channels in time-shared hardware. MICRO 2023, 51.

[75] [n. d.] PicoRV32 - a size-optimized RISC-v CPU. Accessed: 2024-07-10. https: //github.com/YosysHQ/picorv32.

[76] Marco Prandini and Marco Ramilli. [n. d.] Return-oriented programming. In IEEE S&P 2012. Vol. 10.

[77] Qi Qin, JulianAndres JiYang, Fu Song, Taolue Chen, and Xinyu Xing. [n. d.] Dejitleak: eliminating jit-induced timing side-channel leaks. In (ACM ESEC/FSE 2022).

[78] Hany Ragab, Alyssa Milburn, Kaveh Razavi, Herbert Bos, and Cristiano Giuf frida. [n. d.] Crosstalk: Speculative data leaks across cores are real. In IEEE S&P 2021.

[79] Alastair Reid et al. [n. d.] End-to-end verification of processors with ISA formal. In CAV 2016.

[80] Jan Richter-Brockmann, Jakob Feldtkeller, Pascal Sasdrich, and Tim Güneysu. 2022. Verica - verification of combined attacks: automated formal verification of security against simultaneous information leakage and tampering. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2022, 4, (Aug. 2022), 255–284. doi: 10.46586/tches.v2022.i4.255-284.

[81] RISC-V. 2024. RISC-v cryptography extension. [Online; accessed 1-December 2023]. https://github.com/riscv/riscv-crypto.

[82] Grigore Roşu, Wolfram Schulte, and Traian Florin Şerbănuţă. [n. d.] Runtime verification of C memory safety. In RV ’2009. Springer.

[83] Sarwar Sayeed, Hector Marco-Gisbert, Ismael Ripoll, and Miriam Birch. 2019. Control-flow integrity: attacks and protections. Applied Sciences, 9, 20.

[84] [n. d.] SCARV: processor core implementation. Accessed: 2024-07-10. https: //github.com/scarv/scarv-cpu.

[85] Erik Seligman, Tom Schubert, and Achutha M. V. Kiran Kumar. 2023. Formal Verification. An Essential Toolkit for Modern VLSI Design. (2nd ed.). Elsvier Science & Technology.

[86] Siemens AG. [n. d.] The 2022 Wilson Research Group Functional Verification Study. Accessed: 2024-4-28. https://blogs.sw.siemens.com/verificationhorizo ns/2022/12/12/part-8-the-2022-wilson-research-group-functional-verificat ion-study/.

[87] Flavien Solt, Katharina Ceesay-Seitz, and Kaveh Razavi. [n. d.] Cascade: CPU Fuzzing via Intricate Program Generation. In USENIX Security 2024.

[88] Flavien Solt, Ben Gras, and Kaveh Razavi. [n. d.] CellIFT: Leveraging Cells for Scalable and Precise Dynamic Information Flow Tracking in RTL. In USENIX Security 2022.

[89] Flavien Solt, Patrick Jattke, and Kaveh Razavi. [n. d.] RemembERR: Leveraging microprocessor errata for design testing and validation. In IEEE/ACM MICRO 2022.

[90] Flavien Solt and Kaveh Razavi. [n. d.] Hybridift: scalable memory-aware dynamic information flow tracking for hardware. ICCAD 2024.

[91] G Edward Suh, Jae W Lee, David Zhang, and Srinivas Devadas. 2004. Secure program execution via dynamic information flow tracking. ACM Sigplan Notices, 39, 11.

[92] Caroline Tice, Tom Roeder, Peter Collingbourne, Stephen Checkoway, Ul far Erlingsson, Luis Lozano, and Geoff Pike. [n. d.] Enforcing forward-edge control-flow integrity in GCC & LLVM. In USENIX Security 2014.

[93] Mohit Tiwari, Hassan MG Wassel, Bita Mazloom, Shashidhar Mysore, Frederic T Chong, and Timothy Sherwood. [n. d.] Complete information flow tracking from the gates up. In ASPLOS 2019.

[94] T. Trippel, K. G. Shin, A. Chernyakhovsky, G. Kelly, D. Rizzo, and M. Hicks. [n. d.] Fuzzing Hardware Like Software. In USENIX Security 2022.

[95] Daniël Trujillo, Johannes Wikner, and Kaveh Razavi. [n. d.] INCEPTION: Exposing New Attack Surfaces with Training in Transient Execution. In USENIX Security 2023.

[96] Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, and Ranjit Jhala. [n. d.] Solver-aided constant-time hardware verification. In ACM SIGSAC 2021.

[97] Stephan Van Schaik, Alyssa Milburn, Sebastian Österlund, Pietro Frigo, Giorgi Maisuradze, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. [n. d.] RIDL: Rogue in-flight data load. In IEEE S&P 2019.

[98] Jose Rodrigo Sanchez Vicarte, Michael Flanders, Riccardo Paccagnella, Grant Garrett-Grossman, Adam Morrison, Christopher W. Fletcher, and David Kohlbrenner. [n. d.] Augury: Using data memory-dependent prefetchers to leak data at rest. In IEEE S&P 2022.

[99] Huibo Wang et al. [n. d.] Towards memory safe enclave programming with rust-sgx. In ACM SIGSAC 2019.

[100] Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. [n. d.] Specification and verification of side-channel security for open-source processors via leakage contracts. In ACM SIGSAC 2023. Weizhi Meng, Christian Damsgaard Jensen, Cas Cremers, and Engin Kirda, (Eds.) ACM, 2128–2142. https://doi.org/10.1145/3576915.3623192.

[101] Tobias Wiersema, Stephanie Drzevitzky, and Marco Platzner. [n. d.] Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring. In IEEE FPT 2014.

[102] Johannes Wikner, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. [n. d.] Spring: Spectre Returning in the Browser with Speculative Load Queuing and Deep Stacks. In WOOT 2022.

[103] Johannes Wikner and Kaveh Razavi. [n. d.] RETBLEED: Arbitrary Speculative Code Execution with Return Instructions. In USENIX Security 2022.

[104] Johannes Wikner, Daniël Trujillo, and Kaveh Razavi. [n. d.] Phantom: Exploit ing decoder-detectable mispredictions. MICRO 2023.

[105] Clifford Wolf, Johann Glaser, and Johannes Kepler. [n. d.] Yosys-a free Verilog synthesis suite. In Austrochip 2013.

[106] Xiaoyang Xu, Masoud Ghaffarinia, Wenhao Wang, Kevin W Hamlen, and Zhiqiang Lin. [n. d.] Confirm: Evaluating Compatibility and Relevance of Control-Flow Integrity Protections for Modern Software. In USENIX Security 2019.

[107] Sungbae Yoo, Jinbum Park, Seolheui Kim, Yeji Kim, and Taesoo Kim. [n. d.] In-Kernel Control-Flow Integrity on Commodity OSes using ARM Pointer Authentication. In USENIX Security 2022.

[108] Yosys Open SYnthesis Suite. [n. d.] RISC-V Formal Verification Framework. Accessed: 2024-07-10. https://github.com/YosysHQ/riscv-formal.

[109] Jiyong Yu, Trent Jaeger, and Christopher Wardlaw Fletcher. [n. d.] All your PC are belong to us: Exploiting non-control-transfer instruction BTB updates for dynamic PC extraction. In ACM ISCA 2023.

[110] Bin Zeng, Gang Tan, and Greg Morrisett. [n. d.] Combining control-flow integrity and static analysis for efficient and validated data sandboxing. In ACM CCS 2011.

[111] Yu Zeng, Aarti Gupta, and Sharad Malik. [n. d.] Automatic generation of architecture-level models from RTL designs for processors and accelerators. In IEEE DATE 2022.

[112] Anthony Zgheib, Olivier Potin, Jean-Baptiste Rigaud, and Jean-Max Dutertre. [n. d.] A CFI verification system based on the RISC-v instruction trace encoder. In IEEE DSD 2022, 456–463.

[113] Qizhi Zhang, Jiaji He, Yiqiang Zhao, and Xiaolong Guo. 2020. A formal frame work for gate- level information leakage using z3. In AsianHOST, 1–6. doi: 10.1109/AsianHOST51057.2020.9358257.