Security Verification of Low-Trust Architectures

Qinhan Tan
Three co-first authors contributed equally to this research.

Princeton University
New Jersey

Yonathan Fisseha
[1]

University of Michigan
Ann Arbor

Shibo Chen
[1]

University of Michigan
Ann Arbor

Lauren Biernacki

Lafayette College

Jean-Baptiste Jeannin

University of Michigan
Ann Arbor

Sharad Malik

Princeton University
New Jersey

Todd Austin

University of Michigan
Ann Arbor

Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component.
In this paper, we perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust  architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.

<concept_desc>Security and privacy Formal methods and theory of security</concept_desc>
<concept_desc>Security and privacy Information flow control</concept_desc>
<concept_desc>Security and privacy Security requirements</concept_desc>
<concept_desc>Security and privacy Side-channel analysis and countermeasures</concept_desc>

[500]Security and privacy Formal methods and theory of security
[500]Security and privacy Information flow control
[500]Security and privacy Security requirements
[300]Security and privacy Side-channel analysis and countermeasures

[1]

[1]

[1]

§ INTRODUCTION

Security verification of a computing system, while highly desirable, is a challenging task that often falls short of the desired level of guarantees. The verification must be applied to all trusted components of the system, including hardware and software. Unlike penetration testing, which consists of focused attempts to infiltrate a system, formal security verification is a proof that a particular security vulnerability does not exist within a design. Unfortunately, most systems today receive little to no formal security verification, due to design complexity challenges and limitations of formal proof mechanisms. Design complexity manifests in the sheer size of today's secure systems, which comprise architectures, microarchitectures, and deep software stacks, all of which must be trusted and verified. These complex systems easily exceed the capabilities of today's formal proof mechanisms, such as SAT/SMT solvers, model checkers, and proof assistants. Consequently, incomplete penetration testing still remains the backbone of today's security verification efforts.

Low-trust architectures have recently emerged as a secure system design framework that i) eliminates all trust in software, and ii) significantly reduces the amount of hardware trust to a small, software-free enclave component.
These properties make formal security verification feasible by shrinking the system aspects that must be trusted and verified.
In this paper, we focus on the security verification of Sequestered Encryption (SE) <cit.>—a low-trust architecture that claims to protect the confidentiality of sensitive data against direct data disclosures and digital side channels. Direct disclosures refer to any direct leakage of plaintext values through SE computation. Digital side channels represent any indirect leakage of plaintext values through non-analog information paths, including analysis of ciphertext values, operational timing, program control flow, memory access patterns, or microarchitectural resource usage. Currently, SE Enclave does not protect against analog information flow paths, such as frequency throttling <cit.>, power analysis <cit.>, electromagnetic snooping <cit.>, etc.

Within SE, the instruction set architecture (ISA) consists of the native instructions, termed the native ISA, and a set of secure instructions termed the SE ISA.

The native ISA contains insecure instructions to be executed by unsecured (or untrusted) components that do not have access to secret values.
In contrast, the SE ISA consists of secure instructions that operate on encrypted data and are executed solely in its software-free enclave component.
It is the design of this SE Enclave and ISA extension that ensures the cryptographic-strength confidentiality of the sensitive data.

Proof System and Paper Organization

In this work, we perform a complete formal verification of the SE low-trust architecture to show that the design is secure against direct data disclosures and digital side channels for all possible programs. The steps involved are illustrated in Figure <ref>. First, we articulate a set of instruction-level security requirements that SE ISA must fulfill to prevent disclosures or digital side channels. Going upwards to the software, these are used in hand-driven proof techniques to show that no SE program can possibly create a disclosure or digital side-channel leakage. Going downwards toward the hardware, the ISA security requirements necessitate security properties to be enforced in the hardware design, typically called RTL-level security properties.

