{'fraction_non_alphanumeric': 0.03855991691828375, 'fraction_numerical': 0.009789026289978268, 'mean_word_length': 4.702160324596996, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 1, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Solver-Aided Constant-Time Circuit Verification

We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to automatically synthesize a minimal set of secrecy assumptions. Xenon further exploits modularity in Verilog code via a notion of module summaries, thereby avoiding duplicate work across multiple module instantiations. We show how Xenon's assumption synthesis and summaries enable the verification of a variety of circuits including AES, a highly modular AES-256 implementation where modularity cuts verification from six hours to under three seconds, and ScarV, a timing channel hardened RISC-V micro-controller whose size exceeds previously verified designs by an order of magnitude.


Introduction
Timing side-channel attacks are no longer theoretical curiosities. Over the last two decades, they have been used to break implementations of cryptographic primitives ranging from public-key encryption algorithms [25,53,77], to block ciphers [22,61], digital signature schemes [60], zero-knowledge proofs [33], and pseudorandom generators [32]. This, in turn, has allowed attackers to break systems that rely on these primitives for security-for example, to steal TLS keys used to encrypt web traffic [25,32,77], to snoop and forge virtual private network traffic [60], and to extract information from trusted execution environments [24,32,33,76].
The gold standard for preventing timing side-channel attacks is to follow a discipline of constant-time or data-oblivious programming [1, 15,21,28,34,78]. At its core, this discipline ensures that (1) secret data is not used as an operand to variable-time instructions (e.g., floating point operations like division [18,19,54,64]) and (2) the program's control flow and memory access patterns do not depend on secrets.
But for the constant-time discipline to be effective, it is crucial that the constant-time property be preserved by the underlying hardware. For example, an instruction that is deemed constant-time needs to indeed produce its outputs after the same number of clock cycles, irrespective of operands or internal state. Similarly, given that control-flow and memory access patterns are public, i.e., free of secrets, a CPU's timing must indeed be secret-independent.
Unfortunately, simply assuming that hardware preserves constant-time doesn't work. Incorrect assumptions about the timing-variability of floating-point in-structions, for example, allowed attackers to break the differentially private Fuzz database [49]. Attempts to address these attacks (e.g., [65]) were also foiled: they relied on yet other incorrect microarchitectural assumptions (e.g., about the timing-variability of SIMD instructions) [54]. Yet more recently, hardware crypto co-processors (e.g., Intel and STMicroelectronics's trusted platform modules) turned out to exhibit similar secret-dependent timing variability [60].
A promising path towards eliminating such attacks is to formally verify that our hardware preserves the constant-time property of the software it is executing. Such verification efforts, however, require tool support. Unfortunately, unlike software verification of constant-time, which has had a long history [20], constant-time hardware verification is still in its infancy [27,46,78]. As a result, existing verification approaches like Iodine [46] fail to scale to realistic hardware. This has two fundamental reasons. First, existing tools do not help when verification fails, as is inevitable, since hardware circuits only preserve constanttime execution under very specific secrecy assumptions that describe which port and wire values are public or secret. Currently, upon failure, the user must undertake the tedious and time consuming task of determining, whether the circuit is indeed leaky (i.e., variable-time), or whether it is missing additional secrecy assumptions, which the user then has to explicate. In our experience, this process takes up the overwhelming majority of time spent on the verification effort. Second, current methods fail to exploit the modularity that is already explicit at the register transfer level. Hence, they duplicate verification effort across replicated modules which leads to a blow up in verification time.
In this paper, we present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. We develop Xenon via four contributions.
1. Counterexamples. To help users understand verification failures, we introduce the notion of constant-time counterexamples ( § 4.1). A counterexample highlights the earliest point in the circuit where timing variability is introduced; this simplifies the task of understanding whether a circuit is variable-time by narrowing the user's attention to the root cause of the verification failure (and a thereby small fraction of the circuit). To compute counterexamples, Xenon leverages information extracted from the failed proof attempt. In particular, the solver communicates (1) for which variables (i.e., registers and wires) it was able to prove the constant-time property and (2) in which order the remaining variables became non-constant time. This allows Xenon to break cyclic datadependencies which cause a chicken-and-egg problem that is hard to resolve when assigning blame manually.
2. Assumption Synthesis. To help the user resolve the verification failure, Xenon uses the counterexample to synthesize a suggested fix. For example, Xenon may find a constant-time counterexample for a processor pipeline where the two different runs may execute two different ISA instructions (say, addition and division) which take different numbers of clock cycles. Yet, the execution of each instruction (for any inputs) may be constant-time. Xenon uses the counterexample to synthesize a minimal candidate set of secrecy assumptions (e.g., that any two executions have the same, publicly visible sequence of instructions) which address the root cause of the verification failure ( § 4.2). The user then decides either to accept the candidate assumption, or, if they do not match their intuition for the intended usage of the circuit, reject them, in which case Xenon computes an alternative. Internally, Xenon computes candidate assumptions, via a reduction to integer linear programming [63].
3. Modular Verification. Finally, in order to scale both verification and counterexample generation to larger and more complex hardware, we introduce a notion of module summaries ( § 3). Module summaries succinctly capture the timing properties of a module's input and output ports at a given usage site. By abstracting inessential details about the exact computations performed by the module and focusing solely on its timing behavior, Xenon produces fewer and more compact constraints.

