WhisperFuzz: White-Box Fuzzing for
Detecting and Locating Timing Vulnerabilities in Processors

Pallavi Borkar^,These authors contributed equally to this work., Chen Chen^†, ∗, Mohamadreza Rostami^, Nikhilesh Singh^, Rahul Kande^†,

Ahmad-Reza Sadeghi^, Chester Rebeiro^, and Jeyavijayan (JV) Rajendran^†

Indian Institute of Technology Madras, India,
^†Texas A&M University, USA,

^Technische Universität Darmstadt, Germany

{cs20d202, nik<EMAIL_ADDRESS>
^†{chenc, rahulkande<EMAIL_ADDRESS>
^{mohamadreza.rostami<EMAIL_ADDRESS>
Timing vulnerabilities in processors have emerged as a potent threat. As processors are the foundation of any computing system, identifying these flaws is imperative. Recently fuzzing techniques, traditionally used for detecting software vulnerabilities, have shown promising results for uncovering vulnerabilities in large-scale hardware designs, such as processors.
Researchers have adapted black-box or grey-box fuzzing to detect timing vulnerabilities in processors. However, they cannot identify the locations or root causes of these timing vulnerabilities, nor do they provide coverage feedback to enable the designer's confidence in the processor's security.

To address the deficiencies of the existing fuzzers, we present —the first white-box fuzzer with static analysis —aiming to detect and locate timing vulnerabilities in processors and evaluate the coverage of microarchitectural timing behaviors.
uses the fundamental nature of processors' timing behaviors, microarchitectural state transitions, to localize timing vulnerabilities.
automatically extracts microarchitectural state transitions from a processor design at the register-transfer level (RTL) and instruments the design to monitor the state transitions as coverage. Moreover,  measures the time a design-under-test (DUT) takes to process tests, identifying any minor, abnormal variations that may hint at a timing vulnerability.

detects 12 new timing vulnerabilities across advanced open-sourced  processors: , , and . Eight of these violate the zero latency requirements of the Zkt extension <cit.> and are considered serious security vulnerabilities. Moreover,  also pinpoints the locations of the new and the existing vulnerabilities.

§ INTRODUCTION

The evolution in computer architecture has significantly amplified the complexity of hardware design, especially in modern processors, which are the foundation of today's computing systems.
As technology advances, designers integrate more functionalities into hardware, leading to more intricate architectural and microarchitectural features in processors.
However, as the complexity of the design increases, so does the number of design regions to verify and protect.
Traditional techniques to verify modern processors cannot scale with the number of (new) hardware vulnerabilities discovered.
For example, the number of newly detected hardware common vulnerabilities in the National Vulnerability Database (NVD) increased from three in 2012 to 92 in 2022 <cit.>.
Further, as of 2023, MITRE reported 117 hardware-related vulnerability types, known as Common Weakness Enumerations (CWEs) <cit.>.
These rapidly increasing vulnerabilities threaten the security of the expanding digital landscape across different domains.

Timing vulnerabilities are of particular concern as they can leak sensitive information, undermining the entire system's security.
Well-known attacks such as Spectre <cit.>, Meltdown <cit.>, Foreshadow <cit.>, LVI <cit.>, RIDL <cit.>, ZombieLoad <cit.>, CrossTalk <cit.>, Zenbleed <cit.>, and Retbleed <cit.> exploit timing vulnerabilities present in a wide range of commercial processors. Multiple variants of these attacks have been shown to subvert security countermeasures implemented to prevent such attacks.
Unlike functional vulnerabilities, timing vulnerabilities can manifest in a logically correct implementation, making them hard to detect.
Timing vulnerabilities rely on the difference in execution time of the hardware components to leak sensitive information.
These vulnerabilities underscore the need for rigorous security analysis in modern processors.
Moreover, unlike software flaws, which can be patched post-deployment, fixing hardware vulnerabilities after manufacturing is difficult, as they are physically ingrained into the Silicon.
Therefore, detecting vulnerabilities at the pre-Silicon stage is imperative for secure hardware.

Existing timing vulnerability detection strategies for processors use formal methods or fuzzing.
Formal methods, such as theorem proving <cit.>, model checking <cit.>, assertion proving <cit.>, and information-flow tracking <cit.> explore design spaces exhaustively and prove security assertions about hardware.
Thus, detecting timing vulnerabilities using formal methods is a rigorous approach to ensure design security <cit.>.
However, these methods are limited by the state explosion problem <cit.>;

exhaustively exploring the complex modern hardware is computationally hard <cit.>.
Some approaches aim to handle this scalability issue by modeling hardware at the higher abstraction level and approximating its timing behavior <cit.>.
However, abstracting hardware can lead to over-optimistic results or false positives <cit.>.
Furthermore, these formal approaches require a comprehensive understanding of the designs' security specifications and manually defining properties,

an error-prone process <cit.>.

Alternatively, hardware fuzzing has shown its effectiveness in detecting vulnerabilities in large-scale designs <cit.>.
Using fuzzing, Google detected the recent vulnerability on AMD Zen2 processors, Zenbleed <cit.>, a speculative execution vulnerability that allows attackers to extract sensitive information through software exploitation <cit.>.
Black-box fuzzing <cit.> and grey-box fuzzing <cit.> have been applied to detect timing vulnerabilities in processors.
They explore the design spaces by generating different combinations of instructions as inputs and use performance counters to identify potential timing vulnerabilities <cit.>.
While these techniques overcome the scalability issue of formal verification, they suffer from two critical limitations.
First, although they successfully find instructions that cause timing vulnerabilities, they rely on confirmation from designers to identify and pinpoint the root cause (locations) <cit.>. Second, they lack the adequate coverage metric to capture the timing behaviors of the processor.
Designers rely on coverage metrics to obtain the necessary confidence before tape-out <cit.>.
Therefore, introducing such metrics to evaluate the progress of fuzzing is typical <cit.>.

We will elaborate on these shortcomings in Section <ref>.

Our Goals and Contributions.
We enhance existing fuzzing strategies to address their limitations by integrating static analysis.
This allows us to automatically pinpoint the sources of timing vulnerabilities and compute the coverage of timing behaviors in processor designs.
Our fuzzer efficiently explores the design space, detecting timing vulnerabilities, while our novel static approach identifies the root causes and provides timing behavior coverage.

Locating the root cause of timing vulnerabilities and computing timing coverage is non-trivial and poses several challenges:
(i) expressing the timing behaviors of processor modules formally is complex, as they do not operate in isolation and can influence each other; (ii) finer measurement of module timing behaviors is needed, which is time-consuming for modern processors with numerous modules <cit.>; (iii) tracing vulnerabilities to their root causes within the design space is intricate; and (iv) traditional mutation algorithms used in fuzzers are insufficient for detecting timing vulnerabilities due to their reliance on microarchitectural state transitions.

To address these challenges, (i) We have developed the , a static program analysis technique that formally expresses module timing behaviors in a processor by extracting microarchitectural state transitions of a design-under-test (DUT) at the register-transfer level (RTL). To efficiently cover the extensive design space, we tailor the technique to generate individual graphs for each RTL module (cf. Section <ref>).
(ii) We analyze each RTL module's simulation trace to measure its timing behaviors precisely. To streamline our analysis efforts, we devise a hierarchical strategy based on the characteristics of timing vulnerabilities to prioritize modules for examination (cf. Section <ref>).
(iii) We pinpoint the root causes of detected timing vulnerabilities utilizing static analysis techniques and properties of the , employing a module-wise strategy to navigate the complex design space.
(iv) We have adapted traditional hardware fuzzing methods to efficiently explore a DUT's design spaces and crafted a specialized mutation engine to exploit timing vulnerabilities. Furthermore, we have instrumented graphs into the DUT to monitor module state transitions based on the input (cf. Section <ref>).

In summary, our contributions are:

* We present a novel white-box fuzzer with static analysis, , for timing vulnerability detection in processors at the RTL.  extracts and monitors microarchitectural state transitions at RTL and measures the timing behaviors of each RTL module to identify timing vulnerabilities. Hardware fuzzing enables  to explore the microarchitectural state space efficiently.

* With static analysis,  will identify the locations/root causes of timing vulnerabilities. Moreover,  introduces a timing coverage metric to help designers evaluate the timing behaviors explored.

* We evaluate the effectiveness of  on three real-world, open-sourced processors from RISC-V instruction set architecture (ISA) –  <cit.>,  <cit.>, and  <cit.>, which are widely used as benchmarks in the hardware security community.

*  finds 12 new timing vulnerabilities across all three benchmarks. Eight of them pose serious security vulnerabilities, according to the  Zkt contract <cit.>. We have submitted requests for  for these vulnerabilities.  also pinpoints the locations of all existing and new vulnerabilities.

§ BACKGROUND

In this section, we provide a succinct background on hardware fuzzing and microarchitectural timing side channels, which form the basis of .

§.§ Hardware Fuzzing

Hardware fuzzing is a dynamic verification technique that iteratively generates testing inputs called tests to verify target hardware <cit.>.
A coverage-feedback fuzzer starts by generating an initial set of tests, called seeds, randomly using a seed generator.
When fuzzing processors, these seeds are executable programs with a sequence of instructions <cit.>.
The fuzzer simulates the target hardware with these tests using open-source or commercial hardware simulation tools such as Verilator <cit.> and Synopsys VCS <cit.>.

During simulation, the fuzzer collects coverage information that quantifies the activities caused by the test in the hardware. For instance, the coverage information can be represented as transitions of finite-state machines (FSMs) <cit.>.
Fuzzers either instrument the hardware to add activity monitors <cit.>, or use the existing coverage monitors of the simulation tools <cit.> to collect this coverage information.
Next, it generates new tests automatically by performing bit manipulation operations, called mutations on the current tests, increasing coverage. The fuzzer iterates over this cycle of test generation and simulation to verify target hardware till desired coverage is achieved.

Fuzzers use a vulnerability detector to detect vulnerabilities using differential testing or hardware assertions.
In differential testing, the fuzzer runs a golden reference model along with the target hardware and compares its outputs to detect vulnerabilities <cit.>.
Alternatively, some fuzzers insert hardware assertions, i.e., rules describing the expected behavior, in the target hardware and detect vulnerabilities as violations of these assertions <cit.>. While existing black-box <cit.> and grey-box <cit.> fuzzers can detect timing vulnerabilities in processors, these approaches fail to locate the root causes of these vulnerabilities. Further, these techniques can not evaluate the explored timing behaviors. These limitations delay the mitigation process and leave out possibilities for undiscovered vulnerabilities hampering the designer's confidence.

§.§ Timing Side-Channel Attacks

Timing side-channel attacks exploit measurable variations in the execution time of instructions to glean secret information from victim applications. These timing variations arise from interactions of different operands with the micro-architecture.
For instance, <cit.> proposed a timing attack to recover AES keys by measuring the cache accesses during encryption across different keys.

[language=C, label = listing:inst_seq, caption=A pair of instruction sequences that have identical instructions but operate on different data. The instruction sequence is a timing vulnerability if the execution times differ.,style=customcArianeExploit,float,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/instruction_sequence.tex

Over the years, multiple techniques to perform timing attacks have developed such as  <cit.>,  <cit.>, and  <cit.>. The key idea of all these attacks is to target a specific shared resource, such as the cache memory, and exploit its data-dependent timing behavior. Such attacks consist of a sequence of instructions which when executed with different data take different execution times. For example, consider the pair of instruction sequences in Listing <ref>. The two sequences are identical but differ in the data they operate upon. The sequence can be considered a timing vulnerability if the execution of the two sequences results in different execution times.

The objective of our work is to develop , which identifies such instruction sequences and pairs of input data that result in different execution times. Furthermore,  localizes the root cause for the differing execution times, thereby assisting in mitigation.

§ METHODOLOGY

In this section, we first explain the relationship between timing behaviors and transitions of a digital circuit. We introduce the  that helps capture the microarchitectural transitions at a fine granularity. We use this graph to identify the location of timing vulnerabilities and monitor the timing behaviors covered. Further, we  discuss the challenges of extracting the   from a processor design. Finally, we give an overview of our solutions to these challenges and elaborate on each solution.

§.§ Microarchitectural Transitions and Timing Behaviors

A finite-state machine (FSM) can model a sequential digital circuit. Given an input, the circuit transitions through various states in the FSM to produce the output. Assuming each state in the FSM takes constant time, the sequence of state transitions to generate the output determines the execution time of the circuit for a given input. Thus, we claim: two different inputs resulting in the same state transition sequences will take the same execution time.

A finite-state machine (FSM) representation of the cache set protocol. Each state is assumed to take a constant time as shown at each node.

Consider the case study of a cache composed of multiple cache sets. Each cache set can be represented as an FSM with five states: , , , , and , as shown in Figure <ref>. When a program accesses data, the cache first performs a look-up for the associated memory address in the  state. If the data is found in the cache (cache hit), it will be directly transferred to the  state, and the processor can access the data without going to the main memory.
Thus, an input address that is already present in the cache set causes transitions  taking three clock cycles in its corresponding implementation.
However, if the data is not found (cache miss), the cache set will transfer to the  state to look for a free cache block to store the data. If a free block exists, the cache will transition to the  state and request the memory for the corresponding data.
In case the cache does not have a free block, it will transfer to the  state, select a block for eviction based on the replacement policy, and then transfer to the  state.
The cache waits in this state until it receives data from memory. It then transitions to the  state. Thus, if an input address is not present in the cache set, two FSM state transition sequences (and execution times) are possible: (i) , taking 19 clock cycles if the cache has a free block or (ii) , taking 23 cycles if the cache does not have a free block. Assuming each state in the FSM takes a constant execution time, a difference in the execution time of two inputs implies a difference in the sequence of state transitions followed in the FSM.
However, in practice, FSM states do not always take a constant execution time. Moreover, an FSM model is abstract and cannot effectively represent complex microarchitectural details in digital circuits. Thus, an FSM representation fails to uncover timing differences
arising at the microarchitectural level.
Further, it makes localizing the source of timing difference difficult, delaying the mitigation process.

We introduce Micro-Event Graphs (MEGs) to overcome these drawbacks. A MEG models a given digital circuit using the register-transfer level (RTL) as a set of events, which we call microarchitectural events. Each microarchitectural event affects the contents of at least one element, such as a wire or a register in the digital circuit. A MEG models a given digital circuit as possible events and dependencies between these events. Each node in the MEG represents an element while a directed edge from a parent node to a child node indicates that an event on the parent element can potentially trigger an event on the child element.

A high level representation of  (MEG) for cache set protocol represented as an FSM in Figure <ref>.

Figure <ref> shows a high-level representation of the MEG corresponding to the cache set protocol. The MEG consists of 15 nodes and 115 edges. Each state in the corresponding FSM (refer Figure <ref>) maps to one or more nodes in the MEG. For example, nodes colored in green (node labels starting with L) correspond to state  and those colored in yellow (node labels starting with P) correspond to state . Each execution of the cache set protocol can be mapped to at least one path in the MEG shown.
Similar to the state transitions in the FSM, but at the finest granularity, an input triggers a sequence of microarchitectural events in the MEG during its execution, each taking a constant time.
Thus, one can have the following observations:

P1. If two inputs to the microarchitecture result in the same event transitions in the MEG, then the execution time for the two inputs is the same.

P2. If there is a difference in the execution time of the two inputs, then the sequence of microarchitectural events followed is different for the two executions.

P3. If two inputs to the microarchitecture result in different event transitions in the MEG, then the execution time for the two inputs may differ.

§.§ Detecting and Localizing Timing Vulnerabilities in Processors: A High-Level Overview

The goal of  is to detect and localize timing vulnerabilities in a processor design-under-test (DUT). To detect timing vulnerabilities, we leverage the strength of hardware fuzzing. The fuzzer generates an instruction sequence and at least two corresponding data inputs of the form shown in Listing <ref>, that take different execution times when applied to the sequence.
For each pair of instruction sequences and inputs, we trace the path of events in the MEG. For example, in Figure <ref>, each path represents an execution corresponding to different addresses given to a  instruction. These paths are then used to localize the root cause of the vulnerability. The root cause is the event prior to the first bifurcation in these two paths.

The  framework. It includes three key modules. First, the Seed Generation module internally utilizes a coverage-feedback fuzzer to explore the design space. The generated inputs are recorded in a database. Mutations are performed to improve code coverage. Second, the Vulnerability Detection module uses the generated seed, mutates the instruction operands, and identifies the timing vulnerabilities based on DUT simulations. Finally, the Vulnerability Localization module pinpoints the locations of uncovered vulnerabilities.

For example, consider the two highlighted paths in Figure <ref>. One path traces event sequence { L6, L7, R10}, while the other traces {L6, L7, L9, W15, W14, R10}.
Each path corresponds to a different address given to a  instruction. Since the two paths are different, they may take different execution times due to P3 (See Section <ref>), resulting in a timing vulnerability. These paths trace the same events until L7, after which they bifurcate. Hence, an event on node L7 will likely be the vulnerability's root cause. The number of paths covered in the MEG gives a notion of the coverage of timing behaviors of the DUT.

§.§ Challenges

Developing  involves the following challenges.

[] Generating the MEG.
The MEG must capture all possible events and event transitions in a given processor DUT. This is specifically challenging in modern microprocessors due to their complexity and large code bases. We develop an automated strategy to address this challenge that extracts the MEG given the DUT's source code in RTL form. Section <ref> elaborates on this strategy.

[] Characterizing timing behavior of each processor module.
One way to determine timing behaviors is to input instruction sequences to the DUT and measure the execution time. However, a complete processor design contains thousands of signals, complicating the localization of the vulnerability. An alternate bottom-up approach is to isolate each module in the processor, provide inputs, and measure the timing behavior of the module. However, timing differences detected may not be observable when the module is integrated into the complete processor. Therefore, we follow a two-pronged approach where we first generate instruction sequences for the complete processor to detect timing differences and localize at a module level. We present a hierarchical analysis strategy to prioritize the modules to be analyzed, thereby detecting vulnerabilities faster, as discussed in Section <ref>.

[] Localizing the source of timing vulnerability.
The large code space of the processor's DUT makes it challenging to locate the source of a timing vulnerability. It necessitates manual effort and a detailed understanding of the processor's microarchitecture. To address this challenge, we introduce an automated static analysis strategy on the MEG that can identify the root cause of the timing vulnerability within a few seconds. Section <ref> elaborates on the strategy.

[] Fuzzing the microarchitectural state space and determining coverage.
Hardware fuzzing has shown its effectiveness in detecting vulnerabilities in large-scale designs, such as processors.
However, the existing grey-box processor fuzzers <cit.> are not compatible with timing vulnerability detection.
Their mutation algorithms are designed to accelerate coverage increment, but timing vulnerability detection requires sequences of data-dependent instructions that change processors' timing behaviors as seen in Listing <ref>.
Moreover, existing fuzzers lack coverage feedback to demonstrate the timing behaviors covered. Providing such metrics can help designers decide to tape out.
To address this challenge, we develop a specialized mutation algorithm that generates data-dependent instructions.
We then use paths of each module's MEG as the timing coverage metric and instrument the DUT to provide coverage feedback.

§.§ The  Framework

To address the challenges discussed in Section <ref>, we develop
that comprises of three major modules: Seed Generation, Vulnerability Detection, and Vulnerability Localization, as shown in Figure <ref>.

Seed Generation.  first uses the Seed Generation module that contains a coverage-feedback fuzzer <cit.> to explore design spaces guided by the fuzzer's internal code-coverage metric. The fuzzer utilizes the Input Generator to generate input instructions, which are then simulated in the fuzzer's internal DUT Simulation unit. The Feedback Engine calculates the code-coverage metric of this input. Based on this metric, the Code Coverage Mutator mutates the input instructions to improve the coverage. The Input Database records various fuzzer-generated inputs and the corresponding code-space covered.

Vulnerability Detection. Based on the Feedback Engine,  identifies a sequence of instructions that explore new design spaces as seeds and sends them to the Vulnerability Detection module.
The  Operands mutator in the Vulnerability Detection module mutates the data in the instruction sequence to trigger varying timing behaviors (See Section <ref>). These mutated instruction sequences are simulated in the DUT Simulation unit of the Vulnerability Detection module.
The Leakage analyzer then compares simulation traces and detects timing vulnerabilities (See Section <ref>).

Vulnerability Localization.
invokes the Preprocessor in Vulnerability Localization to extract  of modules (See Section <ref>) and instruments potential timing behaviors based on the .
For the timing vulnerabilities identified by the Leakage analyzer,  invokes the Diagnozer to pinpoint the cause of these timing vulnerabilities (See Section <ref>). The Coverage analyzer collects simulation traces of all inputs from the Vulnerability Detection module and calculates the timing behaviors covered.

The  framework repeats these steps until there is a timeout, or the fuzzer and Operand mutator completely cover the timing behaviors of the DUT.

§.§ Extracting Micro State Transitions

In this section, we elaborate on the MEG used to address challenge <ref>. Using a Preprocessor,  parses the RTL code of a given design to generate its MEG representation. Each node in the MEG represents an event corresponding to an element in the RTL, while an edge indicates that there exists an event on the parent node that can trigger a change in the value of the child node. Edges between nodes are also annotated with conditions required to trigger the event and the RTL line number which causes the dependency between the event. Nodes in the MEG can be categorized into sequential nodes or combinational nodes corresponding to the sequential or combinational nature of the hardware element it represents <cit.>. Formally, we define a MEG as:

Given the RTL of a module $D$ in a DUT, the corresponding micro-event graph is defined as $\mathbb G(D) = ( S, \Sigma)$, where the nodes are denoted by $ S=\{s_1,s_2,\cdots ,s_n\}= \{ S_q \cup   S_c \cup  S_I \cup I \cup O\}$ and include all elements in $D$; $  S_q$ and $  S_c$ represent the sequential and combinational elements respectively; $S_I$ represent external modules instantiated in $D$; $I$ and $O$ are the set of inputs and outputs respectively to the module $D$. The set $\Sigma$ represents the edges in the graph, $\mathbb G$, such that $(s_i,s_j) \in \Sigma$ if and only if a change in $s_i$ can trigger a change in $s_j$.

[language=Verilog, label = listing:case_study, caption=Simplified Verilog code of cache set protocol (refer Figure <ref>).,style=prettyverilog,float,belowskip=0pt,aboveskip=0pt,firstnumber=1,linewidth=, xleftmargin=10pt]Codes/casestudy.tex

Sub-graph extracted from  in Figure <ref> of the cache set protocol case study. The L6, L7, L9, W15, W14 and R10 nodes from Figure <ref> correspond to , , , , ,  respectively.

Consider the cache set protocol example given in Section <ref>, with its corresponding simplified  code as in Listing <ref>.
A sub-graph of its MEG is shown in Figure <ref>, denoting input node  with an incoming edge.
Due to the  statement on Line 4, a transition in the value of  triggers a change in the value of .
To denote this dependency, the graph contains a directed edge from the node  to .
Similarly, the value of  can influence the value of  and  if the condition () on Line 6 holds.
Hence, the edges from   to  and  are annotated with the condition. The sub-instance call on Line 13 corresponds to the dashed node  in the MEG. The accept state from node  indicates that it references an output signal. Appendix <ref> provides a further discussion on the implementation details of MEG.

The Preprocessor parses the RTL description of the design, translating it into the corresponding graphical representation using Algorithm <ref>.  Given an RTL module $D$, the Preprocessor first extracts into $\mathbb G(D). X$ where $X = I, O, S, \Sigma, \text{or } S_I$ corresponds to the set of inputs, outputs, nodes, edges, and sub-instance nodes respectively (Lines 3 and 4).
Finally, the Preprocessor iterates over each line in the RTL, identifies destination signals (Line 6) and operand signals (Line 7), and adds an edge between each operand signal and the destination signal (Line 9). The Diagnozer ( Section <ref>) and Coverage Analyzer ( Section <ref>) of  utilize this MEG for further analysis.

Micro-Event Path. We define a Micro-Event Path (MEP) as a  path that starts at the input node and traces connected nodes until it reaches the output node. Given an input, this path traces the sequence of events triggered in the module. Formally,

A sequence of directed edges, $P = \left \langle (s_{1},s_{2}), (s_{2}, s_{3}), \cdots,(s_{n-1}, s_{n}) \right \rangle$ where  $(s_{i}, s_{j}) \in \Sigma, \forall(i,j)$ and $s_{1} \in I$ and $s_{n} \in O$, is a Micro-Event Path in $\mathbb G(D)$.

Figure <ref> notes two different MEPs from the input node  to the output node .
Each path can be mapped to a path in the FSM in Figure <ref>, but at a finer granularity. In case of a cache hit, the module follows the FSM path  mapped to MEP {}. In case of a cache miss, if the cache set has a free cache line, the module follows the FSM path {} mapped to {}. A comparison of these two differing MEPs indicates the RTL wire  as the hardware element responsible for the divergence in the two paths.  utilizes this information to trace the root cause of the vulnerability, as elaborated in Section <ref>.

§.§ Characterizing Timing Behaviors

Existing hardware fuzzers detect timing vulnerabilities by measuring the execution time of an entire processor through performance counters <cit.>.
, however, requires finer information to  localize the timing vulnerabilities.
Therefore,  computes the execution time taken by each module within the processor. For this purpose, we use simulation of inputs generated by the Seed Generation and mutated by the Operand Mutator.

For each simulation of the DUT, the Simulator generates a set of simulation traces corresponding to each signal within the DUT. A simulation trace is a time series that records all transitions of a signal during an execution.
The Leakage Analyzer then selects the subset of interesting traces that can lead to a vulnerability.
These traces are  snipped at the last clock cycle at which any signal within a selected module instance toggles. The duration of this constrained trace is then computed as the execution time of the module instance. The Leakage analyzer analyses the timing behaviors of each module instance in a DUT to identify the module instance with timing vulnerabilities.

Hierarchical leakage analysis.
Modern processors, however, consist of hundreds of module instances with various inter-module dependencies <cit.>. Analyzing all their timing behaviors is time-consuming and computationally expensive.
Hence, we require a staggered approach for leakage analysis, which prioritizes modules based on their dependencies. A different module-specific execution time indicates that the source of the vulnerability either originates in the current module or a module lower in the hierarchy.
For example, the memory control unit (MCU) controls the data accesses in the cache.
Upon storing the data at a memory address, the cache sends the  signal to the MCU. Thus, if a timing difference is in the cache delaying the  signal, the MCU will also observe the timing difference.

The Leakage Analyzer implements a hierarchical method taking a bottom-up approach. In this approach, we map the dependencies between modules and place these modules into various hierarchical levels such that the lower-level modules are sub-instances of a higher-level module.
The hierarchical leakage analysis is then carried out incrementally from the lowest module to the highest module. For example, in  <cit.> there are 431 module instances, when placed hierarchically they constitute 10 levels. Thus,  analysis starts from the tenth level and moves upwards until the top module. This approach also ensures the detection of timing vulnerabilities in all lower levels before detection in a higher level module instance.

Once the Leakage analyzer identifies a module instance with execution time differences caused by a pair of inputs, it sends the module instance and the corresponding simulation traces to Diagnozer to pinpoint the location of timing differences further.

§.§ Localizing the Source of Timing Vulnerabilities

For a pair of inputs exhibiting a difference in execution time in a particular module instance, the Diagnozer localizes the source of the timing difference within the design RTL. The Diagnozer takes as input two sets of simulation traces, each corresponding to an execution of the DUT with different data inputs. It operates in two phases: (i) identifying the element causing the divergence and (ii) mapping the cause in the RTL source code of the processor.

Identifying the element causing the divergence.
For the given pair of inputs, the Leakage Analyzer generates a set of simulation traces corresponding to each input, $ST_1$ and $ST_2$ for the module under examination, $D$. If each trace in the two sets are exactly identical, then the execution time for the two inputs are equal. On the other hand, if the execution time of the two inputs are different, there exists a subset of the traces within the two sets that differ.
In this subset of simulation traces, the trace which first deviates, corresponds to the combinational element that instigates the timing difference.
Algorithm <ref> shows the process of the Diagnozer. In the first phase, the Diagnozer iterates through every clock cycle of simulation traces and finds the first signals which differ in the two sets of traces (Lines 6,7). It creates the list of signals $temp\_{V_s}$ whose traces first differ between $ST_1$ and $ST_2$.

Mapping the cause in the source code.
In a module, a timing difference occurs because some hardware elements take varying clock cycles based on the input. The Sequential element influences the number of clock pulses for execution.  Hence, to trace the source of the timing difference within the module, the Diagnozer traces dependencies from the identified combinational signals to the sequential nodes in the MEG.

In Algorithm <ref>, this tracing is done by a Breadth First Search to identify the subsequent sequential elements which originate from each signal in $temp\_V_s$. This is stored in the list $V_s$ along with line numbers where the corresponding event on the sequential element is found in the RTL of $D$.

§.§ Fuzzing Microarchitectural State Space

introduces two components Operand mutator and Coverage analyzer to generate inputs for timing vulnerability detection and to monitor timing behaviors explored.

Operand mutator consists of specialized mutation algorithms to generate inputs for detecting timing vulnerabilities in processors.
Detecting vulnerabilities requires changing the DUT's timing behaviors by triggering different microarchitectural state transitions <cit.>.
Moreover, a valid timing side-channel is data/memory-dependent <cit.>.
Therefore, we constrain Operand mutator to mutate only the segments of a test that will change the memory or data values.

Processor fuzzers use sequences of instructions to verify DUTs, as mentioned in Section <ref>. An instruction contains  and  fields <cit.>; both of which cause the microarchitectural state transitions.
The  fields determine the instruction's operation.
Meanwhile, the operand fields provide the source and destination registers (i.e., general-purpose registers (GPRs) and control and status registers (CSRs)) and immediate values/memory addresses.
Some instructions contain immediate memory addresses only (e.g., branch operation instructions).
To generate data/memory-dependent inputs, we constrain Operand mutator to mutate only the immediate values/memory addresses of instructions uniformly at random <cit.>. To further increase the mutation space, we assign random values to GPRs and valid memory addresses during the processor's initialization.

However, replacing the original mutation algorithms, Coverage Mutator, with Operand mutator reduces the fuzzer's efficiency in exploring the design space for timing vulnerabilities.
This is because the mutator will not change the  and register-operands of instructions.
Therefore, to maintain the efficacy of design space exploration and guarantee the effectiveness of timing vulnerability detection simultaneously, we use Coverage mutator to explore design spaces and use Operand mutator to exploit time side-channels near the design spaces explored.
Any tests achieving new code coverage will be identified as seeds for Operand mutator.
For each seed, the Operand mutator will generate multiple data-dependent inputs, aiming to trigger the microarchitectural state transitions that will cause timing differences compared to the seed.

Coverage analyzer monitors timing behaviors covered by mapping microarchitectural state transitions to executed paths.
For a given DUT, various paths exist between the input nodes and output nodes of the corresponding MEG. For an input value to the DUT, tracing the execution path followed and mapping it to the MEP poses a challenge.

To address this challenge, we utilize  Assertion (SVA) properties known as  properties <cit.>.
If an  property evaluates to true for a given input, the DUT enters a stage during simulation when the property holds.
Each graphical path is converted to a  property using the annotated edge conditions and the timing behavior of the node.
The timing behavior of a node depends upon the type of node defined.
Algorithm <ref> shows the process of generating the conditions of a MEP, $P \in \mathbb G(D)$, as the expression of a  property.
As combinational nodes are modeled after combinational logic, events occurring on these nodes complete instantaneously (line 4), while those occurring on sequential nodes complete on the next clock edge (line 6).
If the value of a signal is from other modules, including input signals and signals connected with subinstances, we assume the events will eventually happen (line 8).
Appendix <ref> shows the  properties for MEPs in the example cache set.

Properties representing all possible paths in the MEG corresponding to the module are instrumented in the RTL. The DUT Simulation unit of the Vulnerability Detection module takes as input this modified RTL. The Coverage Analyzer utilizes the results of the resultant assertion report for calculating the coverage of the various graphical paths.

§ EVALUATION

We evaluate  on three most advanced open-sourced processors based on   <cit.> instruction set architecture (ISA).
We first demonstrate the new vulnerabilities detected by  and provide statistical analysis to prove the existence of the timing side channels.
We then leverage the power of  of  to identify the root causes of these vulnerabilities. Finally, we evaluate the timing behaviors covered by fuzzing.

§.§ Evaluation Setup

Benchmark selection. Most commercial processors are protected intellectual properties without available source code.
Thus, we pick the three large (in terms of the number of gates) and widely-used open-sourced processors:  <cit.>,  <cit.>, and  <cit.> from the  ISA.
Most recent hardware security tools are evaluated using these processors <cit.>.
The  and  are more complex compared to the .
They possess advanced micro-architectural features such as out-of-order execution and support single instruction-multiple data (SIMD) execution.

Evaluation environment. We use the industry-standard tool, Synopsys  <cit.> for DUT simulation. We convert timing behaviors of RTL modules into  Assertion (SVA)  properties and instrument them into DUTs.
We use Chipyard <cit.> environment for the processors. We collect the coverage report and simulation traces from  to analyze the timing coverage and timing behaviors, respectively.

Fuzzing setup. We use  <cit.> to generate the seeds for Operand mutator. Other processor fuzzers that generate sequences of instructions as inputs are also compatible <cit.>.
is a state-of-the-art hardware fuzzer that combines fuzzing and formal tools to maximize coverage and speed up design exploration.
is also compatible with various coverage metrics.
We use a combination of branch, condition, and FSM metrics for code coverage.
Branch and condition metrics monitor the combinational logic of DUTs. The FSM metric monitors the sequential logic of DUTs <cit.>.
Therefore, any new points covered by inputs represent at least one new microarchitectural state transition triggered.
We collect these inputs as seeds and use the Operand mutator to generate 200 data-dependent inputs for each seed.
We ran the entire fuzzing process for 72 hours, generating 40k inputs, and repeated it thrice to collect coverage results.

Timing behaviour of detected novel side-channels.

§.§ Detecting Novel Side Channels

This section will discuss 12 new timing vulnerabilities found by . Furthermore, Appendix <ref> contains the proof of concept code for mentioned vulnerabilities.

in  <cit.>. The side channel under consideration pertains to the consecutive execution of the  and  instructions. In Figure <ref>, the operational characteristics of this side channel are graphically depicted across various operand executions. Our analysis revealed median discrepancies of 48 cycles, 35 cycles, and 83 cycles between the three distributions, with a maximum deviation of 101 cycles observed when deliberately selecting operands to maximize the disparity. Establishing a threshold for the median separation facilitates a successful discrimination rate of 100% when distinguishing between binary states 0 and 1.

in  <cit.>. The side channel pertains to the execution of  instruction. Figure <ref> illustrates the operational characteristics of this side channel across multiple operand executions. Notably, our analysis has unveiled median discrepancies of 14 cycles, 39 cycles, and 54 cycles among the three distributions. Furthermore, we have observed a maximum deviation of 56 cycles when deliberately selecting divide by zero to maximize the disparity.
Establishing a threshold for the median separation enables the successful discrimination of binary states 0 and 1 with a 100% accuracy rate. However, our findings indicate that attackers leverage this channel to transmit three states rather than the intended two states by defining two thresholds, achieving a success rate of 91%.

in  <cit.>.  detected this novel side channel when fuzzing  with  instruction.
Figure <ref> shows the operational characteristics of this side channel across multiple instances of operand executions. We demonstrate a median difference of 54 cycles between the two timing behavior distributions. Additionally, when we select zero as a divisor in the  instruction to maximize the timing difference, the maximum deviation is 56 cycles. Attackers can use this channel by
establishing a threshold for the median separation to transmit binary states 0 and 1 with 100% accuracy.

and  in  <cit.>.   detected multiple novel side channels that occur when executing compressed  instructions, i.e.  and .  Zkt contract has classified these instructions as serious security vulnerabilities if the instructions are data dependent <cit.>. The  instruction has the same timing behavior as its compressed version, i.e.,  and causes a timing channel.
Figures <ref>, <ref>, and <ref>, show the operational characteristics of these side channels across multiple instances of operand executions. We demonstrate a median difference of 12 cycles between the two timing behavior distributions.
Selecting a specific value of
zero as the operands of these instructions results in 12 more cycles compared to any other operand values.
Establishing a threshold for the median separation allows for the successful discrimination between binary states 0 and 1 with an accuracy rate of 100%.

§.§ Redetecting Known Side Channels

in  <cit.>.
successfully generated test cases that exposed timing side-channel vulnerabilities related to division instructions (), a vulnerability disclosed in  <cit.> for the  processor.
generated multiple test cases featuring the  instruction, and by systematically mutating the input values during the fuzzing process, it revealed variations in the number of clock cycles required for the  instruction to complete its operation. Further investigation elucidated that when the divisor was bigger than the dividend, the division unit necessitated more time to conclude the division process.

in  <cit.> and  <cit.>.
also identified a timing side-channel associated with Store-Conditional operations, effectively diagnosing timing disparities resulting from the presence of the  bit in the data cache implementation.
The vulnerability was discovered in  <cit.> for the  and  processors.
The test cases feature a  instruction containing at least one subsequent load instruction.
Through the mutation of these test cases, we were able to detect timing discrepancies when the load/store module attempted to access an address not present in the cache. Subsequently, the Diagnozer of  pinpointed the root cause of this timing difference, attributing it to the  bit that was set by the Store-Conditional instruction for a cache line.

§.§ Pinpointing the Locations of Side Channels

We apply Diagnozer (See Section <ref>) to identify the root causes of detected timing vulnerabilities (See Sections <ref>, <ref>). We describe, in detail, the Diagnozer results for two novel and two known vulnerabilities. The results for all detected vulnerabilities are summarized in Table <ref>.

[language=Verilog, label = listing:div_cva, caption=Source location of  in  <cit.>.,style=prettyverilog,float,belowskip=0pt,aboveskip=0pt,firstnumber=1, escapechar=%,linewidth=, xleftmargin=25pt]Codes/tv_location/div_cva.tex

in  <cit.>.
In , given the instruction sequence in Listing <ref>, the Diagnozer identifies the source of the vulnerability in module   in the lines highlighted in Listing <ref>. The first phase of the Diagnozer identifies 27 signals as the instigating signals, while the second phase pinpoints that these signals change the values of 8 sequential signals.

Compressed Instructions in  <cit.>.
Given two trace files corresponding to the instruction sequence in Listing <ref> the first phase of the Diagnozer identifies the sources of these vulnerabilities in the  module. The exact RTL lines are as highlighted in Listing <ref>. Though the  module does not have a sequential component, the effects of its outputs are propagated to the inputs of the  thereby influencing further execution.

in  <cit.> and  <cit.>.
Given two trace files corresponding to the instruction sequence in Listing <ref>, the Diagnozer identifies the source of this vulnerability in  <cit.> and  <cit.> at different lines in module  . The vulnerability is localized to the sequential elements  in both processors (refer Table <ref>).

Division by zero in  <cit.>,  <cit.>,  <cit.>.
Given two trace files corresponding to the instruction sequence in Listing <ref> with the divisor set to 0, the Diagnozer identifies the sources of this vulnerability in , ,  as shown in Table <ref>.
Though the root cause is localized to the same module in  and , the pinpointed lines differ. While in , the divide by zero vulnerability is localized to module .

Hence, though the same timing vulnerability can affect multiple DUTs, due to the differences within the microarchitectural design, the source of the vulnerability in the RTL code differs. Furthermore, consider the two division-related vulnerabilities detected in  <cit.>. Although these vulnerabilities affect the same module (), the source of the vulnerabilities within the module differs. Hence, the automated localization of vulnerability sources performed by  is beneficial and efficient.

Timing coverage of RTL modules in  <cit.>,  <cit.>, and  <cit.>. The black line indicates the variation in coverage offered by 40K differing inputs.

§.§ Coverage Analysis

We use Coverage analyzer to monitor timing behaviors explored by inputs from Operand mutator.
Coverage analyzer converts paths of  of an RTL module into  properties and instrument these properties in to DUT.
After simulation, Coverage analyzer collects assertion results to calculate the timing behaviors covered (See Section <ref>).
Figure <ref> shows the coverage achieved in various modules of the three benchmarks.
Due to the space limitation, we only show the coverage of 10 modules with the highest total number of timing coverage points.
On average,  achieves $39.57\%$, $33.16\%$, and $20.20\%$ coverage on  <cit.>,  <cit.>, and  <cit.>, respectively.

Since we emphasize covering timing behaviors, our Operand mutator generates 200 inputs for each seed generated by the coverage-feedback fuzzer.
Thus, of the 40k inputs  took to achieve the above overall coverage, most inputs target triggering timing behaviors in the DUT while only the 200 seeds explore the design space of DUT.
The overall coverage of  can be increased by using more seeds from coverage-feedback fuzzer and running the fuzzer for more time.
Also, many coverage points are left uncovered due to the multiple configurations of DUT.
For example,  has parameters to configure its float-point unit to support operations from 8-bit to 128-bit <cit.>.
fuzzes  in its default configuration where
uses 64-bit operations.
Hence, all other operations' timing behaviors are uncoverable. 's floating-point unit <cit.> and 's branch predictor <cit.> have similar configurations. Therefore, these configurations reduce the overall coverage.

§.§ Exploitability of Detected Vulnerabilities

In this section, we discuss the potential exploitations of the vulnerabilities detected by  as presented in Section <ref>. Such vulnerabilities can be exploited for information leakage across diverse scenarios as described below.

Covert Channels. A timing covert channel breaks the process isolation guarantees provided by the hardware. A sender process can perform operations influencing the execution time of a receiver process, which infers a bit value based on this observed timing. For instance, the -based vulnerability detected by  in  <cit.> can be employed to design a covert channel based on the timing differences. However, realizing such a covert channel requires the communicating processes to execute on the physical core using hyperthreading features which are unavailable on our evaluation processors<cit.>.

Speculative Execution Attacks. Such attacks happen in out-of-order processors when, during the rolled back of speculatively executed instructions, processor leave their footprints on the micro-architectural components such as the cache. This has been exploited in several popular attacks  <cit.>. An attacker can formulate a similar attack with the vulnerabilities found by . For instance, with speculative execution support on , a combination of the load and time-dependent instructions(any instruction that is detected by , See Section <ref>) can utilized to encode sensitive data into the cache, which a cache timing attack can then glean. However, the current state of the evaluated processors is limited to non-speculative execution.

Attacking Library Implementations. An adversary can exploit the timing differences based on the operand values discovered by   to glean sensitive information from popular libraries in cryptography or machine learning domains. For such an attack, the library implementation is required to have the same instruction flow, e.g.,  followed by  for  <cit.> or  for <cit.> with the operand dependent on a secret value.

§ RELATED WORK

Existing state-of-the-art techniques for timing side-channel vulnerability detection primarily employ
formal approaches  <cit.> and fuzzing  <cit.> techniques. However, these approaches still exhibit critical shortcomings. In contrast to , these approaches fail to pinpoint the root causes of the detected timing vulnerabilities without manual efforts that take a long time. Thus, the mitigation based on these techniques is coarse-grained rendering them inefficient in terms of the computational resources in DUT. Further, the coverage metrics used by these solutions, such as hardware performance counters or code coverage <cit.> do not capture the timing behaviors of the DUT, resulting in uncertainty prior to tape-out <cit.>. In this section, we discuss these perform a comparative analysis with , as illustrated in Table <ref>.

Formal approaches for timing vulnerability detection.
<cit.> is a white-box approach to detect side channels in RISC-V RTL designs using SAT-based bounded model-checking. However, such an approach is not scalable to complex processor designs. Alternatively,  <cit.>
employs micro-happens-before graphs to analyze transient execution vulnerabilities and timing side channels. It detects patterns within these graphs to assess the susceptibility of architectural models to timing side-channel threats. In contrast to our methodology,  relies on matching patterns of vulnerable instructions, while
is semantically oriented and automatic.

Fuzzing-based approaches for timing vulnerability detection.
<cit.> is a black-box fuzzer that identifies timing vulnerabilities in commercial processors by brute-forcing different combinations of instruction sequences. However, to reduce the search space, it limits the instruction sequence length to one, leaving vulnerabilities requiring multiple instructions <cit.> or specific operands <cit.> to trigger undetected.
and  <cit.>
identify combinations of instructions that trigger microarchitectural timing side-channel leakages by deriving a leakage template. However,  requires manual efforts to specify mutation algorithms and potential behaviors of a DUT to generate this template. Further, it is limited to the existing cache module and cannot locate them in the DUT.

<cit.> is a grey-box fuzzer that detects the existence of timing vulnerabilities in processors at the RTL.
It generates combinations of instructions to identify cycle-accurate microarchitectural timing side-channels.
However, replacing instructions can create additional architectural differences, such as differences in general-purpose registers, resulting in a high rate of false positives. Further, SIGFuzz suffers from limitations in pinpointing vulnerability locations and coverage metrics as the black-box approaches.

addresses these limitations of existing works by providing a novel white-box fuzzer with static analysis to detect and pinpoint timing vulnerabilities in processors enabling fine-grained mitigations. Further,  is scalable to complex designs and end-to-end automated with a specialized coverage metric for timing behaviors.

§ DISCUSSION

Use of Code coverage mutator and Operand mutator.
employs both the Code coverage mutator and the Operand mutator to explore the design space and generate data-dependent inputs, respectively. In our experiments, we set up the use of these two mutators heuristically. The determination of their utilization is an optimization problem that can aid the efficacy of vulnerability detection. We can model the probability of Operand mutator covering a timing behavior <cit.>. When this probability falls below a threshold, the Code coverage mutator can be called to generate new seeds. However, such an analysis is beyond the scope of this paper.

Port scanning vulnerabilities.
Contention for a port in the architecture can cause execution delays, enabling attackers to create a high-resolution time side-channel by scanning for port contention <cit.>. However, these attacks depend on the high bandwidth of shared resources and, primarily, the simultaneous multithreading architecture <cit.>.
The current open-sourced benchmarks lack such advanced architectures <cit.>, and hence detecting port scanning is outside the scope of .

§ CONCLUSION

Recent hardware fuzzers have showcased their potential to identify timing vulnerabilities in intricate designs, such as processors.
However, the existing black-box or grey-box fuzzing approaches fall short in pinpointing the precise location or root cause of timing vulnerabilities.  Further, these approaches lack the necessary coverage feedback mechanisms for the exploration of timing behaviors.
Addressing these gaps, we develop , the first approach that combines white-box fuzzing with static analysis.
Its primary objectives are not only to accurately determine the locations of timing vulnerabilities but also to evaluate the timing behaviors.
has successfully detected 12 new timing vulnerabilities and all previously known ones in open-source processors. Moreover, it pinpoints the root causes of these vulnerabilities. This opens up novel avenues in vulnerability detection and timely mitigation in processors.

§ ACKNOWLEDGEMENT

Our research work was partially funded by Intel's Scalable Assurance Program, Deutsche Forschungsgemeinschaft (DFG) – SFB 1119 – 236615297, the European Union under Horizon Europe Programme – Grant Agreement 101070537 – CrossCon, the European Research Council under the ERC Programme - Grant 101055025 - HYDRANOS, Lockheed Martin Corporation, and the Centre for Hardware Security Entrepreneurship Research and Development (C-HERD) project, Ministry of Electronics and Information Technology (MEiTY), Government of India.
This work does not in any way constitute an Intel endorsement of a product or supplier. Any opinions, findings, conclusions, or recommendations expressed herein are those of the authors and do not necessarily reflect those of Intel, the European Union, the European Research Council, Lockheed Martin Corporation, the US Government, or the India Government.

§ APPENDIX

§ IMPLEMENTATION DETAILS OF

Section <ref> explains the concept of a  (MEG).
However, when implementing the strategy for real RTL designs, the syntaxes of hardware description languages (HDLs), such as  and  <cit.>, introduce more implementation challenges. Based on the example shown in Listing <ref>, we created a more complicated cache set with multiple ways as shown in Listing <ref>.
We use the cache set as a case study to explain the implementation details of MEGs. Figure <ref> shows the sub-graph of the protocol.

[language=Verilog, label = listing:case_study_full, caption=Verilog code of multi-ways cache set protocol.,style=prettyverilog,float,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/fullcasestudy.tex

Sub-graph extracted from  in Listing <ref> of the multi-ways cache set protocol.

Nested branch statements. Except for the fundamental branch statements of HDLs, such as  and ternary (), a register-transfer level (RTL) module also contains nested branch statements.
Since all branch statements must be satisfied to trigger the operations under the most nested branch statement, we annotate an edge from each signal in those branch statements to the destination signals of the operations.
For example, from line 10 to 12, nested branch statements  and  drive the assignments of the  signal.
Therefore, in Figure <ref>, the condition on the edge () is the conjunction of  and .

Path Explosion:
In certain cases, an event on one component is capable of triggering an event on another component under multiple different conditions. For example, from line 6 to 9, since the cache set has multiple ways, both condition
and  can represent a cache hit.
This results in the existence of four edges from node  to  and . Each is annotated with one condition between the two nodes. The existence of multiple edges between the same pair of nodes causes a path explosion during timing coverage instrumentation as mentioned in Section <ref>.
Consequently, the number of  Assertion (SVA)  properties in the module increases exponentially.
To solve this challenge, we create a disjunction for different conditions on edges joining the same pair of nodes in a path.
Figure <ref> shows the disjunction on edge () and ().

§ SVA  PROPERTIES FOR CASE STUDY

Listing <ref> shows the  property for the graphical paths in the  of the cache case study as shown in Listing <ref>. Section <ref> mentions two Micro-Event Paths from its input  to its output :  and
Among these paths, , , ,  are sequential nodes; the events occurring on these nodes complete on the next clock edge. The value of the  signal is driven by , a subinstance.

[language=Verilog, label = listing:sva_case, caption=SVA  properties for case study.,style=prettyverilog,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/sva_property.tex

§ PROOF OF CONCEPT CODES FOR TRIGGERING DETECTED VULNERABILITIES

This section shows the proof of concept code snippets on triggering various timing vulnerabilities in different  processors.
Listing <ref> shows the code snippets of  side-channel on  <cit.>.
Listing <ref> shows the code snippets of  side-channel on  <cit.>.
Listing <ref> shows the code snippets of  side-channel on  <cit.>.
Listing <ref> shows the code snippets of compressed instruction-based side-channels on  <cit.>.

[language=C, label = listing:boom_divuw_rem_poc, caption= side-channel proof of concept code snippets on <cit.>.,style=customcArianeExploit,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/testcases/boom_divuw_rem_poc.tex

[language=C, label = listing:cva6_divuw_poc, caption= side-channel proof of concept code snippets on <cit.>.,style=customcArianeExploit,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/testcases/cva6_divuw_poc.tex

[language=C, label = listing:cva6_remw_poc, caption= side-channel proof of concept code snippets on <cit.>.,style=customcArianeExploit,float=h!,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/testcases/cva6_remw_poc.tex

[language=C, label = listing:cva6_other_poc, caption= side-channel proof of concept code snippets on <cit.>.,style=customcArianeExploit, float=h!,belowskip=0pt,aboveskip=0pt,firstnumber=1]Codes/testcases/cva6_other_poc.tex

§ LOCATIONS OF SIDE CHANNELS

This section shows the locations of timing vulnerabilities identified by the Diagnozer (See Section <ref>).
Listing <ref> shows the location of Division by zero in  <cit.>.
Listing <ref> shows the location of Division by zero in  <cit.>.
Listing <ref> shows the location of Division by zero in  <cit.>.
Listing <ref> shows the location of  in .
Listing <ref> shows the location of compressed instructions and  in ; nine vulnerabilities share the same root cause.
The results show that the Diagnozer of  can successfully identify the location of timing vulnerabilities in processors.

[language=Verilog, label = listing:div0_boom, caption=Source location of Division by zero in  <cit.>.,style=prettyverilog,float=h!,belowskip=0pt,aboveskip=0pt,firstnumber=1, escapechar=%,linewidth=, xleftmargin=25pt]Codes/tv_location/div0_boom.tex

[language=Verilog, label = listing:div0_rc, caption=Source location of Division by zero in  <cit.>.,style=prettyverilog,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1, escapechar=%,linewidth=, xleftmargin=25pt]Codes/tv_location/div0_rc.tex

[language=Verilog, label = Listing:div0_cva, caption=Source location of Division by zero in  <cit.>.,style=prettyverilog,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1, escapechar=%,linewidth=, xleftmargin=25pt]Codes/tv_location/div0_cva.tex

[language=Verilog, label = listing:div_rem, caption=Source location of  in  <cit.>.,style=prettyverilog,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1, escapechar=%, linewidth=, xleftmargin=25pt]Codes/tv_location/div_rem.tex

[language=Verilog, label = listing:ci_cva, caption=Source location of compressed instructions and  in  <cit.>.,style=prettyverilog,float=h,belowskip=0pt,aboveskip=0pt,firstnumber=1, escapechar=%,linewidth=, xleftmargin=25pt]Codes/tv_location/ci_cva.tex