Last, we propose a verification scheme to formally verify RTL-level properties using an off-the-shelf commercial formal verification tool (Cadence's JasperGold <cit.>) on real designs.
Our evaluation experiments show that our RTL-level verification scheme can prove the security properties being met by correct implementations, and also capture security leakages in flawed implementations.

This demonstrates the practical applicability of our proposed verification scheme to designs at scale.

To our knowledge, this is the first formal verification of a secure computing framework that extends to both direct disclosures and digital side channels, for all possible programs running on a verified computing platform.

A key takeaway from this work is that low-trust architectures lend themselves to formal security verification. We find two primary reasons for this outcome. First, the nature of low-trust architectures eliminates any trust in software. Since our verification ensures that the software can only see values encrypted under semantically secure cryptosystems <cit.>, software verification is not part of the overall proof system. Using only hand-driven proof, we show that any program using our ISA cannot disclose or create digital side channels, thus ending concern for any software.
In traditional security verification, where properties must be proven partly in hardware and software, often the complexity of software reasoning leads to compromises on what can be guaranteed in these systems.
Second, the simplicity of the low-trust SE hardware enclave, having minimal state and control logic, allows all of our ISA-level-based security assertions to complete on the actual RTL of the design, ensuring no gaps between the deployed design and any potential abstractions employed to enable formal verification.
We are confident that the approach we have detailed in this paper will extend itself to future low-trust architectures as they become available.

This work observes and demonstrates how low-trust architectures enable end-to-end software-to-hardware verification of strong security attributes, i.e., confidentiality and digital side-channel free execution.  Below is the list of specific contributions:

* Formal SE ISA Semantics: Define formal SE ISA semantics that enable privacy-related reasoning.

* Software-Level Proof: Povide proof of confidentiality and side-channel freedom for all programs written using this ISA.

* Hardware Proof Obligations: Provide proof obligations for any hardware implementation of the SE ISA to serve as the interface between the verification of the software and the hardware.

* Hardware-Level Proof:

* Provide a list of security properties that meet the hardware proof obligations for a specific SE hardware implementation.

* Demonstrate that these properties can be checked using standard information flow tracking (IFT) and commercial off-the-shelf IFT tools with novel RTL-verification elements.

* Demonstrate how the checking detects bugs in four buggy different implementations that violate these properties.

To further clarify the contributions of this work, we do not claim generalizability beyond the small enclaves in low-trust architectures detailed in <ref>. In fact, the increased level of verification is enabled by the low-trust architecture's property of limiting trust to only within the small SE Enclave, which in turn eliminates all trust in software and significantly reduces the degree of hardware that must be trusted (and thus needs to be verified) to ensure the proof properties.

Figure <ref> also serves to illustrate our paper organization. In  <ref>, we provide a brief overview of SE. In  <ref>, we articulate the threat model and the scope of this work. In  <ref>, we formalize ISA-level properties and prove the program-level properties inducted from the ISA-level properties followed by proof responsibilities discharged to the RTL-level. In  <ref>, we present our modeling and verification strategy at the RTL-level. In  <ref>, we describe the SE design variances and apply our verification scheme to these designs. We close the paper with related works ( <ref>) and final conclusions ( <ref>).

Our designs and verification scripts are available at <https://github.com/qinhant/SE_verification_CCS>.

§ BACKGROUND

In this section, we provide an overview of Sequestered Encryption (SE) <cit.> and show that the unique characteristics and design principles of SE open up new opportunities for hardware verification to provide complete reasoning of the underlying computing paradigm without the knowledge of specific programs.
A more detailed study of the SE design, including comparisons with related work, can be found in <cit.>.

§.§ Sequestered Encryption (SE)

Sequestered Encryption (SE) is a hardware-based technique to protect the confidentiality of secret third-party data during computation.
With SE, third-party data is encrypted in a trusted, client-side environment and offloaded to a server for computation. The server application operates on third-party data using SE's ISA instructions backed by custom hardware support.
Specifically, SE extends the conventional ISA to include secure instructions that operate on ciphertext data. We call these additional secure instructions the SE ISA. These instructions are dispatched to SE's hardware enclave, which computes the requested operation on the source ciphertexts.

The SE Enclave works to significantly reduce software and hardware trust by sequestering all sensitive computation to the hardware enclave. As such, the SE Enclave design claims that sensitive private data cannot be disclosed by any SE instruction sequence, either directly through a disclosure or indirectly through a digital side channel. This claim covers all digital side channels, including cryptanalysis of the ciphertext emitted by the Enclave, Enclave operational timing, and any possible influence the SE Enclave has on the system's memory access patterns and control flow. The goal of this paper is to formalize and prove these claims for the SE Enclave, through proofs on the SE instruction set operational semantics and their proof obligations expressed in the RTL implementation in the SE Enclave. With these claims proven, the SE Enclave represents the first enclave that has been formally verified to not suffer from software vulnerabilities or digital side channels.

SE Enclave Design

§.§ SE Instruction Set Architecture (ISA)

SE extends the native ISA with secure instructions that explicitly operate on ciphertext data.
When the processor decodes a secure instruction from the SE ISA, the instruction is dispatched to the SE Enclave for processing.

This operation mirrors how native instructions are dispatched to functional units in a conventional processor.
Insecure instructions in the native ISA are dispatched to unsecured functional units.

SE makes no claim about these instructions, as they are executed in an untrusted environment.

To ensure that sensitive data does not leave the enclave, SE restricts its secure instructions to be `data-oblivious,' only supporting arithmetic, logical, comparison, and shift operators.
The classes of instructions supported by the SE ISA are summarized in Table <ref>.
Specifically, the SE ISA does not support control flow or memory instructions, as these would innately leak information about sensitive data through architectural states like the program counter. Insecure versions of these instructions (i.e., those assumed to be operating on public data) are still present in the native ISA.
SE enables secure control flow via an encrypted conditional move () instruction.
Secure  instructions function as ternary operators, where a destination register is updated based on the value of some condition, akin to predicated instructions. This primitive enables programmers to make decisions on secret conditions, mimicking the logic of if-statements, in a safe manner.
Finally, to perform plaintext-ciphertext operations, the processor must first encrypt the plaintext value using SE's  instruction before passing the resultant value to another secure instruction for computation.

=0ex, =0ex]@0pt|lllcc|

[HTML]f3f3f31|l      2l     1cSecure    1c|Insecure

[HTML]f3f3f31|lInstruction Class      2lExample     1c(SE Enclave)    1c|(Native)

Encryption          Encryption

Arithmetic          Addition

Logical          Logical And

Comparison          Less Than

Shift          Logical Left Shift

Conditional          Conditional Move

Memory          Load

Control Flow          Jump

Summary of ISA

§.§ SE Enclave Implementation

The SE Enclave is architected as a small hardware functional unit embedded within the execute stage of the pipeline. This hardware unit includes storage of the secret key under which the user data is encrypted. When instructions are dispatched to the SE Enclave, the unit decrypts ciphertext source operands under this key, computes the requested operation in plaintext, then re-encrypts the result.
Namely, the syntax for a secure  instruction is  $\mathsf{ENC(~DEC(}$$\mathsf{)}$  $\mathsf{DEC(}$$\mathsf{)~)}$
This operation is illustrated in Figure <ref>.
The resultant ciphertext value is the only value that leaves the enclave.
The SE Enclave implementation is trusted and assumed to be free of direct data leakage.
Further, the SE Enclave is implemented to have data-independent timing, such that timing the execution of the enclave cannot reveal the plaintext values of ciphertexts.

For example, the SE Enclave cannot contain hardware optimizations that accelerate instructions for specific inputs (e.g., forwarding for multiply-by-zero <cit.>), as these optimizations leak information via timing.

While the design in Figure <ref> implements the syntax of the SE ISA, the SE Enclave can have many instantiations, including different implementations of encryption and decryption.
Below, we discuss some of the different variations of SE Enclave presented in <cit.>.
In this work, we present different RTL instantiations in Section <ref>.

§.§.§ Encryption Scheme

In SE, a value ($m$) is encrypted by appending a fresh random salt ($u$), then applying a strong pseudorandom permutation (PRP), such as a block cipher.
In this encryption scheme, both the data value and salt are 64 bits long, thereby producing a 128-bit ciphertext.
This scheme can be implemented in hardware with a variety of symmetric or asymmetric encryption ciphers built as rolled or unrolled implementations.
Prior work analyses three cryptographic ciphers for use within SE: AES-128, QARMA, and Simon. In this work, we also consider the popular asymmetric public-private key cryptosystem RSA.

The SE encryption scheme salts each ciphertext value with fresh randomness through the True Random Number Generator (TRNG) to ensure that ciphertexts are diversified to thwart cryptanalysis attacks and some side-channel attacks, i.e., CIPHERLEAKS <cit.>. This requirement is specified in the ISA and can be ensured by a structural RTL check.

§.§.§ Optimizations

SE can also be implemented with internal optimizations that seek to improve its performance. For example, <cit.> proposes caching recently decrypted ciphertexts in order to bypass the decryptor for instructions with data dependencies.

Optimizations have the potential to invalidate the security claims of SE.
In this work, we assess several secure and insecure optimizations of the SE Enclave to demonstrate that the secure optimizations are fully verified and the insecure optimizations are detectable by our novel verification technique.

§.§ Opportunities for Hardware Verification

SE's security claims are based on the assumption that the hardware is secure.
The SE architecture positions itself well for formal verification because it has a minimal hardware footprint and possesses no trusted software, which is in sharp contrast to other Trusted Execution Environments (TEEs), like Intel SGX. As noted by prior work <cit.>, formally reasoning about existing enclaves including Intel SGX is infeasible as any proof would have to model all processor features that exposed registers. Further, such work would be short-lived as any architectural modifications would invalidate this security proof.
Rather, SE's compact design allows it to be verified independently of other structures of the processor, thus avoiding the deficiency of verifying the whole processor.
In this work, we formally verify SE's security claims to establish trust in the SE ISA and its implementation.

§ SE ISA MODELING AND ANALYSIS

A conventional ISA does not place any requirements on microarchitectural states and state transitions as it only requires functional correctness. However, the SE ISA needs to make explicit and verifiable rules such that the system can guard off software-based attacks.

On the hardware side, the microarchitectural implementations need to faithfully follow the design requirements set by the ISA in a verifiable manner. The security properties resulting from these rules should be attested with formal proofs on the implementation side.

From the perspective of a program defined in such an ISA, there are two types of data: user private data and public data. Private data are sensitive data that are always encrypted under secured keys. The value of private data should only be visible to trusted and formally verified hardware components and remain invisible to any software or untrusted components. Public data are non-sensitive data that are stored in plaintext, i.e., program code, public constants, etc. While the conventional ISA is sufficient to operate on public data, a specialized set of instructions needs to be implemented in order to process private data securely. This set of secure instructions specifies additional requirements, which are not needed for public data only programs, to securely execute programs that compute on secured sensitive data. While previous work <cit.> has described these properties informally, we give precise definitions of the properties in this work and state proof obligations for the RTL verification to ensure that the implementation is faithful to the ISA specification. These requirements can be organized into two groups: Direct Disclosure Safety and Indirect Disclosure Safety. We will now consider them one at a time in the following sections.

§.§ ISA Direct Disclosure Safety Requirements

SE ISA must define the trust boundary between secure instructions and insecure instructions. This boundary is then guaranteed by the architecture. Inappropriate disclosure at the ISA level can happen in two ways: first, instructions could directly disclose the private plaintext data to insecure locations (e.g., registers that are readable by the attacker); second, the ciphertext is produced by a weak encryption cipher, making it vulnerable to cryptanalysis attacks.
Therefore, for any valid SE program, which is a sequence of instructions defined by the secure ISA, we have the following two requirements. First, we put the obvious restriction that there are no direct disclosures; and second, we put a requirement on the quality of the ciphertexts produced by the secure instructions.

§.§.§ Direct Information Disclosures

SE instructions take either a ciphertext or a public plaintext and produce a ciphertext as a result. Any secret data must never be disclosed to insecure (i.e., non-SE) instructions. This is reflected at both architectural and microarchitectural levels since SE uses encryption to hide sensitive information from untrusted software and hardware. The encryption module marks the trust boundary between the hardware components since all data is re-encrypted before it is emitted out of the trusted execution component and exposed to untrusted software and hardware. Encrypted data can be safely stored in untrusted storage or computed on by an insecure instruction.

The instruction level properties lift to programs naturally. All SE instructions produce ciphertext and there is no decrypt instruction in the ISA. Thus, non-SE instructions cannot get access to the plaintext. From this, we conclude that any composition of SE instructions and non-SE instructions cannot disclose the secret data.

§.§.§ Quality of Ciphertexts

Ciphertexts need to be safe from cryptanalysis when disclosed to an attacker of reasonable strength.
In this work, we consider security against chosen-ciphertext attacks (CCA), a standard attack model for cryptanalysis where the attacker has oracle access to the encryption function and an arbitrary collection of old ciphertext-plaintext pairs from the SE Enclave.
This model is more powerful than that of chosen plaintext attacks (CPA).
We assume that the attacker has bounded computational power and storage space, and does not have access to the encryption key a priori.
If the encryption scheme used by the SE Enclave has indistinguishability under CCA (termed CCA Security), then an attacker has close to a random-guess success rate in learning the plaintext value of a new ciphertext released by the SE Enclave, even if the attacker has amassed an arbitrary collection of previous ciphertext-plaintext pairs. In the following sections, we detail the encryption scheme used by the SE Enclave and how it achieves CCA security.

The single-instruction CCA security described above immediately lifts to programs involving multiple instructions since CCA security in the single-message case implies CCA security in the multiple-messages scenario.

§.§ ISA Indirect Disclosure Safety Requirements

Another important requirement that the ISA specifies and the underlying design should enforce is that there cannot be any observable digital effects correlated to the plaintext value of the secrets. The most prominent indirect disclosure is based on the digital side channel of the program's timing behavior. Similarly, the control flow and memory access pattern of the program can produce information about private user data without direct disclosure. The ISA must restrict all three indirect disclosures.

§.§.§ Instruction Stream Side-Channels

It is necessary that knowledge of which instructions get executed does not yield any more information than what is known at compile time.
Intuitively, such information can be derived only if there is a relationship between the control-flow structures of SE and the secret data of the user. However, insecure control-flow instructions do not see secret values by the definition of the ISA thus control-flow decisions cannot give any information about the secret. The only control-flow instruction that operates on secret data is the secure  instruction. However, as a secure SE instruction, it always produces ciphertexts with the property described in <ref>.

Unlike general control-flow instructions, like , which influence which instructions are executed,  always moves encrypted (and thus indistinguishable) data into the same destination register.
Therefore, although  makes a move decision based on secret data, it does not expose the secret. Consequently, observing the stream of executed instructions does not give the attacker a better-than-chance shot at guessing the secret. This property lifts to the program level from the instruction's property since all other disclosures from secure instructions to insecure instructions are removed by the direct disclosure restrictions from  <ref>.

§.§.§ Address Stream Side-Channels

Side channels in programs can also exist in their address streams where memory access patterns can expose information about private data indirectly. Similar to  <ref> above, such indirect disclosure is possible only when there is a relationship between the user's private data and memory access instructions. However, the insecure memory instructions, such as  and , do not have access to secret values. The only instruction that writes data to a location is the secure  instruction, which we have argued in  <ref> to be side-channel free.

Since all secure SE instructions do not disclose secrets by  <ref> and the ciphertexts produced have the property described in <ref>, we conclude that all programs composed of SE instructions do not leak secret information through their address access streams.

§.§.§ Instruction Timing Side-Channels

A final possible side channel we consider is timing variance in secure instructions that can leak information about the secret data indirectly. First, we require all secure instructions not to have timing variance that correlates to secret data. By the direct disclosure argument in <ref> we know that insecure SE instructions do not have access to secret data thus any timing variance they might have in their execution (including nondeterministic variance) cannot be correlated to secret values. From these two properties of instructions, we can lift to program-level properties naturally. Specifically, a program composed of SE instructions executed on two different secret data will have exactly the same timing behavior if we fix the rest of the execution environment. All variations that might occur in this setting would be caused by insecure instructions possibly exhibiting nondeterministic behavior, which is always independent of the secret data. Thus the timing of programs does not reveal any secrets.

§.§ Formalization of ISA Properties

While designing an ISA is already a challenging task that must carefully tread the interface between the hardware's behavior and the software's expectations, stating security principles at the ISA level is an even harder task. Fortunately, the SE ISA comprises a few unique instructions with precise semantics and security requirements. This allows us to give a formal treatment to some of the informal descriptions presented in  <ref> and  <ref> regarding disclosure and side channels, respectively. To formally reason about the ISA level properties we first start by defining a minimal syntax recognized by the secure SE processor. We allow an arbitrary but finite set of registers observable by the attacker except for the  which is private to the secure SE Enclave. The instruction $\mathsf{enc~r_1}$ is the encryption instruction that encrypts the value in the parameter register and places the result back into the same register. We abstract all binary operations, e.g., addition, subtraction, and shifts, to the instruction $\mathsf{bop~r_1, r_2}$ where some operation is performed on the values of the parameter registers, and the result is placed into the first parameter. Finally, a  is written as an if-else statement with a single assignment instruction as the body. Note that, unlike standard imperative languages, we do not allow conditional  statements with arbitrary bodies and there is no  construct either. The sequential composition operator $\mathsf{c;p}$ is a syntax restriction, forcing it to be right-associative. Enforcing it syntactically simplifies the semantics and type system, yet has no significant effect since sequential composition is associative. Figure <ref> presents this syntax of the SE language.

Registers $e$$r_1$ ⋯$r_{n}$ keyReg b [b]

Commands $c$enc $r_1$  bop $r_1,r_2$ skip

if $r_1: r_2 \leftarrow r_3~\mathsf{else}~r_2 \leftarrow r_4$

Program $p, q$c c; p

Minimal syntax for the SE ISA.

The semantics of the language is given by the small-step semantics in Figure <ref>. The semantics is entirely standard in imperative languages with the exception of the encryption and decryption operations and the time function $t$. First, all values are defined on finite length bits, i.e., $bits = \{0, 1\}^\rev{j}$ where $j \in \mathbb{N}$ is a non-deterministically picked natural number, which allows bit-level operators to be well defined in . Bits of all zeros can be interpreted as a boolean false and, conversely, bits of all ones can be interpreted as a boolean true.

Next, we use a simple and well-known encryption scheme which we present here for completeness. Details of this construction can be found in introductory textbooks such as <cit.>. Let $Func$ be the set of all functions of type $\{0,1\}^n \rightarrow \{0, 1\}^n$ and $F: \{0, 1\}^n \times \{0, 1\}^n \rightarrow \{0, 1\}^n$ be a keyed pseudorandom function inducing a distribution on $Func$. As usual, a bijective pseudorandom function $P$ is a pseudorandom permutation. We will write $F_k$ and $P_k$ defined as $F_k(\cdot) = F(k, \cdot)$ and $P_k(\cdot) = P(k, \cdot)$. A strong pseudorandom function $F$ is a pseudorandom function such that any polynomially bounded adversary $\mathcal{A}$ has a negligible advantage in differentiating between $F$ and the random function $F'$ even when given the inverse function $F^{-1}$. A strong pseudorandom permutation $P$ is a bijective strong pseudorandom function.

Now we can define the encryption scheme used by the SE enclave. Let $\mathcal{SE} = \langle encrypt(\cdot, \cdot), decrypt(\cdot, \cdot) \rangle$. The encryption key $k$ is uniformly picked from keys of length $s + n$. The message space is $\mathcal{M} = \{0, 1\}^n$, i.e., messages of length $n$. The encryption scheme is constructed as follows for any $m \in \mathcal{M}$:

\begin{align*}
& u \leftarrow uniform(s) && encrypt(k, m) = P_k(m || u) \\
&decrypt(k, m) = P_k^{-1}(m)[0:n] && decrypt(k, encrypt(k, m)) = m \end{align*}

for any strong keyed pseudo-permutation $P$ of block length $s + n$, where $||$ is defined as string concatenation. The random value $u$ is sampled from the uniform distribution of strings of length $s$.

This scheme, $\mathcal{SE}$, is known to be secure against chosen ciphertext attacks (CCA-secure) because an attacker has only negligible advantage in learning about $m$ given the ciphertext $encrypt(k, m)$. In Appendix <ref>, we give a formal definition of CCA security (Definition <ref>) and show that $\mathcal{SE}$ is  CCA-secure (Theorem <ref>).

To simplify the semantics of the ISA, we implicitly make the assumption that the polynomially-bounded attacker $\mathcal{A}$ has a stricter bound on the number of queries it can make to the encryption oracle. Intuitively, this assumption guarantees that the probability of the event that the same random value $u$ is used for two different encryption oracle calls is effectively zero. Given this assumption, we take the distribution of the ciphertexts to be truly uniform.[This effectively means the encryption scheme is a perfect encryption scheme. Strictly speaking, the pseudorandom permutation of the encryption scheme needs to be swapped for a random permutation to achieve this. But, any polynomial attacker only loses a negligible advantage due to this swap.]
This assumption only allows us to avoid the more complicated probabilistic semantics that would be required to properly model this negligible chance and otherwise has no effect on the semantics.

In the ISA semantics, we assume there is a truly uniform function that can generate $s$ bits for every encryption query and that a strong pseudorandom permutation is used. We justify these assumptions in <ref> by discharging verification responsibilities to the RTL-level verification, as summarized in Table <ref>. This leaves us with two tasks at the ISA level: i) ensure that $u$ is of some pre-fixed length $s$ on every encryption, and ii) ensure that a fresh $u$ from the random number generator is used for each encryption query. We formalize these two tasks in the semantics in the rest of this section.

The state of the system is represented by a set of registers $R$ containing values of $b \in bits$ and the syntactically decorated $[b]$. Marking values representing ciphertexts with brackets allows us to consider all ciphertexts to be effectively equivalent once we define the equivalence class. The function $\sigma:R \rightarrow bits$ provides the mapping. Let $\Sigma$ be the set of state maps $\sigma$ and allow $\sigma_1, \cdots, \sigma_n$ to range over $\Sigma$. There are three syntactic categories: programs, commands, and registers. The small-step arrow $\rightarrow_r$ produces bits by reading registers. We combine programs and commands into one syntactic category for the semantics, since all commands are programs; this makes the semantics more readable. The small-step arrow $\rightarrow$ for this combined syntactic category is defined over configurations of $\langle p, \sigma \rangle$. We write $u \sim uniform(s)$ to say the value $u$ is sampled from the uniform distribution of strings of length $s$. The function $t: \Sigma \rightarrow \mathbb{N}$ models the timing behavior of the system by allowing an arbitrary finite function to decide how long it takes for the instruction to complete execution. In a concrete design, the time taken can depend on a number of system and instruction level properties thus we allow the system to make this decision based on the entire system state $\sigma$.

The SE language semantics is a restricted fragment of standard imperative languages. For example, the conditional move commands ( and ) reflect this in that the bodies are single assignment instructions instead of the traditional recursive bodies. Additionally, the assignment is forced to the same location in both the true and false branch of the conditional. There is no use of exposed  or assignment operator in the language, but one could mimic it using the existing operators with the restriction that only ciphertext is written to locations. The occurrence of register symbols is treated as usual as a free variable (). The encryption instruction () encrypts the value found in the parameter register and places it back in the parameter. Similarly, the binary operations instruction () first decrypts the values, and computes on the plaintext values using the semantic operator $\oplus \in \{+, <<, >>, -, \cdots\}$, then finally re-encrypts the resulting value using the $encrypt$ relation, and writes the ciphertext back into the first operand register. Finally, the sequence operator () takes single steps transforming the head of the sequence until the base case of  is reached.

Since the  is the only inductive rule in the semantics, the program structure is that of a list instead of a tree as usual. Consequently, the small-step semantics never diverges in its execution. This property is essential for the soundness proof in Theorem <ref>. The security reasoning is done within the type system thus keeping the semantics standard.

decrypt(c_1, k) = true

decrypt(c_3, k) = m

u ∼uniform(s)

encrypt(m||u, k) = [c_5]

𝗂𝖿 r_1: r_2 ←r_3 𝖾𝗅𝗌𝖾 r_2 ←r_4 σskipσ[[c_5]/r_2]2 [cmov-f]

decrypt(c_1, k) = false

decrypt(c_4, k) = m

u ∼uniform(s)

encrypt(m||u, k) = [c_5]

𝗂𝖿 r_1: r_2 ←r_3 𝖾𝗅𝗌𝖾 r_2 ←r_4 σskipσ[[c_5]/r_2]2 [reg]
σ(r_1) = b
r_1σb [enc]

u ∼uniform(s)

encrypt(n||u,k) = [c_1]

𝖾𝗇𝖼 r_1σskipσ[[c_1]/r_1]1[bop]

decrypt(c_1, k) = n

decrypt(c_2, k) = m

u ∼uniform(s)

encrypt((n⊕m) || u, k) = [c_3]
𝖻𝗈𝗉 r_1 r_2σskipσ[[c_3]/r_1]2[seq] 𝗌𝗄𝗂𝗉; 𝗊σqσ1[]𝖼σ𝗌𝗄𝗂𝗉σ'1𝖼;𝗉σskip;pσ'1

The small-step semantics of the SE Enclave.

The type system used to reason about the security of information flow in the SE language is presented in Figure <ref>. The types are generated by the following grammar

Security labels $\ell$

Program Types $\tau$$\ell$  prog $\ell$

Let $L = \{\ell_1, \cdots, \ell_n\}$ be the set of security labels and $\mathcal{L} = \langle L, \leq \rangle$ by the bounded security lattice generated by $L$. We assume $L = \{\pu, \pr\}$ and that $\pr$ is the top of the lattice and $\pu$ is the bottom of the lattice. Generally, any security lattice can be decomposed into a low and high partition so our assumption is without loss of generality.

The typing environment $\G$ maps register locations to their types. We consider all register locations to be $\mathsf{\pu}$ except the  which is marked as private, thus,

\[
\G(r) = \begin{cases}
\mathsf{\pr}, &r = keyReg\\
\mathsf{\pu}, &\text{otherwise}
\end{cases}
\]

The rule  simply states this in the inductive rules. All constant values from $bits$ start out as $\pum$ (rule ). Similarly, the  instruction is always typed as $\pum$ (rule ). The instruction  is typed as $\pum$ if the two programs that are composed are already typed as $\mathsf{\pud}$. The instructions  and  are only required to demonstrate their operands are $\pum$ and can be immediately typed as $\mathsf{\pud}$.[It is not always the case that functions with $\mathsf{\pu}$ inputs will output $\mathsf{\pu}$ outputs. These typing rules for CMOV and BOP are sound because the security features of the semantics ensures the output is encrypted with fresh salt. ]

[reg](r) = ℓr ℓ[const] b ∈bitsb [enc]
r_1 enc  r [skip] skip [seq]
p_1 ℓ' prog

p_2 ℓ” prog

ℓ= ℓ' ⊔ℓ”
p_1; p_2 ℓ prog[bop]

bop  r_1 r_2  [cmov]

r_4 if r_1:r_2 ←r_3 else r_2 ←r_4

A high-level security type system for the secure SE language.

Next, we define an equivalency of states of the system and, specifically, low-equivalency following the convention in the literature <cit.>.

First, on the finite length bits $b$ and $[b]$, we define the equivalence class generated by the rules[This equivalence class is justified by the fact that the ciphertexts have a uniform distribution. Thus to the attacker, any two ciphertext carry the same information and the attacker shouldn't have a reasonable preference between any two ciphertexts.],

[equiv-br]b, b' ∈bits [b] ≈[b'][equiv]b, b' ∈bits
b = b'b ≈b'

Now we can define low-equivalence. In context $\Gamma$, states $\sigma, \sigma'$ are low equivalent $\sigma \approx_l \sigma'$ if they are equivalent on all low locations,

\begin{align*}
\Gamma\vdash\sigma(r) \approx \sigma'(r) \text{ for all $r$ where } \G(r) \leq l
\end{align*}

We can now restrict the behavior of $t$ using the definition above. We require that $t$ decides the amount of time taken by the instruction only using  data,

\begin{align}
\label{eq:time-invariance}
\text{ if } \Gamma\vdash\sigma \approx_l \sigma'  \text{  then }t(\sigma) = t(\sigma')
\end{align}

Intuitively, this means the timing function $t$ is influenced only by the location of level $l$ or lower (i.e., there is no timing dependency between the private data and the public data that could lead to timing side channels). This corresponds to the instruction timing property in  <ref>.

We just need one preliminary security lemma toward the main theorem now. For a well-typed program $c$, taking one step in the small-step semantics on two different states of the system that agree on publicly visible state locations will always produce states that continue to agree on publicly visible state locations. Moreover, the timing behavior of $t$ will also be equivalent on the two final states. This means changing any private locations in the state will not have an observable change on the publicly observable locations of the output states or the timing behavior of the program. The attacker that can observe only public locations (thus not inside of SE) cannot tell the difference between two executions of a program where the private data might be different and thus cannot derive additional knowledge about the secret user data from the public data. This property corresponds to <ref>. Lemma <ref> states this property formally now.

* $\tp c {\ell}$

* $\G \vdash \sigma_1 \approx_l \sigma_2$

* $\langle c, \sigma_1 \rangle \xrightarrow{t(\sigma_1)} \langle \mathsf{c_1'}, \sigma_1' \rangle$

* $\langle c, \sigma_2 \rangle \xrightarrow{t(\sigma_2)} \langle \mathsf{c_2'}, \sigma_2' \rangle$

* $dom(\G) = dom(\sigma_1) = dom(\sigma_2)$

then we have $\G \vdash \sigma_1' \approx_l \sigma_2'$ and $t(\sigma_1) = t(\sigma_2)$

By induction on structure of the derivation of $\langle c, \sigma_1 \rangle \xrightarrow{t(\sigma)} \langle \mathsf{c_1'}, \sigma_1' \rangle$. The timing requirement is immediate from assumption (2) and Eq. <ref>. See Appendix <ref> for the full proof.

The security result can now be stated via the soundness of the type system. The soundness argument of Theorem <ref> follows from Lemma <ref> for the most part by generalizing the number of steps to an arbitrary number (e.g., multiple steps until the program is equivalent to ).

* $\tp c {\ell}$

* $\G \vdash \sigma_1 \approx_l \sigma_2$

* $\langle c, \sigma_1 \rangle \xrightarrow{n}_* \langle \mathsf{skip}, \sigma_1' \rangle$

* $\langle c, \sigma_2 \rangle \xrightarrow{m}_* \langle \mathsf{skip}, \sigma_2' \rangle$

* $dom(\G) = dom(\sigma_1) = dom(\sigma_2)$

then we have $\G \vdash \sigma_1' \approx_l \sigma_2'$ and  $n = m$.

By induction on the number of steps. Both the base case and inductive case are consequences of Lemma <ref>. The timing property follows from the induction as well. See Appendix <ref> for details.

The type system and its soundness formalize the properties discussed in <ref> except <ref> (Instruction stream) and <ref> (Address Stream).  <ref> and <ref> refer to insecure instructions that can access all $r$ where $\tp r \pu$ but cannot decrypt ciphertexts since  is . An insecure instruction can at most corrupt ciphertexts but when executed on two low-equivalent states must produce a pair of low-equivalent states as well. Any timing variation in these instructions is not correlated to private data since the behavior of $t$ is restricted by low-equivalence. In the following section, we summarize the requirements the ISA places on the RTL-level to provide the security properties of Theorem <ref>.

§.§ Summary of Proof Obligations Discharged to RTL Verification

To achieve the above program-level properties, we expect the RTL implementation to satisfy some requirements about individual secure SE instructions. Note that we have no requirements for insecure instructions. We enumerate these requirements here and later show how the RTL-level verification formally guarantees these instruction-level properties. The properties are split into instruction-level properties which are properties that must be satisfied by each instruction, and a system-level property which is a more general requirement on the system.

In Table <ref>, property (P1) summarizes <ref> and is required by all the direct and indirect disclosure arguments in <ref> and <ref> respectively. Both (P1.1) and (P1.2) are formalized in <ref> and Appendix <ref>. Property (P2) is required by <ref> and Eq. <ref> formally states this requirement.
Finally, the system-level property (P3) is required by all the disclosure arguments since each assumes there is no way to get a plaintext from a ciphertext using the SE Enclave's key except within the small SE Enclave. The formal semantics in Figure <ref> and the concluding remarks regarding insecure commands in <ref> require it as well.

=0ex, =0ex]@0pt|cc|c|c|

[HTML]f3f3f3     3cInstruction-Level Property

1|c|2*P1     Strong    P1.1     $encrypt$ is a strong keyed PRP; $decrypt$ is its inverse

1|c|    ciphertext     P1.2    The value $u$ has length $s$ and is sampled from a uniform dist.

1|c|P2     3cInstructions have no secret dependent time variation

[HTML]f3f3f3     3cSystem-Level Property

1|c|P3     3cRe-encrypt all data for output. No decrypt operation outside SE Enclave

Properties assumed at the ISA level and discharged to the RTL verification.

§ RTL SECURITY PROPERTIES

In this section, we formally define the security properties in an RTL implementation of SE so as to support the instruction-level requirements from  <ref>.
We employ standard hardware information flow tracking (IFT) to check RTL-level properties.
Briefly, if secret variables (plaintext and crypto key) do not leak to outputs of the Enclave, then the attacker is not able to infer secret values based on any observation and thus security is guaranteed.

For the rest of this section, we will first discuss the security goal at the RTL level, clarify the connection between ISA-level assumptions and RTL-level properties, then provide a formal definition for the hardware information flow properties to be checked for the RTL design.

§.§ RTL-Level Security Goal

We assume that the attacker can observe and control any signal, register, and memory location outside the boundary of SE Enclave (including the Enclave's outputs), but they cannot observe and manipulate signals and states within SE Enclave.
SE Enclave is connected with the rest of the system with a well-defined IO interface.
Such an assumption keeps the footprint of trusted RTL design minimal.

Our RTL-level security goal is to prevent secret variables inside the Enclave from leaking to the outputs of the Enclave in two forms: functional leakage and timing leakage.
Functional leakage happens if the attacker can directly infer secret information from the result of the SE Instruction.
Timing leakage happens if the execution time of some instruction depends on the secret and the attacker may infer secret information by measuring the execution time.

=0ex, =0ex]@0pt|c|c|

[HTML]f3f3f3 ISA-Level Requirement     RTL-Level Property

P1    Functional Correctness of Crypto and RNG

P2     No Timing Leakage at the SE Enclave Outputs

P3     No Functional Leakage at the SE Enclave Outputs

Mapping between ISA-Level Requirement and RTL-Level Properties.

§.§ ISA-RTL Property Mapping

Table <ref> provides the connection between requirements from the ISA-level and the properties to be checked at the RTL-level.

P1: The implementation is required to satisfy the requirements of the scheme $\mathcal{SE}$ defined in <ref> without the restriction of the semantics on the number of calls the attacker makes. Thus, the implementation supports the strictly stronger attacker of the CCA-security game in Appendix <ref>. Two specific requirements are discharged on the cryptographic algorithms: the use of a strong pseudorandom permutation and availability of a truly random $s$-bit generator. For example, the RTL may implement AES-128 which is a block-cipher (thus $s=64, n=64$), and block-ciphers are an implementation of strong pseudorandom permutation <cit.>. Other implementation options, such as RSA, come from the closely related family of trapdoor permutations and satify this requirement as well.
The values $u$, which is defined in <ref>, is generated by a hardware-based TRNG as shown in Figure <ref>. As discussed in <ref>, we assume the existence of high-bandwidth and bias-free TRNGs and consider their design out of scope for this work. The quality of the random number generator can be checked using existing tools, e.g., Dieharder <cit.>. Similarly, the functional correctness of the encryption and decryption units can be checked by existing techniques <cit.> and is not discussed in this paper.

P2: Any secret-dependent execution time will result in timing leakage, i.e., secret dependent variation in the timing at which results are available at the SE Enclave outputs. Thus, we need to check there is no timing leakage at the SE Enclave outputs in the RTL.

P3: Any unencrypted secret at the data output would result in a functional leakage of the instruction result at the SE Enclave outputs. Thus, we need check there is no functional leakage at the SE Enclave outputs in the RTL.
Further, without any information (functional or timing) about the encryption key (which is only in the SE Enclave), it is impossible to decrypt the ciphertext outside of the Enclave.

The notion of `leakage' can be formalized using standard hardware IFT, which we will define for the SE Enclave and discuss in the following subsections.

§.§ SE Definition

We use the following finite state machine (FSM) to represent an SE Enclave: $SE = (I,O,S,S_0,N,F)$, where:

* $I$ is a vector of input variables and the domain of $I $ is $ \mathbb{I}$.

* $O$ is a vector of output variables. The domain of $O$ is $\mathbb{O}$.

* $S$ is a vector of state variables and the domain of $S $ is $ \mathbb{S}$.

* $S_0$ is the initial value for $S$.

* $N: (\mathbb{S}\times \mathbb{I})\rightarrow \mathbb{S}$ is the next state function for $S$.

* $F: (\mathbb{S}\times \mathbb{I})\rightarrow \mathbb{O}$ is the output function.

The secrets, i.e., plaintext output $p$ of decryption and the secret key $k$ are also state variables in $S$.
$S$ also includes the random salt $r$ used as input to the encryption unit.

To describe the execution of the SE Enclave, we introduce the notion of a finite-length execution trace:
$\Pi = (\pi_I, \pi_O, \pi_S) $ represents an execution for $n$ cycles where $\pi_I=(I_0, I_1, I_2, ... I_{n-1})$ is a trace of input values for each cycle, $\pi_O=(O_0, O_1, O_2, ... O_{n-1})$ is a trace of output values for each cycle, $\pi_S=(S_0, S_1, s_2, ... S_{n-1})$ is a trace of state variable values from each cycle.
The elements in $\pi_I, \pi_O, \pi_S$ follow the next state function $N$ and the output function $F$.
In the following parts of the paper, we may use $\pi_x=(x_0, x_1, x_2, ... x_{n-1})$ to denote the trace of a variable $x$ which consists of the value of $x$ at every cycle in the execution, and $\pi_Y=(Y_0, Y_1, Y_2, ... Y_{n-1})$ to denote the trace of a vector $Y$ which consists of the value of $Y$ at every cycle in the execution.

Next, we define information flow using execution traces.

§.§ Classic Information Flow Definition

The classic information flow definition is based on the well-known `non-interference' property <cit.>.
The key idea of this property is: if a variable $x$ never interferes with another variable $y$ in the system, then replacing $x$ with different values will never affect the value of $y$.
Let $s$ be a secret variable and $o$ be an output variable. In our setting, if there is no information flow from $s$ to $o$, then the value of $o$ is independent of the value of $s$, thus it is impossible to infer $s$ based on $o$.

$s$ not influencing $o$ means the value of $o$ at every cycle is not changed when the value of $s$ is replaced with an arbitrary value.
Let $\Pi$ be an execution trace of length $n$, $Q$ be the vector state variables besides $s$, $\pi_s$ denote the trace of $s$, $\pi_{Q}$ denote the trace of $Q$, $\pi_o$ denote the trace of $o$, $F_o$ denote the output function for $o$, $N_{Q}$ denote the next state function for $Q$.
If in $\Pi$ we replace $\pi_s$ with a different trace $\pi_s'$ (it differs from $\pi_s$ in at least one cycle), then we can use $\pi_s'$ to compute the new trace of $Q, o$, i.e., $\pi_Q'$ and $\pi_o'$ as follows:

$$ Q_0' = Q_0, Q_i' = N_Q(I_{i-1}, Q_{i-1}', s'_{i-1}), 1\leq i<n$$

$$o_i'=F_o(I_i, Q_i', s'_i),0\leq i < n$$

There exists information flow from $s$ to $o$ if and only if

$$\exists \Pi, \exists \pi_s'$$

such that after computing $\pi_Q'$, $\pi_o'$,

$$\pi_o\neq \pi_o'$$
($\pi_o, \pi_o'$ differ in at least one cycle)

However, we need to modify this classic information flow definition to analyze a design with encryption.
In the threat model, we assume that the ciphertext after encryption will not leak any information about the plaintext. However, changing the plaintext will necessarily change the ciphertext regardless of the encryption scheme.
Therefore, we would reach the conclusion that there is information flow from the plaintext to the ciphertext, but this would be a false alert.
We describe our solution to this issue in the following subsection by using the notion of `ciphertext declassification.'

§.§ Information Flow with Ciphertext Declassification

The idea of declassification <cit.> allows  information flow under a specific condition.
This allows information flow to go through a certain variable such as the ciphertext output of the encryption unit under the condition that the encryption is finished.
The similar idea is also applied in our ISA-level proof.

Let $s$ be a secret variable, $o$ be an output variable, and $c$ be the ciphertext output of encryption.
Let $p$ be a predicate that represents the completion of encryption, i.e., $p$ is only true when encryption is completed.
The intuitive way to realize declassification is to model the design such that when $p$ is true, $c$ is replaced by a free variable $c_f$.
This cuts off the connection between $s$ and $c$ when $p$ is true and blocks the information flow under this condition, but not otherwise.

Next, we will give a formal description of the above method. We construct a new FSM $SE'$ from FSM $SE$ as follows.
(i) We add a free variable $c_f$ to the input vector $I$.
(ii) For the output function $F$ and next state function $N$, replace all occurrences of $c$ in their arguments using the following expression $p\;?\;c_f:c$.

Denote the new input vector as $I'$, the new output function as $F'$, and the new next state function as $N'$.
The only difference between FSM $SE'$ and FSM $SE$ is that in $SE'$, $c$ is replaced by $c_f$ when $p$ is true.
Then, in the original FSM $SE$ there exists information flow from $s$ to $o$ not going through $c$ when $p$ holds if and only if there exists information flow from $s$ to $o$ in $SE'$.
We call the above technique `ciphertext declassification information flow'.

§.§ Summary

Based on our threat model

we want to check if there exists information flow from the secrets to the Enclave outputs not going through the ciphertext after encryption.
We will demonstrate in  <ref> how both functional and timing leakage can be captured using standard hardware IFT.

In the next section, we detail the SE implementations, including three secure implementations and four insecure implementations, then use hardware IFT to either detect leakage or prove security.

§ IMPLEMENTATION AND EVALUATION

To evaluate the effectiveness and performance of our RTL verification technique, we implemented a collection of SE Enclave designs with different microarchitectural optimizations or security flaws. The goal of the evaluation is to check if our verification technique is sufficient to support common microarchitectural design optimizations and catch security flaws when they are present. In this section, we first describe the designs we implemented as the verification targets and then explain our verification process on each of those design options, followed by experiment results.

§.§ SE RTL Enclave Design Details

§.§ Evaluation Overview

§.§.§ Checking RTL Properties Using IFT

We check the RTL properties stated in Table <ref> using standard IFT. The secret variables (the source in IFT) are i) the plaintext after decryption and ii) the crypto key in the key register. The destination variables for the IFT are the two outputs of the SE Enclave,  and .
Information flow to  indicates timing leakage as when  goes high, i.e., the completion signal, depends on a secret. Information flow to  indicates dependence of  on the secret. This dependence may indicate functional leakage, i.e., the secret may be inferred from the value of  or timing leakage depending on the sequence of values at . For example,  may stay at a value of  till it has a valid value, and switch to this valid value when it is ready. This distinction between functional leakage and timing leakage at  is made by design analysis or using techniques from previous works <cit.>. To distinguish this from the timing leakage observed at , we refer to timing leakage at  as functional-timing leakage.

§.§.§ Hardware Information Flow Tracking Tool

We can use any available IFT tool <cit.> to check for information flow. In this work, we use Cadence JasperGold Security Path Verification (SPV) tool <cit.> for its availability in both industry and academia (through a university license).

The tool will either prove that there is no information flow from the sources (the decrypted plaintext and key register) to the destination (the SE Enclave outputs) or find a hardware trace that demonstrates the information flow using symbolic model checking, i.e., over all possible inputs.

§.§.§ Conditional Ciphertext Declassification

In our setting we need to check information flow with ciphertext declassification. SPV could potentially check this using blackboxing and the not-through switch (in previous SPV versions). SPV also allows specifying predicates on the source and destination under which information flow is allowed. However, in our setting we need to check information flow with conditional ciphertext declassification using predicates on intermediate signals, rather than with the source/destination (e.g., only declassify the ciphertext when the encryption is finished).

We accomplish this with a simple modification of the RTL design as described in  <ref>.
Note that we need to treat unrolled encryption and rolled encryption differently.
For unrolled encryption, because of its pipeline structure, we can directly replace the ciphertext output of the last crypto unit in the pipeline with a free input $c_f$ because the output of the last crypto unit is always completely encrypted which means the completion predicate $p$ is always true.
For rolled encryption, since there is only one crypto unit, we only replace its output with a free input when the counter indicates that it is the last round.
Thus, for a 10-round encryption, the completion predicate $p$ is $Counter==10$.

§.§.§ Cache Initialization

When evaluating SE variants with caching, we initialize the cache to be in an arbitrary state, i.e., any cache line can be valid or invalid.
Since JasperGold conducts symbolic model checking, all possible initial states will be explored, thus ensuring full coverage.
This helps catch vulnerabilities in a much shorter time because some vulnerabilities only leak information when the cache is full.
If we initialize the cache to be empty, the formal tool needs to conduct an extremely long symbolic execution, which significantly increases the verification time.
If we initialize the cache to be full, although we may catch the vulnerability leaking information with the full cache faster, the tool cannot cover the entire search space because there is no instruction to flush the cache in the SE Enclave.
However, we will fail to capture vulnerabilities that only leak information when the cache is not full.
Therefore, initializing the cache to be in an arbitrary state can avoid the above two drawbacks.
As the experiments demonstrate, the formal tool can prove security with full coverage, and also capture vulnerabilities efficiently.

In the following subsection, we will evaluate implementations of the SE Enclave and its variants, along with several buggy implementations using the JasperGold SPV tool.

5|c|Processor: two Intel Xeon 5222 cores

5|c|Memory: 256 GB

5|c|Tool: Cadence JasperGold 2021

[HTML]f3f3f3     SE Variant          register bits     result     leakage      time     memory

Default    6544     secure     -     0.1s     1.6GB

Rolled AES   1412    secure    -     0.1s     0.7GB

Cache   12784   secure    -     0.1s     1.6GB

Vulnerable    2*1412    2*insecure     functional     2*109.4s    2*2.5GB

Rolled AES             (plaintext $\rightarrow$
, key $\rightarrow$ )

Vulnerable    2*6737    2*insecure     timing     2*63.3s    2*4.7GB

Multiplier             (plaintext $\rightarrow$ )

Vulnerable     2*12752    2*insecure     timing     2*402.4s    2*14.7GB

Cache             (plaintext $\rightarrow$ )

Vulnerable    2*4328    2*insecure     timing, functional-timing      2*0.1s     2*0.3GB

RSA             (key $\rightarrow$ , key $\rightarrow$  )

Experimental Evaluation

§.§ Experimental Results

The experimental results are provided in Table <ref>.
For every SE design variant, we show the number of register bits as an indicator of the size of the state space.
In addition to the verification result, i.e., secure or insecure, we also label every insecure design with the leakage type, along with the source and sink of the information flow captured.
The  implementation has functional leakage where both plaintext secrets and the encryption key are leaked to .
The  and  have timing leakage where the plaintext secrets are leaked to .
For , there exists information flow to both  and .
The leakage through  is timing leakage, but there is also timing leakage through  as it is also leaking information about execution time as follows.
The RSA crypto engine can only be implemented as a non-pipeline structure (the number of rounds is variable and depends on the decryption key).
Thus, similar to rolled AES encryption, its output needs to be blocked when the encryption is ongoing.
This means that when the ciphertext is not ready, it will output some default value such as all  to the .
The attacker can infer the decryption key by measuring the number of s between two non-zero ciphertext outputs which is timing leakage. As discussed in  <ref>, we distinguish between the timing leakage to  and   by referring to the latter as functional-timing leakage.

In a pipelined AES encryption in the default SE Enclave design, the crypto engine outputs a fully encrypted ciphertext every cycle, thus only  carries timing information and this attack does not work.
This explains why there is no information flow to  for  and .

As shown in Table <ref>, it takes less time and memory to prove no information leakage for secure implementations than to detect information leakage for the vulnerable ones.
In secure designs, since the path from secrets to both outputs is cut off after declassification, SPV only needs to do a simple structural path check to prove the security. In comparison, SPV needs to do a state space search in order to detect information leakage in a vulnerable design.
The time and memory usage are also affected by the number of register bits and the complexity of the design.
Across all implementations, the maximum verification time is less than 7 minutes.
The experimental results demonstrate that our evaluation scheme is able to prove security or catch leakage precisely and efficiently.

§.§ Summary

In this section, we evaluated different SE Enclave variants using information flow checking.
In general, our information flow definition and evaluation methodology work on any low-trust architecture with encryption.
This is because low-trust architectures limit trust to only a small hardware enclave which facilitates formal verification, and the conditional ciphertext declassification we implemented can correctly deal with the information flow going through encryption.

§ RELATED WORK

§.§ Secure Hardware Architectures

There have been numerous works in designing secure architectures as microarchitectural flaws (and lack of security awareness at the architecture level) continue to be exploited by software attacks.

Trusted Execution Environments (TEEs) <cit.> have been widely deployed by mainstream hardware vendors in their server-grade CPUs to provide execution integrity and data confidentiality.
Although the root of trust is also in hardware, TEEs such as Intel SGX <cit.> and Keystone <cit.> have a significantly different threat model as they do not eliminate timing side channels.
Sanctum <cit.>, MI6 <cit.>, and Ascend <cit.> aim to eliminate timing side channels, but they have much larger trusted computing bases than SE, making them hard to be formally verified.

Multiple works have been developed to mitigate leakage of data through timing side channels during speculative execution.

Hyperflow <cit.> enforces data security properties by static flow analysis at the hardware construction time. It relies on a trusted label manager to assign correct labels to data.  OISA <cit.> presents a timing-channel free ISA extension that uses tags to distinguish Public and Confidential data. It verifies both ISA and microarchitectural implementation through an abstract machine. Speculative Taint Tracking (STT) <cit.> and Speculative Data-Oblivious Execution (SDO) <cit.> are consecutive works that use runtime speculative taint analysis to eliminate timing side channels for safe speculative execution by delaying transient execution on the backend. DOLMA <cit.> introduces the principle of transient non-observability and delays executions that are reliant on speculative memory micro-ops. Software-hardware contract <cit.> formalizes software security requirements and hardware capabilities to ensure confidentiality for benign programs.

In comparison, we present the ISA and RTL level verification of a low-trust architecture that cannot leak secrets for any (even malicious) program, which is absent in the aforementioned works.

§.§ Functional Leakage and Timing Leakage

In this work, we use the role of signals to differentiate between functional leakage and timing leakage, i.e., using hardware information flow tracking at  for functional leakage and at  for timing leakage.
This idea was discussed in a previous work <cit.>.

Aside from using the role of signals, previous works also tried to use the observation of a signal in consecutive cycles (sequence) to differentiate between functional and timing leakage <cit.>.
Such techniques require more complex hardware information flow tracking logic and can separate timing leakage and functional leakage without needing to know the role of signals.
However, since our work is interested in capturing both types of leakage, we choose to use the simpler role-based classification.

§.§ Hardware Security Evaluation Schemes

§.§.§ Type-Based Hardware Security Evaluation

SecVerilog <cit.> and its variants <cit.> introduce new hardware design languages that allow developers to attach different security levels to hardware variables while programming, and also to define the rules for information flowing between different security levels.
To declassify, these languages provide 'downgrading' syntax in the language to permit specific information flows.
Static type checking is conducted to formally verify that the security policy is followed by the design.

While it is computationally faster, verification based on static type checking is not as precise as verification based on symbolic checking as in our work <cit.>.
Static type checking may easily produce false positives due to its conservative nature.
Further, it is inconvenient and error-prone for users to use a new language along with security labels in developing hardware.

§.§.§ Other Evaluation Schemes Based on Information Flow

Depending on threat models, different security properties have been proposed and verified.
These properties are based on the basic information flow property and add different conditions and constraints according to the threat model.

Attempts have been made to detect timing leakage with taint propagation <cit.> by verifying properties such as `constant-time execution'. Works based on Unique Program Execution Checking <cit.> are aimed at checking information leakage through out-of-order execution, where information flow caused by in-order execution is ruled out by constraints.

A key advantage of our work is that we are able to verify security properties at the instruction level for all programs while other works do not provide the same guarantees.

§ CONCLUSIONS

This work demonstrates how the security of all programs running on low-trust architectures can be ensured by clearly defining the security requirements of their ISA instructions, formally specifying the consequent proof obligations for RTL implementations, and then executing these proof obligations using RTL formal verification tools. Further, it shows how these proof obligations cover functional as well as timing side-channel leakage. Finally, the small footprint of the trusted part of the implementation enables completing the formal checks using existing state-of-the-art formal verification tools - something that is currently not possible for non-low-trust architectures. We demonstrate our approach using the SE architecture where the ISA and the program-level proof are handwritten and the RTL-level verification done using off-the-shelf formal tools.
Our experiments using seven different design variants shows that our approach is effective in proving the security of correct implementations and detecting flaws in buggy implementations.

We thank Professor Paul Grubbs from the University of Michigan for lending his expertise in cryptography.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

Known-plaintext Attack.

[Alam et al(2018)]
authorpersonMonjur Alam, personHaider Adnan
Khan, personMoumita Dey, personNishith Sinha,
personRobert Callan, personAlenka Zajic, and
personMilos Prvulovic. year2018.
One&Done: A Single-Decryption EM-Based
Attack on OpenSSL’s Constant-Time Blinded RSA. In
booktitle27th USENIX Security Symposium (USENIX Security
18). publisherUSENIX Association, addressBaltimore,
MD, pages585–602.

authorpersonTiago Alves.
Trustzone: Integrated Hardware and Software
journalWhite paper (year2004).

[Anati et al(2013)]
authorpersonIttai Anati, personShay Gueron,
personSimon Johnson, and personVincent Scarlata.
Innovative Technology for CPU based Attestation and
Sealing. In booktitleProceedings of the 2nd international
workshop on hardware and architectural support for security and privacy,
Vol. volume13. ACM New York, NY, USA.

[Ardeshiricham et al(2017a)]
authorpersonArmaiti Ardeshiricham, personWei
Hu, and personRyan Kastner. year2017a.
Clepsydra: Modeling timing flows in hardware
designs. In booktitle2017 IEEE/ACM International Conference
on Computer-Aided Design (ICCAD). IEEE, pages147–154.

[Ardeshiricham et al(2017b)]
authorpersonArmaiti Ardeshiricham, personWei
Hu, personJoshua Marxen, and personRyan Kastner.
Register transfer level information flow tracking
for provably secure hardware design. In booktitleDesign,
Automation & Test in Europe Conference & Exhibition (DATE), 2017. IEEE,

[Askarov and Sabelfeld(2007)]
authorpersonAslan Askarov and personAndrei
Sabelfeld. year2007.
Gradual Release: Unifying Declassification,
Encryption and Key Release Policies. In booktitle2007 IEEE
Symposium on Security and Privacy (SP'07). IEEE, pages207–221.

authorpersonJim Attridge.
An Overview of Hardware Security Modules.
journalSANS Institute. Information Security Reading
Room (year2002).

authorpersonRoberto Avanzi.
The QARMA Block Cipher Family. Almost MDS Matrices
Over Rings With Zero Divisors, Nearly Symmetric Even-Mansour Constructions
With Non-Involutory Central Rounds, and Search Heuristics for Low-Latency
journalIACR Transactions on Symmetric Cryptology
volume2017, number1 (dateMar.
year2017), pages4–44.

[Bardeh and Rønjom(2019)]
authorpersonNavid Ghaedi Bardeh and
personSondre Rønjom. year2019.
Practical Attacks on Reduced-Round AES. In
booktitleProgress in Cryptology – AFRICACRYPT 2019,
editorpersonJohannes Buchmann,
personAbderrahmane Nitaj, and personTajjeeddine
Rachidi (Eds.). publisherSpringer International Publishing,
addressCham, pages297–310.

[Baudet et al(2011)]
authorpersonMathieu Baudet, personDavid
Lubicz, personJulien Micolod, and personAndré
Tassiaux. year2011.
On the Security of Oscillator-Based Random Number
journalJ. Cryptol. volume24,
number2 (dateapr year2011),

[Beaulieu et al(2015)]
authorpersonRay Beaulieu, personStefan
Treatman-Clark, personDouglas Shors, personBryan
Weeks, personJason Smith, and personLouis
Wingers. year2015.
The SIMON and SPECK Lightweight Block Ciphers. In
booktitle2015 52nd ACM/EDAC/IEEE Design Automation
Conference (DAC). pages1–6.

[Biernacki et al(2022)]
authorpersonLauren Biernacki,
personMeron Zerihun Demissie, personKidus Birkayehu
Workneh, personFitsum Assamnew Andargie, and
personTodd Austin. year2022.
Sequestered Encryption: A Hardware Technique for
Comprehensive Data Privacy. In booktitle2022 IEEE
International Symposium on Secure and Private Execution Environment Design
(SEED). pages73–84.

[Bittau et al(2014)]
authorpersonAndrea Bittau, personAdam
Belay, personAli Mashtizadeh, personDavid
Mazières, and personDan Boneh.
Hacking Blind. In booktitle2014
IEEE Symposium on Security and Privacy. IEEE, pages227–242.

[Blaze et al(1998)]
authorpersonMatt Blaze, personJoan
Feigenbaum, and personAngelos D Keromytis.
KeyNote: Trust Management for Public-Key
Infrastructures. In booktitleInternational Workshop on
Security Protocols. Springer, pages59–63.

[Bourgeat et al(2019)]
authorpersonThomas Bourgeat, personIlia
Lebedev, personAndrew Wright, personSizhuo Zhang,
and personSrinivas Devadas. year2019.
Mi6: Secure Enclaves in a Speculative Out-Of-Order
Processor. In booktitleProceedings of the 52nd Annual
IEEE/ACM International Symposium on Microarchitecture.

[Bresson et al(2007)]
authorpersonEmmanuel Bresson, personOlivier
Chevassut, and personDavid Pointcheval.
Provably Secure Authenticated Group Diffie-Hellman
Key Exchange.
journalACM Transactions on Information and System
Security (TISSEC) volume10, number3
(year2007), pages10–es.

authorpersonRobert G Brown.
Dieharder: A Random Number Test Suite.

<https://webhome.phy.duke.edu/ rgb/General/dieharder.php>

authorpersonCadence. year2022.
titleJasperGold Security Path Verification.

[Champagne and Lee(2010)]
authorpersonDavid Champagne and
personRuby B Lee. year2010.
Scalable Architectural Support for Trusted
Software. In booktitleHPCA-16 2010 The Sixteenth
International Symposium on High-Performance Computer Architecture. IEEE,

[Clarkson and Schneider(2010)]
authorpersonMichael R Clarkson and
personFred B Schneider. year2010.
journalJournal of Computer Security
volume18, number6 (year2010),

[Costan and Devadas(2016)]
authorpersonVictor Costan and
personSrinivas Devadas. year2016.
Intel SGX Explained.
journalCryptology ePrint Archive

[Costan et al(2016)]
authorpersonVictor Costan, personIlia
Lebedev, and personSrinivas Devadas.
Sanctum: Minimal Hardware Extensions for Strong
Software Isolation. In booktitle25th USENIX Security
Symposium (USENIX Security 16). pages857–874.

[Delgado-Restituto et al(1992)]
authorpersonM. Delgado-Restituto, personA.
Rodriguez-Vasquez, personS. Espejo, and personJ.L.
Huertas. year1992.
A Chaotic Switched-Capacitor Circuit for 1/f Noise
journalIEEE Transactions on Circuits and Systems I:
Fundamental Theory and Applications volume39,
number4 (year1992), pages325–328.

[Fadiheh et al(2020)]
authorpersonMohammad Rahmani Fadiheh,
personJohannes Müller, personRaik Brinkmann,
personSubhasish Mitra, personDominik Stoffel, and
personWolfgang Kunz. year2020.
A Formal Approach for Detecting Vulnerabilities to
Transient Execution Attacks in Out-of-Order Processors. In
booktitle2020 57th ACM/IEEE Design Automation Conference
(DAC). IEEE, pages1–6.

[Fadiheh et al(2019)]
authorpersonMohammad Rahmani Fadiheh,
personDominik Stoffel, personClark Barrett,
personSubhasish Mitra, and personWolfgang Kunz.
Processor Hardware Security Vulnerabilities and
Their Detection by Unique Program Execution Checking. In
booktitle2019 Design, Automation & Test in Europe
Conference & Exhibition (DATE). IEEE, pages994–999.

[Ferraiuolo et al(2017a)]
authorpersonAndrew Ferraiuolo, personWeizhe
Hua, personAndrew C Myers, and personG Edward
Suh. year2017a.
Secure Information Flow Verification with Mutable
Dependent Types. In booktitle2017 54th ACM/EDAC/IEEE Design
Automation Conference (DAC). IEEE, pages1–6.

[Ferraiuolo et al(2017b)]
authorpersonAndrew Ferraiuolo, personRui
Xu, personDanfeng Zhang, personAndrew C Myers, and
personG Edward Suh. year2017b.
Verification of a Practical Hardware Security
Architecture through Static Information Flow Analysis. In
booktitleProceedings of the Twenty-Second International
Conference on Architectural Support for Programming Languages and Operating
Systems. pages555–568.

[Ferraiuolo et al([n. d.])]
authorpersonAndrew Ferraiuolo, personMark
Zhao, personAndrew C. Myers, and personG. Edward
Suh. year[n. d.].
HyperFlow: A Processor Architecture for
Nonmalleable, Timing-Safe Information Flow Security. In
booktitleProceedings of the 2018 ACM SIGSAC Conference
on Computer and Communications Security (Toronto Canada, 2018-10-15).
publisherACM, pages1583–1600.

[Fletcher et al(2012)]
authorpersonChristopher W Fletcher,
personMarten van Dijk, and personSrinivas Devadas.
A Secure Processor Architecture for Encrypted
Computation on Untrusted Programs. In booktitleProceedings
of the seventh ACM workshop on Scalable trusted computing.

[Gleissenthall et al(2019)]
authorpersonKlaus v Gleissenthall,
personRami Gökhan Kıcı, personDeian Stefan,
and personRanjit Jhala. year2019.
IODINE: Verifying Constant-Time Execution of
Hardware. In booktitle28th USENIX Security Symposium
(USENIX Security 19). pages1411–1428.

[Goguen and Meseguer(1982)]
authorpersonJoseph A Goguen and
personJosé Meseguer. year1982.
Security Policies and Security Models. In
booktitle1982 IEEE Symposium on Security and Privacy.
IEEE, pages11–11.

[Goldwasser and Micali(1982)]
authorpersonShafi Goldwasser and
personSilvio Micali. year1982.
Probabilistic Encryption: How to Play Mental Poker
Keeping Secret All Partial Information. In
booktitleProceedings of the Fourteenth Annual ACM Symposium
on Theory of Computing (San Francisco, California, USA)
(seriesSTOC '82). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Goubin and Patarin(1999)]
authorpersonLouis Goubin and personJacques
Patarin. year1999.
DES and Differential Power Analysis the
“Duplication” Method. In booktitleCryptographic
Hardware and Embedded Systems: First InternationalWorkshop, CHES’99
Worcester, MA, USA, August 12–13, 1999 Proceedings 1. Springer,

[Großschädl et al(2009)]
authorpersonJohann Großschädl,
personElisabeth Oswald, personDan Page, and
personMichael Tunstall. year2009.
Side-channel Analysis of Cryptographic Software via
Early-terminating Multiplications. In
booktitleInternational Conference on Information Security
and Cryptology. pages176–192.

[Guarnieri et al(2021)]
authorpersonMarco Guarnieri, personBoris
Köpf, personJan Reineke, and personPepe Vila.
Hardware-Software Contracts for Secure
Speculation. In booktitle2021 IEEE Symposium on Security
and Privacy (SP). pages1868–1883.

[Haddad et al(2014)]
authorpersonPatrick Haddad, personYannick
Teglia, personFlorent Bernard, and personViktor
Fischer. year2014.
On the Assumption of Mutual Independence of Jitter
Realizations in P-TRNG Stochastic Models. In booktitle2014
Design, Automation and Test in Europe Conference and Exhibition (DATE).

[Hamalainen et al(2006)]
authorpersonPanu Hamalainen, personTimo
Alho, personMarko Hannikainen, and personTimo D
Hamalainen. year2006.
Design and Implementation of Low-Area and Low-Power
AES Encryption Hardware Core. In booktitle9th EUROMICRO
conference on digital system design (DSD'06). IEEE,

authorpersonZiyad Hanna.
titleJasper Case Study on Formally Verifying Secure
On-Chip Datapaths. <https://www.deepchip.com/items/0524-03.html>.

authorpersonBen Harris.
booktitleRSA Key Exchange for the Secure Shell (SSH)
Transport Layer Protocol.
typeTechnical Report.

authorpersonSimon Heron.
Advanced Encryption Standard (AES).
journalNetwork Security volume2009,
number12 (year2009), pages8–12.

[Housley et al(1999)]
authorpersonRussell Housley, personWarwick
Ford, personWilliam Polk, and personDavid Solo.
booktitleInternet X. 509 Public Key Infrastructure
Certificate and CRL Profile
typeTechnical Report.

[Hu et al(2021)]
authorpersonWei Hu, personArmaiti
Ardeshiricham, and personRyan Kastner.
Hardware information flow tracking.
journalACM Computing Surveys (CSUR)
volume54, number4 (year2021),

[James Wyllie(1944)]
authorpersonTony Sale James Wyllie.
A Cryptographic Dictionary.
journalNR 4559, Historic Cryptographic Collection,
Pre-World War I Through World War II, Record Group 457

[Katz and Lindell(2020)]
authorpersonJonathan Katz and personYehuda
Lindell. year2020.
booktitleIntroduction to modern cryptography.
publisherCRC press.

[Khoo et al(2010)]
authorpersonYit Phang Khoo,
personBor-Yuh Evan Chang, and personJeffrey S
Foster. year2010.
Mixing type checking and symbolic execution.
journalACM Sigplan Notices volume45,
number6 (year2010), pages436–447.

[Kim et al(2021)]
authorpersonKyungduk Kim, personStefan
Bittner, personYongquan Zeng, personStefano
Guazzotti, personOrtwin Hess, personQi Jie Wang,
and personHui Cao. year2021.
Massively Parallel Ultrafast Random Bit Generation
with a Chip-scale Laser.
journalScience volume371,
number6532 (year2021), pages948–952.

[Kiniry et al(2018)]
authorpersonJoseph R Kiniry, personDaniel M
Zimmerman, personRobert Dockins, and personRishiyur
Nikhil. year2018.
A Formally Verified Cryptographic Extension to a
RISC-V Processor.
journalComputer Architecture Research with
RISC-V–CARRV 2018 (year2018).

[Kocher et al(1999)]
authorpersonPaul Kocher, personJoshua
Jaffe, and personBenjamin Jun.
Differential Power Analysis. In
booktitleAdvances in Cryptology—CRYPTO’99: 19th Annual
International Cryptology Conference Santa Barbara, California, USA, August
15–19, 1999 Proceedings 19. Springer, pages388–397.

[Kuan et al(2014)]
authorpersonTing-Kuei Kuan, personYu-Hsuan
Chiang, and personShen-Iuan Liu.
A 0.43pJ/bit True Random Number Generator. In
booktitle2014 IEEE Asian Solid-State Circuits Conference
(A-SSCC). pages33–36.

[Lee et al(2020)]
authorpersonDayeol Lee, personDavid
Kohlbrenner, personShweta Shinde, personKrste
Asanović, and personDawn Song.
Keystone: An open framework for architecting
trusted execution environments. In booktitleProceedings of
the Fifteenth European Conference on Computer Systems.

[Li et al(2021)]
authorpersonMengyuan Li, personYinqian
Zhang, personHuibo Wang, personKang Li, and
personYueqiang Cheng. year2021.
CIPHERLEAKS: Breaking Constant-time Cryptography on
AMD SEV via the Ciphertext Side Channel.. In
booktitleUSENIX Security Symposium.

[Liu et al(2022)]
authorpersonChen Liu, personAbhishek
Chakraborty, personNikhil Chawla, and personNeer
Roggel. year2022.
Frequency Throttling Side-Channel Attack. In
booktitleProceedings of the 2022 ACM SIGSAC Conference on
Computer and Communications Security (Los Angeles, CA, USA)
(seriesCCS '22). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Liu et al(2015)]
authorpersonFangfei Liu, personYuval Yarom,
personQian Ge, personGernot Heiser, and
personRuby B. Lee. year2015.
Last-Level Cache Side-Channel Attacks are
Practical. In booktitle2015 IEEE Symposium on Security and
Privacy. pages605–622.

[Loughlin et al(2021)]
authorpersonKevin Loughlin, personIan Neal,
personJiacheng Ma, personElisa Tsai,
personOfir Weisse, personSatish Narayanasamy, and
personBaris Kasikci. year2021.
DOLMA: Securing Speculation with the Principle of
Transient Non-Observability. In booktitle30th USENIX
Security Symposium (USENIX Security 21). publisherUSENIX
Association, pages1397–1414.

authorpersonStefan Mangard.
A Simple Power-analysis (SPA) Attack on
Implementations of the AES Key Expansion. In
booktitleInformation Security and Cryptology—ICISC 2002:
5th International Conference Seoul, Korea, November 28–29, 2002 Revised
Papers 5. Springer, pages343–358.

authorpersonUeli Maurer.
Modelling a Public-Key Infrastructure. In
booktitleEuropean Symposium on Research in Computer
Security. Springer, pages325–350.

[McKeen et al(2013)]
authorpersonFrank McKeen, personIlya
Alexandrovich, personAlex Berenzon, personCarlos V
Rozas, personHisham Shafi, personVedvyas Shanbhogue,
and personUday R Savagaonkar. year2013.
Innovative Instructions and Software Model for
Isolated Execution.
journalHasp@ isca volume10,
number1 (year2013).

[Mehibel and Hamadouche(2017)]
authorpersonNissa Mehibel and
personM'hamed Hamadouche. year2017.
A New Approach of Elliptic Curve Diffie-Hellman Key
Exchange. In booktitle2017 5th International Conference on
Electrical Engineering-Boumerdes (ICEE-B). IEEE, pages1–6.

authorpersonAndrew Myers.
Proving noninterference for a while-language using
small-step operational semantics.

[Oberg et al(2014)]
authorpersonJason Oberg, personSarah
Meiklejohn, personTimothy Sherwood, and personRyan
Kastner. year2014.
Leveraging Gate-level Properties to Identify
Hardware Timing Channels.
journalIEEE Transactions on Computer-Aided Design of
Integrated Circuits and Systems volume33, number9
(year2014), pages1288–1301.

[Petrie and Connelly(2000)]
authorpersonC.S. Petrie and personJ.A.
Connelly. year2000.
A Noise-based IC Random Number Generator for
Applications in Cryptography.
journalIEEE Transactions on Circuits and Systems I:
Fundamental Theory and Applications volume47,
number5 (year2000), pages615–621.

[Ravi et al(2020)]
authorpersonPrasanna Ravi, personShivam
Bhasin, personSujoy Sinha Roy, and personAnupam
Chattopadhyay. year2020.
titleDrop by Drop you break the rock - Exploiting generic
vulnerabilities in Lattice-based PKE/KEMs using EM-based Physical Attacks.
howpublishedCryptology ePrint Archive, Paper 2020/549.

[Ren et al(2017)]
authorpersonLing Ren, personChristopher W
Fletcher, personAlbert Kwon, personMarten Van Dijk,
and personSrinivas Devadas. year2017.
Design and Implementation of the Ascend Secure
journalIEEE Transactions on Dependable and Secure
Computing volume16, number2 (year2017),

authorpersonEric Rescorla.
booktitleDiffie-hellman Key Agreement Method.
typeTechnical Report.

[Rodríguez Vázquez et al(1991)]
authorpersonÁngel Benito
Rodríguez Vázquez, personManuel Delgado Restituto,
personServando Carlos Espejo Meana, and
personJosé Luis Huertas Díaz.
A Switched-Capacitor Broadband Noise Generator for
CMOS VLSI.
journalElectronics Letters, 27 (21), 1913-1915.

[Rosulek([n. d.])]
authorpersonMike Rosulek.
year[n. d.].
titleThe Joy of Cryptography.

[Sabelfeld and Sands(2009)]
authorpersonAndrei Sabelfeld and
personDavid Sands. year2009.
Declassification: Dimensions and principles.
journalJournal of Computer Security
volume17, number5 (year2009),

authorpersonMatthias Schunter.
Intel Software Guard Extensions: Introduction and
Open Research Challenges. In booktitleProceedings of the
2016 ACM Workshop on Software Protection. pages1–1.

[Sehatbakhsh et al(2020)]
authorpersonNader Sehatbakhsh,
personBaki Berkay Yilmaz, personAlenka Zajic, and
personMilos Prvulovic. year2020.
A New Side-Channel Vulnerability on Modern
Computers by Exploiting Electromagnetic Emanations from the Power Management
Unit. In booktitle2020 IEEE International Symposium on High
Performance Computer Architecture (HPCA). pages123–138.

[Solt et al(2022)]
authorpersonFlavien Solt, personBen Gras,
and personKaveh Razavi. year2022.
CellIFT: Leveraging Cells for Scalable and
Precise Dynamic Information Flow Tracking in RTL. In
booktitle31st USENIX Security Symposium (USENIX Security
22). pages2549–2566.

[Suh et al(2003)]
authorpersonG Edward Suh, personDwaine
Clarke, personBlaise Gassend, personMarten Van Dijk,
and personSrinivas Devadas. year2003.
AEGIS: Architecture for Tamper-Evident and
Tamper-Resistant Processing. In booktitleACM International
Conference on Supercomputing 25th Anniversary Volume.

[Suh et al(2005)]
authorpersonG Edward Suh, personCharles W
O'Donnell, personIshan Sachdev, and personSrinivas
Devadas. year2005.
Design and Implementation of the AEGIS Single-Chip
Secure Processor using Physical Random Functions. In
booktitle32nd International Symposium on Computer
Architecture (ISCA'05). IEEE, pages25–36.

[Tiwari et al(2009)]
authorpersonMohit Tiwari, personHassan MG
Wassel, personBita Mazloom, personShashidhar Mysore,
personFrederic T Chong, and personTimothy
Sherwood. year2009.
Complete Information Flow Tracking from the Gates
Up. In booktitleProceedings of the 14th international
conference on Architectural support for programming languages and operating
systems. pages109–120.

[Volpano et al(1996)]
authorpersonDennis Volpano, personCynthia
Irvine, and personGeoffrey Smith.
A sound type system for secure flow analysis.
journalJournal of computer security
volume4, number2-3 (year1996),

[Wang et al(2022)]
authorpersonYingchen Wang, personRiccardo
Paccagnella, personElizabeth Tang He, personHovav
Shacham, personChristopher W. Fletcher, and
personDavid Kohlbrenner. year2022.
Hertzbleed: Turning Power Side-Channel Attacks
Into Remote Timing Attacks on x86. In booktitle31st USENIX
Security Symposium (USENIX Security 22). publisherUSENIX
Association, addressBoston, MA, pages679–697.

[Wei and Guo(2009)]
authorpersonWei Wei and personHong Guo.
Bias-free true random-number generator.
journalOpt. Lett. volume34,
number12 (dateJun year2009),

authorpersonJoel Weise.
Public Key Infrastructure Overview.
journalSun BluePrints OnLine, August
(year2001), pages1–27.

authorpersonWing H Wong.
Timing Attacks on RSA: Revealing Your Secrets
through the Fourth Dimension.
journalXRDS: Crossroads, The ACM Magazine for
Students volume11, number3 (year2005),

[Yasuda et al(2004)]
authorpersonS. Yasuda, personH. Satake,
personT. Tanamoto, personR. Ohba, personK.
Uchida, and personS. Fujita. year2004.
Physical Random Number Generator Based on MOS
Structure after Soft Breakdown.
journalIEEE Journal of Solid-State Circuits
volume39, number8 (year2004),

[Yu et al([n. d.])]
authorpersonJiyong Yu, personLucas Hsiung,
personMohamad El'Hajj, and personChristopher W.
Fletcher. year[n. d.].
Data Oblivious ISA Extensions for Side
Channel-Resistant and High Performance Computing. In
booktitleProceedings 2019 Network and Distributed System
Security Symposium (San Diego, CA, 2019). publisherInternet

[Yu et al(2020)]
authorpersonJiyong Yu, personNamrata
Mantri, personJosep Torrellas, personAdam Morrison,
and personChristopher W. Fletcher.
Speculative Data-Oblivious Execution: Mobilizing
Safe Prediction For Safe and Efficient Speculative Execution. In
booktitle2020 ACM/IEEE 47th Annual International Symposium
on Computer Architecture (ISCA). pages707–720.

[Yu et al(2019)]
authorpersonJiyong Yu, personMengjia Yan,
personArtem Khyzha, personAdam Morrison,
personJosep Torrellas, and personChristopher W.
Fletcher. year2019.
Speculative Taint Tracking (STT): A Comprehensive
Protection for Speculatively Accessed Data. In
booktitleProceedings of the 52nd Annual IEEE/ACM
International Symposium on Microarchitecture (Columbus, OH, USA)
(seriesMICRO '52). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Zhang et al(2015)]
authorpersonDanfeng Zhang, personYao Wang,
personG Edward Suh, and personAndrew C Myers.
A Hardware Design Language for Timing-sensitive
Information-flow Security.
journalAcm Sigplan Notices volume50,
number4 (year2015), pages503–516.

[Çiçek and Dündar(2013)]
authorpersonİhsan Çiçek and
personGünhan Dündar. year2013.
A Chaos-based Integrated Jitter Booster Circuit for
True Random Number Generators. In booktitle2013 European
Conference on Circuit Theory and Design (ECCTD). pages1–4.