Evaluation.
We implement Xenon and evaluate the impact of counterexamples, assumption synthesis and modularity on the verification of different kinds of hardware modules ( § 6). We find that Xenon's counterexample synthesis dramatically reduces the number of potential error locations a user has to inspect in order to understand the root-cause of the violation (to 6% of its original size) and that Xenon is highly effective at suggesting useful assumptions-on average 81.67% are accepted by the user. Similarly, our evaluation shows that module summaries are key to reducing verification times for certain hardware designs (e.g., for AES-256 crypto core summaries reduced the verification time from six hours to a three seconds). Overall, we find that Xenon's solver-aided verification process drastically reduces verification effort (e.g., manually verifying the largest benchmark of [46] took us several minutes instead of days) and is key to scaling verification to realistic hardware: the SCARV side-channel hardened RISC-V core [4] we verify is an order of magnitude larger than the RISC-V cores verified by previous state-of-the-art tools.

Overview
We start by reviewing how to specify and verify the absence of timing channels in Verilog hardware designs ( § 2.1), show how existing techniques fail to scale on real-world hardware designs, as these designs are often only constant-time under additional secrecy assumptions which are tedious to derive by hand ( § 2.2), sketch how Xenon helps finding secrecy assumptions automatically ( § 2.3), and finally discuss how Xenon exploits modularity ( § 2.4).

Verifying Constant-Time Execution of Hardware
Lookup Circuit. Figure 1 shows the code for a Verilog module, which implements a lookup table by case-splitting over the 8-bit input value. This module executes in constant-time: even if input in contains a secret value, producing output out takes the same amount of time (one clock cycle), irrespective of the  Figure 1 showing values and liveness-bits input (in) and output (out). X represents an undefined value.
value of in, and therefore, an attacker cannot make any inference about the value of in by observing the timing of the computation.
Specifying Constant-Time Execution. Figure 2 makes this intuition more precise, using a recent definition of constant-time execution for hardware [46].  Instead of tracking timing indirectly through information flow [57,71,80] the definition uses a direct notion of timing. 3 The Figure shows two runs of module S: one for input 8 h00 and one for input 8 hff. We want to track how long it takes for the two inputs, issued at cycle 1 to pass through the circuit and produce their respective outputs. For this, we put a "tracer" on the inputs by assigning a liveness-bit to each register. For some register x, we set its liveness-bit x • to ⋆, if x has been influenced by the input at initial cycle 1 (we say x is 1-live) and •, otherwise. Figure 2 shows how liveness-bits are propagated through the circuit. Initially, in both executions, the input is 1-live and the output is not. In cycle 2, both outputs 1-live due to the case-split on the value of in. Assuming that an attacker can observe the liveness-bits of all outputs, here, register out, the attacker cannot distinguish the two executions, and we can conclude that the pair of executions is indeed constant-time.
Verifying Constant-Time Execution. In order to show constant-time execution, not only for the two runs in Figure 2, but for the whole circuit, Xenon proves that for any pair of runs, that is, for any pair of inputs, and any initial cycle, the constant-time property holds. Xenon's solver achieves this by constructing a product circuit [46] whose runs correspond to pairs of runs-called left and right -of the original circuit. In this product, each original variable x has two copies x L and x R that hold the values of x in the left and right runs, re-spectively. Following [46], Xenon's solver uses the product circuit to synthesize invariant properties of the circuit. For example, let's define that a variable x is constant time (and write ct(x)), if for any pair of executions, its liveness-bit in the left execution x • L is always the same as its liveness-bit in the right execution x • L , i.e., x • L = x • R always holds, for all initial cycles t. Xenon synthesizes the following invariant on the module which proves constant-time execution, under the condition that module inputs are constant-time: ct(in) ⇒ ct(out).  Unfortunately, unlike the simple lookuptable from Figure 1, real world circuits are typically not constant-time, in an absolute sense. Instead, when carefully designed, they are constant-time under specific secrecy assumptions detailing which circuit inputs are supposed to be public (visible to the attacker) or secret (unknown to the attacker). Thus, verification requires the user to painstakingly discover secrecy assumptions through manual code inspection, which can be prohibitively difficult in real world circuits.

Real
A Pipelined MIPS Processor. We illustrate the importance of these assumptions using the program in Figure 3 which shows a a code-fragment taken from one of our benchmarksa pipelined MIPS processor [8]. If the reset bit rst is set, the processor sets a number of registers to zero (Line 18). Otherwise, the processor checks whether the pipeline is stalled (Line 21) and either forwards the current instruction from the instructionfetch stage to the instruction-decode stage (Line 28) and advances the program counter (Line 29), or stalls by reassigning the current values (Line 22).
The Pipeline is not Constant-Time. When using the processor in a security critical context, we want to make sure that it avoids leaking secrets through timing, i.e., that it is constant-time. Unfortunately, our example pipeline is not constant-time without any further restrictions on its usage. For example, the execution time for a given instruction depends on whether or not the pipeline is stalled before the instruction is retired. This is illustrated in Figure 4. We model an attacker that can measure how long an instruction takes to move through the pipeline, i.e., from source IF pc to sink WB reg (this is specified through the annotation in Line 1 of Figure 3). Such an attacker can distinguish the two runs in Figure 4, as the liveness-bits of WB reg differ in cycle 3. This timing difference lets the attacker make inferences about the control-flow of the program which is executed on the processor, and therefore any attempt to verify constant-time execution results in a failure.

Automatically Finding Secrecy Assumptions
We may, however, still be able to use this processor safely, if we can find a suitable set of secrecy assumptions. For example, we could assume that register Stall is public (i.e., free of secrets, which can be formally expressed by the assumption that Stall L = Stall R always holds). In this case, the timing difference in Figure 4 would only leak information that the attacker is already aware of. However, Stall is defined deep inside the pipeline and therefore, it is hard to translate this assumption into a restriction on the kind of software i.e., code we are allowed to execute on the processor. Instead, we want to phrase our assumptions in terms of externally visible computation inputs. For example, restricting program counter IF pc to be public directly translates into the obligation that the executed program's control-flow be independent of secrets. To achieve this using existing technology, the engineer first has to manually identify that the timing variability is first introduced in variable ID instr (Line 28) due to a control dependency on Stall. They then need to inspect how Stall is set (Line 13) and painstakingly trace the definitions which may involve complex combinatorial logic (excerpt starting in line Line 5) and circular data-flows in order to identify a promising candidate register, such that marking the register as public will render the circuit constant-time. Counterexamples like Figure 4 are often of little help as they are hard to interpret, and fail to focus attention on the relevant parts of the circuit.

Solver Aided Verification:
ÒÓÒ's Interactive Loop. Xenon drastically simplifies this time consuming process through a solver-aided workflow that helps finding secrecy assumptions automatically.
Step 1. First, we start with an empty set of secrecy assumptions and run Xenon on the pipeline. The verification fails, as the pipeline is not constant-time, however, Xenon displays the following prompt to guide the user towards a solution.

> Mark reset as PUBLIC? [Y/n]
The user either says Y indicating that reset should indeed be considered public, or else responds N which tells Xenon to exclude the variable from future consideration (i.e., not suggest it in future). Suppose that we follow Xenon's advice, and click Y: this marks reset public and re-starts Xenon for another verification attempt.
Step 2. Next, Xenon suggests marking M PCSrc as public. M PCSrc acts as a flag that indicates whether the current instruction in the memory stage contains an indirect jump. But since M PCSrc's value depends on register values (i.e., M PCSrc is set depending on whether the output of the execute phase is zero) assuming that M PCSrc is public would lead to assumptions about the datamemory which we wish to avoid. We therefore tell Xenon to exclude it in future verification attempts and restart verification.
Step 3. Restarting verification causes Xenon to suggest candidate variables IF pc and IF pcn, the program counter of the fetch stage and its value in the next cycle, respectively. We mark IF pc as public as this directly encodes the assumption that the program's control flow does not depend on secrets. In addition, Xenon infers a second set of usage assumptions which details the parts of the pipeline that have to be flushed on context switches. These assumptions would otherwise have to be supplied by the user as well. Finally, Xenon proves that the resulting program executes in constant-time and therefore concludes the verification process.
Counterexamples. While synthesizing candidate assumptions, Xenon internally computes a constant-time counterexample which consists of the set of variables that have lost the constant-time property earliest. While the user can simply follow Xenon's suggestions without further investigating the root cause of the violation, we find that-if the user chooses to do so-the counterexample often helps to further understand why the circuit has become non constant-time. For example in our simple pipeline, Xenon returns a counterexample consisting only of variable ID instr for all three interactions. Indeed, inspecting the parts of the circuit where ID instr is assigned focuses our attention on the relevant parts of the circuit, that is, the conditional assignment of ID instr under rst (Line 18) and under Stall (Line 21). We discuss how Xenon computes counterexamples using an artifact extracted from the failed proof attempt in § 4.1, and how Xenon synthesizes secrecy assumptions via a reduction to integer linear programming in § 4.2.

Real World Circuits Aren't Not Small
While Xenon's solver-aided verification loop significantly reduces the time the user has to spend on verification efforts, large real world circuits often also present a challenge for to solver. This is because computing invariants requires a whole program analysis. Hence, the efficiency of our solver crucially depends of the size of the circuit we are analyzing, and therefore verification might become prohibitively slow on large designs. Consider, for example, the AES-256 benchmark from [10]. Fig. 5 depicts the dependency graph of its modules, where each node m represents a Verilog module, and we draw an edge between modules m and n, if m instantiates n. Each edge is annotated with the number of instantiations. Even though there are only ten modules, the total number of module instantiations is 789. This, in turn, causes a blowup in the size of code Xenon has to verify. Even though the sum of #LOC of the modules is only 856, inlining module instances causes this number to skyrocket to 135194 rendering verification all but intractable. (In fact, Xenon does manage to verify the naive, inlined circuit, however, verification takes over 6 hours to complete). Fortunately, we can avoid this blowup by exploiting the modularity that is already apparent at the Verilog level. We illustrate this process using module S from Figure 1.
Module Summaries. Since the value of out only depends on in, we can characterize its timing behavior as follows: the module output out is constant-time, if module input in is constant-time.
We can formalize this in the following module summary, which we Xenon computes automatically: ct(in) ⇒ ct(out). Instead of inlining the module, we can now use its summary thereby eschewing the code explosion and enabling efficient verification. The code in Figure 6 shows an instantiaton of module S in module S4. Instead of inlining S at its four instantiaton sites S_0 to S_3, Xenon uses the single module summary to compute a correctness proof, which only takes 3 seconds.

Modular Constant-Time Verification
We now formalize the concepts introduced in the overview. We first review a formal definition of constant-time execution for hardware circuits ( § 3.1) and its translation to Horn-clause verification conditions ( § 3.2). We then show how to modularize this naive encoding via summaries ( § 3.3).

Defining Constant-Time Execution
Configurations. Configurations represent the state of a Verilog computation. A configuration Σ (P, σ, θ, c, t, Src) is made up of a Verilog program P (say, the processor in Figure 3), a store σ, a liveness map θ, current clock cycle c ∈ N, initial clock cycle t ∈ N and, finally, a set of sources Src ⊆ Vars. Store σ ∈ Vars → Z maps variables Vars (registers and wires) to their current values; map θ ∈ Vars → {⋆, •} maps variables to liveness-bits; cycle t marks the starting-cycle of the computation we want to track and finally Src identifies the inputs of the computation we are interested in.
Transition relation. Transition relation ∈ (Σ × Σ) encodes a standard Verilog semantics which defines how a configuration is updated from one clock-cycle to the next. We omit its definition, as it is not needed for our purposes, but formal accounts can be found in [46,47,80]. In addition to updating the store and current cycle, the transition relation updates the liveness map θ by tracking which variables are currently influenced by the computation started in t. At initial cycle t, our transition relation starts a new computation by setting the liveness-bits of all variables in Src to ⋆, and those of all others variables to •.
Example. Consider again Figure 2. The Figure depicts two runs π L and π R of length 3 with respect to initial cycle 1 and source {in} of the program in Figure 1. Columns in and out show store(π, i)(in) and store(π, i)(out), for π ∈ {π L , π R } and i ∈ {1, 2}. Similarly, columns in • and out • show live(π, i)(in) and live(π, i)(out), for π ∈ {π L , π R }, and i ∈ {1, 2}. The Figure omits the initial state at cycle 0, where all liveness-bits are set to •.
Flushed, Constant-Time, Public. For two runs π L and π R of length n, we say that variable v is flushed, if store(π L , 0) = store(π R , 0), we call v public, if store(π L , i) = store(π R , i), for i ∈ {0, . . . , n − 1} and finally, we call v constanttime, if live(π L , i) = live(π R , i), for i ∈ {0, . . . , n − 1}. Secrecy Assumptions. A set of secrecy assumptions A (Flush, Pub) consists of a set of variables Flush ⊆ Vars that are assumed to be flushed in the initial state, and a set of variables Pub ⊆ Vars, that are assumed equal throughout. A pair of runs π L and π R of length n, satisfy a set of assumptions A, if, for each v ∈ Flush, v is flushed, and for each v in Pub, v is public. We describe how Xenon synthesizes secrecy assumptions in § 4.
Constant-Time Execution. We now define constant-time execution with respect to a set of sinks Snk ⊆ Vars, sources Src, and assumptions A. We say that a program P is constant-time, if for any initial cycle t and any pair of runs π L and π R of P with respect to t and Src of length n that satisfy A, and any sink o ∈ Snk, o is constant-time.
Example. Consider again Figure 2. If we assume that variables in cycle 0 have the same value as in cycle 1, then out is flushed while in is not. Neither in, nor out are public, but both are constant-time. As out is constant-time in all runs, the program in Figure 1 is constant-time with respect to the empty set of assumptions and sink {out}. In Figure 4, none of the variables are public or constant-time, however, the program in Figure 3 can be shown to be constanttime with Pub = {IF pc, reset}.

Verifying Constant-Time Execution via Horn Constraints
To verify constant-time execution of a circuit, we mirror the formal definition of constant-time execution in a set of Horn clauses [23]. We start with the naive, monolithic encoding and discuss how to make it modular in § 3.3. At high level, the constraints i) issue a new live instruction at a non-deterministically chosen initial cycle t, and ii) ensure constant-time execution by verifying that the liveness-bits for each sink are always the same, in any two runs. The clausesshown in Figure 7-encode standard verification conditions over an invariant inv (vs L , vs R , c, t) of the product circuit, where vs ranges over all variables in the circuit and their respective liveness bits, and c and t are the current and initial cycles, respectively. We now describe the verification conditions in more detail.
Initial States and Transition Relation. Formula init (vs L , vs R ) describes the product circuit's initial states and requires all liveness-bits to be set to •. To ensure that the proof holds for any initial cycle, init does not constrain t. Formula next encodes the transition relation of the product circuit. Like , next sets liveness-bits of all sources to ⋆ at clock cycle t. Importantly, constructing next requires inlining all modules and therefore can lead to large constraints that are beyond the abilities of the solver.
Assumptions. For a set of assumptions A (Flush, Pub), we construct formulas flush and pub, both of which require the variables in their respective sets to be equal in the two runs. We let flush Horn Constraints & Solutions. We then require that the invariant holds,initially (init ), assuming all variables in Flush and Pub are equal in both runs; that the invariant is preserved under the transition relation of the product circuit, assuming that public variables are equal in both runs (cons), and finally, that the liveness-bits of any sink are the same in both runs (ct ). These constraints are then passed to an off-the-shelf solver [9] yielding a formula which, when substituted for inv , makes all implications valid and thus proves constant-time execution.
Proof Artifacts. While attempting to construct the invariant, the solver's internal representation keeps track of i) the set of variables which it was able to prove to be constant-time and public and ii) the order in which the remaining variables lost the respective properties. In case of a failed proof attempt, the prover communicates these artifacts to the assumption synthesis part of Xenon, which in turn uses them to identify the verification failure, as we will discuss in the next section.

Finding Modular Invariants
Naively, constructing next requires all the code to be in a single module. However, this can yield gigantic circuits whose Horn clauses are too large to analyze efficiently. To avoid instantiating the entire module at each usage site, Xenon constructs module summaries which concisely describe the timing relevant properties of the module's input and output ports.
Per-Module Invariants and Summaries. Instead of a single whole program invariant inv , the modular analysis constructs a per-module invariant inv m , and an additional summary sum m , for each module m. The summary only ranges over module inputs and outputs, and respective liveness-bits (io) and needs to be implied by the invariant, i.e., we add a clause stating that inv m (vs L , vs R , t) ⇒ sum m (io L , io R , t). The analysis produces the same constraints as before, but now on a per-module basis, that is, we require module invariants to hold on initial states (init ), and be preserved under the transition relation (cons), but, instead of using the overall transition relation next we use a per-module transition relation next m . It may now happen that next m makes use of a module n, but instead of inlining the transition relation of n as before, we substitute it by its module summary sum n , thereby avoiding the blowup in constraint size. Finally, we restrict sources and sinks to occur at the top-level module, and add a clause requiring that any sink has the same liveness-bits in both runs (ct ). The summaries are also used to modularize our assumption synthesis algorithm § 4.3.

Counterexamples & Assumption Synthesis
We now explain how Xenon uses the proof artifacts to help the user understand and explicate secrecy assumptions when verification fails. We first describe how Xenon analyzes the artifacts from the failed proof attempt in order to compute a counterexample consisting of the set of variables that-according to the information communicated by the prover-lost the constant-time property first ( § 4.1). Next, we discuss how Xenon uses the counterexample to synthesize a set of secrecy assumptions that eliminate the root cause of the verification failure ( § 4.2). This is done by computing a blame-set which contains the set of variables that likely caused the loss of constant-time for the variables in the counterexample via a control dependency. This blame set is then used to encode an optimization problem whose solution determines a minimal set of assumptions required to remove the timing violation. Finally, we briefly discuss how Xenon uses module summaries to speed up counterexample generation and secrecy assumption synthesis ( § 4.3).

Computing Counterexamples
Dependency Graph. To compute the counterexample from a failed proof attempt, Xenon first creates a dependency graph G (V, D ∪ C) which encodes data-, and control dependencies between program variables. G consists of vari- if v's value is used to compute w directly through an assignment, and controldependencies C ⊆ (Vars×Vars) where (v, w) ∈ C, if v's value is used indirectly, i.e., w's value is computed under a branch whose condition depends on v.
Variable-Time Map. Next, Xenon extracts an artifact from the failed proof attempt: a partial map varTime ∈ (Vars ⇀ N) which records the temporal order in which variables started to exhibit timing variability. Importantly, if for some v, varTime is undefined (we write varTime(v) = ⊥), the solver was able to prove that v is constant-time. For any other variables v and w, if varTime(v) < varTime(w), then v started to exhibit timing variability before w. 4 Xenon uses this map to break cyclic data-flow dependencies.
Computing the Counterexample. Using the data-flow graph, and varTime, Xenon computes a reduced graph. Xenon removes from the dependency graph, all nodes that are constant-time and all edges (w, v) such that varTime(w) > varTime(v). Intuitively, if variable w has started to exhibit timing variability after variable v, it cannot be the cause for v losing the constant-time property. Finally, Xenon removes all nodes that cannot reach a sink node using the remaining edges. This leaves us with a set of variables Cex ⊆ Vars without incoming edges, which we identify as the root cause of the violation, and which we present-as counterexample-to the user. We now define the reduced graph in more detail.
Reachability. For dependency graph G (V, D ∪ C) and nodes v, Reduced Graph. For a data-flow graph G (V, D ∪ C), and map varTime, we define the reduced graph with respect to varTime as the largest subgraph  Figure 3, the pipeline either stalls (Line 10) if flag Stall is set (Line 9), or else forwards values to the next stage (Line 13).

Like in
To avoid a write-after-write data-hazard, the Stall flag is set, if the instructions in the execute and decode stage have the same target registers (Line 6). The target register is calculated from the current instruction (Line 1), and the instruction is, in turn, fetched from memory using the current program counter (Line 3). Note the cyclic dependency between ID instr and Stall that turns comprehending the root cause into a "chicken-and-egg" problem.   Figure 9a shows the dependency graph for Figure 8. Data-dependencies are shown as solid edges, and control-dependencies are shown dashed. Each node is labeled with its varTime-value and marked ( ) if Xenon was able to prove the variable constant-time and (X) otherwise. Figure 9b shows the dependency graph after eliminating constant-time nodes from Figure 9a, and removing edges that violate the variable-time map. Removing the edge between Stall and ID instr breaks the cyclic dependency in the original graph. Figure 9c shows the variable dependency graph with a summary-graph extracted from the module summary.
pipeline is variable-time, the verification fails. To compute a minimal counterexample, Xenon creates the dependency graph shown in Figure 9a. Each node is annotated with information extracted from the failed proof attempt: the node is labeled with its value under varTime, and is marked with ( ) if Xenon was able to verify that the variable is constant-time and (X) otherwise. Solid edges represent data-, and dashed edges represent control dependencies. The ordering induced by varTime allows us to break the cyclic dependency between variables Stall and ID instr, thereby resolving the chicken-and-egg problem.
Reduced Dependency Graph. Figure 9b shows the dependency graph after removing all constant-time nodes and edges that violate the causal ordering. Xenon erases all nodes that cannot reach sink ID instr. This only leaves ID instr which we return as counterexample.
Remark. In case the proof artifact only partially resolves the cyclic dependencies, that is, vartime only defines a partial order over non-constant-time variables, the reduced graph may still contain cycles, and therefore there may be no nodes without predecessor. We can however still apply our technique by computing the graph's strongly connected components, and including all nodes in the respective component in the counterexample.

Assumption Synthesis
The previous step leaves us with a set of nodes Cex, which lost the constanttime property first. Since these nodes must have lost the constant-time property through a control dependency on a secret value, we can compute a set of variables Blame that are directly responsible: the immediate predecessors of Cex in the dependency graph with respect to a control dependency. Formally, for To synthesize secrecy assumptions that remove the constant-time violation, we could directly assume that all nodes in Blame are public. But this is often a poor choice: variables in Blame can be defined deep inside the circuit, whereas we would like to phrase our assumptions in terms of externally visible input sources.
Finding Secrecy Assumptions via ILP. Instead, we compute a minimal set of assumptions close to the input sources via a reduction to Integer Linear Programming (ILP). To this end, we use a second proof artifact, a map secret that-similar to varTime-describes the temporal order in which the verifier determines variables have become secret, i.e., ceased being public. Let G ′ = (V ′ , D ′ ∪ C ′ ) be the reduced dependency graph with respect to secret, and let No ⊆ V ′ be a set of variables that the user chose to exclude from consideration. Xenon produces constraints on a new set of variables: two constraint variables m v ∈ {0, 1} and p v ∈ {0, 1}, for each program variable v, such that m v = 1, if program variable v is marked public by an assumption, and p v = 1, if v can be shown to be public, that is, it is either marked public, or all its predecessors are public. Then, Xenon produces the following set of constraints.
Constraints (1) and (2) ensure that a variable is public, if either it is marked public, or all its predecessors in G ′ are public. Constraint (3) ensures that all blamed variables that have not been excluded can be shown to be public, and finally, constraint (4) ensures that all excluded constraints are not marked. Let d(v, w) be a distance metric, i.e., a function that maps pairs of nodes to the natural numbers. Then we want to solve the constraints using the following objective function that we wish to minimize, where for v ∈ V ′ , we define as weight the minimal distance from one of the source nodes w v = (arg min in∈Src d(in, v)): A solution to the constraints defines a set of assumptions A = (Flush, Pub), The constraints can be solved efficiently by an off-the-shelf ILP solver.
Example: Simplified Pipeline. Consider again the simplified pipeline in Figure 8. As we identified ID instr as the root cause in the previous step, we need to ensure that its blame-set consisting of all indirect influences is public. ID instr only depends on Stall, and therefore we add constraint p Stall = 1. Since, all variables are secret (i.e., we didn't make any public-assumptions yet), the reduced graph is equal to the original graph. For variables IF instr and ID instr, we get: m IF instr + p IF pc p IF instr and m ID Instr + p IF instr +p Stall 2 p ID Instr . We obtain the following objective function: m IF pc + 2m IF instr + 3m ID instr +. . . . Sending the constraints to an ILP solver produces a solution, where m IF pc = 1, m v = 0, for all variables v = IF PC, and p v = 1, for all v. This corresponds to the following assumption set A (Flush, {IF PC}), where Flush includes all variables except IF PC. This corresponds exactly to the desired minimal solution where we only mark IF pc as public. Note that our method does not necessarily result in all variables becoming public. We give an example in Appendix A.

Modular Assumption Synthesis
To avoid a blowup in constraint size, we want to avoid inlining instantiated modules. We therefore extract a dependency graph from the module summary: whenever the summary requires an input in to be public for an output out to be constant-time, we draw a control dependency between in and out. Whenever the summary requires an input in needs to be constant-time for an output out to be constant-time, we draw a data dependency. Finally, we insert the computed summary graph into the top level dependency graph, and connect the instantiation parameters to the graph's inputs and outputs.
Example. We modify Figure 8 to factor out the updates to ID instr into a separate module. Xenon computes the following summary invariant, from which we create the graph in Figure 9c: ct(IF instr) ∧ pub(Stall) ⇒ pub(ID instr). Since connecting the instantiated variables to the summary graph is equivalent to the original graph (Figure 9a), our analysis returns the same result.

Implementation
Xenon is split into front-end and back-end. Our front-end translates Verilog to the Iodine intermediate representation (IR) [46] and associates secrecy assumptions with input and output wires. Our back-end translates this annotated IR into verification conditions (Horn clauses); when verification fails, we generate counter examples and secrecy assumptions and present them to the user for feedback. We implement the back-end in roughly 9KLOC Haskell, using the liquid-fixpoint (0.8.0.2) [9] and Z3 (4.8.1) [35]  Inlined and Modular represent inlining module instances and using module summaries respectively. # Iter is the number of times the user has to invoke Xenon to verify the benchmark starting with an empty set of assumptions; CEX Ratio is the average ratio of the number of identifiers in the counterexample to all variable-time identifiers in a given iteration; Sugg Ratio is the average ratio of the number of secrecy assumptions that Xenon suggests to all secret variables in a given iteration, and Accept Ratio is the average ratio of the suggested assumptions accepted by the user. In the Total row, we use * to denote averages instead of sums. We do not run error localization on FPU2 and RSA because they are variable-time; AES-256 does not need any assumptions.

Evaluation
We evaluate Xenon by asking the following questions: ◮ Q1: Are constant-time counterexamples effective at localizing the cause of verification failures? ◮ Q2: Are the secrecy assumptions suggested by Xenon useful? ◮ Q3: What is the combined effect of counterexamples and secrecy assumption generation on the verification effort? ◮ Q4: Do module summaries improve scalability?
To answer questions Q1 and Q2, we use Xenon to recover the assumptions for the benchmark suite from [46]. These benchmarks include a MIPS and RISC-V core, ALU and FPU modules, and RSA and SHA-256 crypto modules. To evaluate questions Q3 and Q4, we evaluate Xenon on two challenging new benchmarks, the SCARV "side-channel hardened RISC-V" processor [4] whose size exceeds the largest benchmark from [46] by a factor of 10, and a highly modular AES-256 implementation [10].
Summary. Xenon's counterexample synthesis dramatically reduces the number of potential error locations users have to manually inspect (6% of its original size) and most of Xenon's assumption suggestions are accepted by the user (on average 81.67%). Module summaries are key to reducing verification times for certain hardware designs (e.g., for AES-256 crypto core summaries reduced the verification time from six hours to a three seconds). We find the counterexamples and secrecy assumptions suggested by Xenon to be crucial to reducing the human-in-the-loop time from days to (at worst) hours. Experimental Setup. We run all experiments on a 1.9GHz Intel Core i7-8650U machine with 16 GB of RAM, running Ubuntu 20.04 with Linux kernel 5.4. Methodology. For every benchmark, we start with an empty set of secrecy assumptions and run Xenon repeatedly to recover the missing assumptions needed to verify the benchmark. We collect the following information after every invocation of the tool: the total number of variables that are variable-time and secret; the size of the counterexamples measured by the number of variables they contain; the number of assumptions Xenon suggests, and the number of assumptions we reject during each iteration; finally, we record the number of times we invoke Xenon to complete each verification task. With all the assumptions in place, we measure the time it takes for the tool to verify each benchmark; we report the median of thirty runs for all but the non-modular (inlined) AES benchmark, for which-due to its size-we report the median of three runs. Q1: Error Localization. To understand whether our counterexample generation is effective at localizing the cause of verification failures, we compare the number of variables in the counterexample to the total number of non-constanttime variables. The CEX Ratio column Table 1 reports the average ratio per iteration. On average, we observe that less than 6% of non-constant-time variables are included in the counterexample. Since the total number of non-constant-time variables is typically on the order of hundreds (e.g., the median (and geomean) number of non-constant-time variables across all benchmarks and iteration is 97 (94)), this dramatically reduces the number of variables the developer has to inspect in order to understand the violation. For the benchmarks that were variable time, the counterexamples also precisely pinpointed where in the circuit the constant-time property was violated. For example, in the FPU2 benchmark Xenon included the state register in its third iteration counterexample. This register indicates when the FPU's output is ready. Inspecting the register's blame-set (similar to the process described in § 2.3) revealed that its value is set depending on whether one of the operands to the division operation is NaN and thus the FPU clearly leaks information about its operands. Q2: Identifying Secrecy Assumptions. To assess the quality of secrecy assumptions suggested by Xenon, we record the number of suggestions that the user accepts (useful suggestions) and the ratio of suggestions to the total number of secret variables the user would otherwise have to inspect manually. We find that most (on average 81.67%) of Xenon's suggestions are useful, reported in the Accept Ratio column of Table 1. Moreover, we observe that the number of variables included in the counterexamples is relatively small (Sugg Ratio column); on average, we only had to inspect 2.77% of the secret variables. Q3: Verification Effort. Finally, as a rough measure of the overall verification effort, we count the number of user interactions, i.e., the number of times we invoked Xenon after modifying our set of secrecy assumptions. Verifying the largest benchmark from [46], the Yarvi RISC-V core [6] took five invocations over several minutes. The final assumptions we arrived at were the same as the assumptions manually identified by the authors of Iodine in [46]; they, however, took multiple days to identify these assumptions and verify this core [52]. Verifying the SCARV core took thirty four iterations and roughly three hours; this core is considerably larger (roughly 10×) than the Yarvi RISC-V core and, we think, beyond what would possible with tools like Iodine, which rely on manual annotations and error localization. Indeed, we found the error localization and assumption inference to be especially useful in narrowing our focus and understanding to small parts of the core and avoid the need to understand complex implementation details irrelevant to the analysis.
Q4: Scalability. To evaluate how module summaries affect the scalability, we compare the time it takes to verify (or show variable-time) a program with and without module summaries. Columns Inlined and Modular of Table 1 gives the run times of Xenon with inlining (no summaries) and module summaries, respectively. On the Iodine benchmarks (the first seven benchmarks), we observe that module summaries don't meaningfully speed up verification. Indeed, on average, module summaries only reduce the size of the query sent to our solver by roughly 5% on these benchmarks. On the more complex AES-256 and SCARV benchmarks, however, we see the benefit of module summaries. For AES-256, using module summaries reduces the query size by 99.7%, from 391.3MB to 1.2MB, which, in turn, reduces the verification time by three orders of magnitude-from six hours to three seconds. Module summaries allow Xenon to exploit the core's modular design, i.e., AES-256's multiple and nested instantiations of the same modules (see Figure 5). For SCARV, summaries reduce the query size by 41%, and speed up the verification time by 40%. Though this reduction is not as dramatic as the AES-256 case, the speedup did improve Xenon's interactivity.

Related Work
Verifying Leakage Freedom. There are various techniques, such as ct-verif [16], [21], and CT-Wasm [74], that verify constant-time execution of software, and quantify leakage through timing and cache side-channels [13,14,39,56,68,79]. However, their analyses do not directly apply to our setting: They consider straight-line, sequential code, unlike the highly parallel nature of hardware. There are many techniques for verifying information flow properties of hardware. Kwon et al. [55] prove information flow safety of hardware for policies that allow explicit declassification and are expressed over streams of input data. SecVerilog [80] and Caisson [57] use information flow types to ensure that generated circuits are secure. GLIFT [71,72] tracks the flow of information at the gate level to eliminate timing channels. Other techniques such as HyperFlow [41], GhostRider [58] and Zhang et al. [79] take the hardware and software co-design approach to obtain end-to-end guarantees. dudect [66], detects end-to-end timing variabilities across the stack via a black-box technique based on statistical measurements. Iodine [46], like Xenon, focuses on clock-precise constant-time execution, not information flow. Unlike Xenon, none of these methods provides help in elucidating secrecy assumptions, in case the verification fails-a feature we found essential in scaling our analysis to larger benchmarks. We see the techniques presented in this paper as complementary and would like to explore their potential for scaling existing verification methods for hardware and software.
Fault Localization. There are several approaches to help developers localize the root causes of software bugs [75]. Logic-based fault localization techniques [30,40,50,51] are the closest line of work to ours. For example, BugAssist [50] uses a MAXSAT solver to compute the maximal set of statements that may cause the failure given a failed error trace of a C program. Xenon is similar in that we phrase localization as an optimization problem, allowing the use of ILP to locate the possible cause of a non-constant-time variable. However, Xenon focuses on constant-time, which is a relational property, and hardware which has a substantially different execution model.
Synthesizing Assumptions. Our approach to synthesizing secrecy assumptions is related to work on precondition synthesis for memory safety. Data-driven precondition inference techniques such as [43,44,62,69,70], unlike Xenon, require positive and negative examples to infer preconditions. Xenon's synthesis technique is an instance of abductive inference, which has been previously used to triage analysis reports by allowing the user to interactively determine the preconditions under which a program is safe or unsafe [36] or to identify the most general assumptions or context under which a given module can be verified safe [26,37,38,45]. Unlike the above, our abduction strategy is tailored to the relational constant-time property. Furthermore, Xenon uses information from the verifier to ensure that the user interaction loop only invokes the ILP solver (not the slower Horn-clause verifier), yielding a rapid cycle that pinpoints the assumptions under which a circuit is constant-time. In future work, we would like to see, if ideas introduced in Xenon can be applied to localization, explanation and verification of other classes of correctness or security properties.
Modular Verification of Software and Hardware. Xenon exploits modularity to verify large circuits by composing summaries of the behaviors of smaller sub-components of those circuits. This is a well-know idea in verification; for example, [67] shows how to perform dataflow analysis of large programs by computing procedure summaries, and Houdini [42] shows how to verify programs by automatically synthesizing pre-and post-conditions summarizing the behaviors of individual procedures. On the hardware side, model checkers like Mocha [17] and SMV [59] use rely-guarantee reasoning to perform modular verification. Kami [29] and [73] develops a compositional hardware verification methodology using the Coq proof assistant. However, the above require the user to provide module interface abstractions. There are some approaches that synthesize such abstractions in an counterexample guided fashion [48,81]. All focus on functional verification of properties of a single run, and do not support abstractions needed to reason about timing-channels which require relational hyperproperties [31].

A Example: Not all Variables Become Public
Example 3. One might think that Xenon requires all variables occurring in branch conditions to be annotated as public, however, this is not the case. Appendix A shows an example of such a program. Running Xenon produces the dependency graph shown in Figure 10. Xenon computes root-cause candidates by eliminating constant-time nodes and edges violating the precedence order. The result is shown in Figure 11. Removing all nodes that cannot reach source out leaves only nodes r3 and out, and since r3 has no predecessors, we identify it as the earliest node that became non-constant time, and therefore the root cause of the problem. Solving the ILP constraints yields stall as candidate assumption, and marking stall as public and restarting Xenon verifies constant time execution without the need to mark cond as public. This is possible because Xenon is able to prove that tmp1 and tmp2 have the same colors, irrespective of the value of cond, i.e., that tmp1 • =tmp2 • holds irrespective of cond.  out (X, 10) Fig. 11: Example 3: Variable dependency graph after eliminating non-ct nodes and edges that violate the precedence relation.