{'fraction_non_alphanumeric': 0.03730096721178974, 'fraction_numerical': 0.00758412587224183, 'mean_word_length': 4.432889344262295, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Verifying and Synthesizing Constant-Resource Implementations with Types

We propose a novel type system for verifying that programs correctly implement constant-resource behavior. Our type system extends recent work on automatic amortized resource analysis (AARA), a set of techniques that automatically derive provable upper bounds on the resource consumption of programs. We devise new techniques that build on the potential method to achieve compositionality, precision, and automation. A strict global requirement that a program always maintains constant resource usage is too restrictive for most practical applications. It is sufficient to require that the program's resource behavior remain constant with respect to an attacker who is only allowed to observe part of the program's state and behavior. To account for this, our type system incorporates information flow tracking into its resource analysis. This allows our system to certify programs that need to violate the constant-time requirement in certain cases, as long as doing so does not leak confidential information to attackers. We formalize this guarantee by defining a new notion of resource-aware noninterference, and prove that our system enforces it. Finally, we show how our type inference algorithm can be used to synthesize a constant-time implementation from one that cannot be verified as secure, effectively repairing insecure programs automatically. We also show how a second novel AARA system that computes lower bounds on resource usage can be used to derive quantitative bounds on the amount of information that a program leaks through its resource use. We implemented each of these systems in Resource Aware ML, and show that it can be applied to verify constant-time behavior in a number of applications including encryption and decryption routines, database queries, and other resource-aware functionality.


I. INTRODUCTION
Side-channel attacks extract sensitive information about a program's state through its observable use of resources such as time, network, and memory. These attacks pose a realistic threat to the security of systems in a range of settings, in which the attacker has local access to the native host [1], through multi-tenant virtualized environments [2], [3], or remotely over the network [4]. Side channels have revealed highly-sensitive data such as cryptographic keys [1], [4], [5], [6], [7] and private user data [8], [9], [10], [11], [12].
These attacks are mounted by taking repeated measurements of a program's resource behavior, and comparing the resulting observations against a model that relates the program's secret state to its resource usage. Unlike direct information flow channels that operate over the input/output semantics of a program, the conditions that give rise to side channels are oftentimes subtle and therefore difficult for programmers to identify and mitigate. This also poses a challenge for automated tool support aimed at addressing such problems-whereas direct information flow can be described in terms of standard program semantics, a similar precise treatment of side channels requires incorporating the corresponding resource into the semantics and applying quantitative reasoning.
This difficulty has led previous work in the area to treat resource use indirectly, by reasoning about the flow of secret information into branching control flow or other operations that might affect resource use [13], [14], [15], [16]. These approaches can limit the expressiveness of secure programs and further complicate the development. For example, by requiring programmers to write code using a "constant-time discipline" that forbids the use of variables influenced by secret state in statements that could affect the program's control path [13].
Verifiable constant-resource language: In this paper, we present a novel type system that gives developers the ability to certify that their code is secure against resource side-channel attacks w.r.t. a high-level attack model, in which the resource consumption of each language construct is modeled by a constant. Our approach reduces constraints on the expressiveness of programs that can be verified, and does not introduce general stylistic guidelines that must be followed in order to ensure constant-resource behavior. Programmers write code in typical functional style and annotate variables with standard types. Thus, it does not degrade the readability of the code. At compile time, our verifier performs a quantitative analysis to infer additional type information that characterizes the resource usage. From this, constant-resource behavior w.r.t. the high-level model on all executions of the program is determined automatically.
The granularity with which our resource guarantees hold against an attacker who can measure the total quantity of consumed resources is roughly equivalent to what can be obtained by adhering to a strict constant-time programming discipline. The certified constant-resource programs prevent side-channels that are inherent in implementing algorithms w.r.t. the provided high-level attack model. For example, if the resource under consideration is execution time, measured by the number of language constructs executed by the program (e.g., the total number of arithmetic operations, function calls, etc.), then our system provides a defense against attackers that can observe the same resource measure. To have a stronger guarantee, e.g., against cache side channels, our resource model could in principle incorporate memoryaccess patterns and instruction caches. Other types of side channels arising from low-level behaviors, such as branch prediction or instructions whose resource usage is influenced by argument values, require corresponding changes to the resource model. Our technique does not currently model such timing differences, so is not a defense against such attacks.
In general, requiring that a program always consumes constant resources is too restrictive. In most settings, it is sufficient to ensure that the resource behavior of a program does not depend on selected confidential parts of the program's state. To account for this, our type system tracks information flow using standard techniques, and uses this information to reason about an adversary who can observe and manipulate public state as well as resource usage through public outputs. Intuitively, resource-aware noninterference-the guarantee enforced by this type system-requires that the parts of the program that are both affected by secret data and can influence public outputs, can only make constant use of resources.
To accomplish this without limiting expressiveness or imposing stylistic requirements, the type system must be allowed to freely switch between local and global reasoning. One extreme would be to ignore the information flow of the secret values and prove that the whole program has global constant resource consumption. The other extreme would be to ensure that every conditional that branches on a secret value (critical conditionals) uses a constant amount of resources. However, there are constant-resource programs in which individual conditionals are not locally constantresource (see Section III). As a result, we allow different levels of global and local reasoning in the type system to ensure that every critical conditional occurs in a constantresource block.
Finally, we show that our type-inference algorithm can be used to automatically repair programs that make inappropriate non-constant use of resources, by synthesizing constantresource ones whose input/output behavior is equivalent. To this end, we introduce a consume expression that performs resource padding. The amount of resource padding that is needed is automatically determined by the type system and is parametric in the values held by program variables. An advantage of this technique over prior approaches [17], [18] is that it does not change the worst-case resource behavior of many programs. Of course, it would be possible to perform this transformation by padding resource usage dynamically at the end of the program execution, but this would require instrumenting the program to track at runtime the actual resource usage of the program.
Novel resource type systems: In order to verify constant resource usage, as well as to produce quantitative upper and lower-bounds on information leakage via resource behavior, this work extends the theory behind automatic amortized resource analysis (AARA) [19], [20], [21] to automatically derive lower-bound and constant-resource proofs.
Previous AARA techniques are limited to deriving upper bounds. To this end, the resource potential is used as an affine quantity: it must be available to cover the cost of the execution, but excess potential is simply discarded. We show that if potential is treated as a linear resource, then corresponding type derivations prove that programs have constant resource consumption, i.e., the resource consumption is independent of the execution path. Intuitively, this amounts to requiring that all potential must be used to cover the cost and that excess potential is not wasted. Furthermore, we show that if potential is treated as a relevant resource then we can derive lower bounds on the resource usage. Following a similar intuition, this requires that all potential is used, but the available potential does not need to be sufficient to cover the remaining cost of the execution.
We implemented these type systems in Resource Aware ML (RAML) [21], a language that supports user-defined data types, higher-order functions, and other features common to functional languages. Our type inference uses efficient LP solving to characterize resource usage for general-purpose programs in this language. We formalized soundness proofs for these type systems, as well as the one of classic linear AARA [19], in the proof assistant Agda. The soundness is proved w.r.t. an operational cost semantics and, like the type systems themselves, is parametric in the resource of interest.
Contributions: We make the following contributions: • A security type system that incorporates our novel lower-bound and constant-time type systems to prevent and quantify leakage of secrets through resource side channels, as well as an LP-based method that automatically transforms programs into constant-resource versions. • An implementation of these systems that extends RAML. We evaluate the implementation on several examples, including encryption routines and data processing programs that were previously studied in the context of timing leaks in differentially-private systems [8]. • A mechanization of the soundness proofs the two new type systems and classic AARA for upper bounds in Agda. To the best our knowledge, this is also the first formalization of the soundness of linear AARA for worst-case bounds. Technical details including the complete proofs and inference rules can be found on the RAML website [21].

II. LANGUAGE-LEVEL CONSTANT-RESOURCE PROGRAMS
In this section, we define our notion of a constant-resource program. We start with an illustrative example: a login with a username and password. During the login process, the secret password with a high security level is compared with the lowsecurity user input, and the result is sent back to the user. As a result, the pure noninterference property [22], [23] is violated because data flows from high to low. Nevertheless, such a program is often considered secure because it satisfies the relaxed noninterference property [24], [25], [26]. Fig. 1 shows an implementation of the login process in a monomorphically-typed purely-functional language. The arguments h and l are lists of integers that are the bytes of the password and the user input (characters of the hashes). The function returns true if the input is valid and false otherwise.
This implementation is vulnerable against an attacker who measures the execution time of the login function. Because the function returns false immediately on finding a mismatched pair of bytes, the resource usage depends on the size of the longest matching prefix. Based on this observation, the attacker can mount an efficient attack to recover the correct password byte-by-byte. For example, if we assume that there is no noise in the measurements, it requires at most 256 = 2 8 calls to the function to reveal one byte of the secret password. Thus, at most 256 * N runs are needed to recover a secret password of N bytes. If noise is added to the measurements then the number of necessary guesses is increased but the attack remains feasible [1], [4].
One method to prevent this sort of attack is to develop a constant-resource implementation of the compare function that minimizes the information that an attacker can learn from the resource-usage information. Ideally, the resource usage should not be dependent on the content of the secret password, which means it is constant for fixed sizes of all public parameters.
Syntax and semantics: We use the purely-functional first-order language defined in Fig. 2 to formally define the notion of a language-level constant-time implementation. The grammar is written using abstract binding trees [27] ⋄ ∈ {+, −, * , div , mod , =, <>, >, <, and , or } consumption of programs, we first define the operational cost semantics of the language. It is standard big-step semantics instrumented with a non-negative resource counter that is incremented or decremented by a constant at every step. The semantics is parametric in the cost that is used at each step and we call a particular set of such cost parameters a cost model. The constants can be used to indicate the costs of storing or loading a value in the memory, evaluating a primitive operation, binding of a value in the environment, or branching on a Boolean value. It is possible to further parameterize some constants to obtain a more precise cost model. For example, the cost of calling a function may vary according to the number of the arguments. In the following, we will show that the soundness of type systems does not rely on any specific values for these constants. In the examples, we use a cost model in which the constants are 0 for all steps except for calls to the tick function where tick(q) means that we have resource usage q ∈ Q. A negative number specifies that resources (such as stack space) become available.
The cost semantics is formulated using an environment E : VID → Val that is a finite mapping from a set of variable identifiers to values. Evaluation judgements are of the form E q q ′ e ⇓ v where q, q ′ ∈ Q + 0 . The intuitive meaning is that under the environment E and q available resources, e evaluates to the value v without running out of resources and q ′ resources are available after the evaluation. The evaluation consumes δ = q − q ′ resource units. Fig. 12 presents some selected evaluation rules. In the rule E:FUN for function applications, e g is an expression defining the function's body and x g is the argument.
Constant-resource programs: Let Γ : VID → T be a context that maps variable identifiers to base types T . We write |= v : T to denote that v is a well-formed value of type T . The typing rules for values are standard [19], [20], [28] and we omit them here. An environment E is well-formed w.r.t. Γ, denoted |= E : Γ, if ∀x ∈ dom(Γ). |= E(x) : Γ(x). Below we define the notation of size equivalence, written |v| ≈ |u|, which is a binary relation relating two values of the same type.
Informally, a program is constant resource if it has the same quantitative resource consumption under all environments in which values have the same sizes. Let X ⊆ dom(Γ) be a set of variables and E 1 , E 2 be two well-formed environments. Then E 1 and E 2 are size-equivalent w.r.t. X, denoted E 1 ≈ X E 2 , when they agree on the sizes of the variables in X, that is, ∀x ∈ X.|E 1 (x)| ≈ |E 2 (x)|.
, if for all well-formed environments E 1 and E 2 such that E 1 ≈ X E 2 , the following statement holds.
We say that a function g(x 1 , . . . , x n ) is constant resource w.r.t. X if const X (e g ) where e g is the expression defining the function body. We have the following lemma.
Lemma 1. For all e, X, and Y ⊆ X, if const Y (e) then const X (e).
Example. The function p compare in Fig. 4  Intuitively, this implementation is constant w.r.t. the given cost model for fixed sizes of all public parameters, e.g., the lengths of argument lists. However, it might be not constant resource at a lower level, e.g., machine code on modern hardware, because the cost model does not precisely capture the resource consumption of the instructions executed on the hardware. Moreover, the compilation process can interfere with the resource behavior. It may introduce a different type of leakage that could reveal the secret data on the lower level. For instance, memory accesses would allow an attacker with access to the full trace of memory addresses accessed to infer the content of the password. This leakage can be exploited via cache-timing attacks [29], [30]. In addition, in some modern processors, execution time of arithmetic operations may vary depending on the values of their operands and the execution time of conditionals is affected by branch prediction.

III. A RESOURCE-AWARE SECURITY TYPE SYSTEM
In this section we introduce a new type system that enforces resource-aware noninterference to prevent the leakage of information in high-security variables through lowsecurity channels. In addition to preventing leakage over the usual input/output information flow channels, our system incorporates the constant-resource type system discussed in Section IV to ensure that leakage does not occur over resource side channels.
The notion of security addressed by our type system considers an attacker who wishes to learn information about secret data by making observations of the program's public outputs and resource usage. We assume an attacker who is able to control the value of any variable she is capable of observing, and thus to influence the program's behavior and resource consumption. However, in our model the attacker can only observe the program's total resource usage upon termination, and cannot distinguish between intermediate states or between terminating and non-terminating executions.

A. Security types
To distinguish parts of the program under the attacker's control from those that remain secret, we annotate types with labels ranging over a lattice (L , ⊑, ⊔, ⊥). The elements of L correspond to security levels partially-ordered by ⊑ with a unique bottom element ⊥. The corresponding basic security types take the form: A security context Γ s is a partial mapping from variable identifiers and the program counter pc to security types. The context assigns a type (unit, k) to pc to track information that may propagate through control flow as a result of branching statements. The security type for lists contains a label L(S) for the elements, as well as a label k for the list's length.
As in other information flow type systems, the partial order k ⊑ k ′ indicates that the class k ′ is at least as restrictive as k, i.e., k is allowed to flow to k ′ . We assume a non-trivial security lattice that contains at least two labels: ℓ (low security) and h (high security), with ℓ ⊑ h. Following the convention defined in FlowCaml [31], we also make use of a guard relation k ⊳ S, which denotes that all of the labels appearing in S are at least as restrictive as k. The definition  is given in Figure 13 along with its dual notion S ◭ k, called the collecting relation, and the standard subtyping relation To refer to sets of variables by security class, we write [Γ s ] ◭k to denote the set of variable identifiers x in the domain of Γ s such that Γ s (x) ◭ k, and define k⊳ [Γ s ] similarly. This gives us the set of variables upper-and lower-bounded by k, respectively. Conversely, we define [Γ s ] ◭k = {x ∈ dom(Γ s ) : Γ s (x) ◭ k}, the set of variables more restrictive than k. To refer to the set of variables strictly bounded below by k 1 and above by k 2 , we write k1⊳ [Γ s ] ◭k2 . Given two well-formed environments E 1 and E 2 , we say that they are k-equivalent w.r.t Γ s if they agree on all variables with label at most k: This relation captures the attacker's observational equivalence between the two environments. The first-order security types take the following form. The annotation pc indicates the security level of the program counter, i.e., a lowerbound on the label of any observer who is allowed to learn that a given function has been invoked. The const annotation denotes that the function body respects resourceaware noninterference.
pc ∈ L F s : Figure 5. Guards, collecting security labels, and subtyping (Atoms = {unit, int, bool}) partial mapping from a set of function identifiers to a nonempty sets of first-order security types.

B. Resource-aware noninterference
We consider an adversary associated with label k 1 ∈ L , who can observe and control variables in [Γ s ] ◭k1 . Intuitively, we say that a program P satisfies resource-aware noninterference at level (k 1 , k 2 ) w.r.t Γ s , where k 1 ⊑ k 2 , if 1) the behavior of P does not leak any information about the contents of variables more sensitive than k 1 , and 2) does not leak any information about the contents or sizes of variables more sensitive than k 2 . The definition follows. Definition 2. Let E 1 and E 2 be two well-formed environments and Γ s be a security context sharing their domain. An expression e satisfies resource-aware noninterference at level (k 1 , k 2 ) for k 1 ⊑ k 2 , if whenever E 1 and E 2 are: The final condition in Defintion 2 ensures two properties. First, requiring that v 1 = v 2 provides noninterference [22], given that E 1 and E 2 are observationally equivalent. Second, the requirement p 1 −p ′ 1 = p 2 −p ′ 2 ensures that the program's resource consumption will remain constant w.r.t changes in variables from the set [Γ s ] ◭k1 . This establishes noninterference w.r.t the program's final resource consumption, and thus prevents the leakage of secret information.
Before moving on, we point out an important subtlety in this definition. We require that all variables in k1⊳ [Γ s ] ◭k2 begin with equivalent sizes, but not those in k2⊳ [Γ s ]. By fixing this quantity in the initial environments, we assume that an attacker is able to control and observe it, so it is not protected by the definition. This effectively establishes three classes of variables, i.e., those whose size and content are observable to the k 1 -adversary, those whose size (but not content) is observable, and those whose size and content remain secret. In the remainder of the text, we will simplify the technical development by assuming that the third and most-restrictive class is empty, and that all of the secret variables reside in k1⊳ [Γ s ] ◭k2 .

C. Proving resource-aware noninterference
There are two extreme ways of proving resource-aware noninterference. Assume we already have established classic noninterference, the first way is to additionally prove constant-resource usage globally by forgetting the security labels and showing that the program has constant-resource usage. This is a sound approach but it requires us to reason about parts of the programs that are not affected by secret data. It would therefore result in the rejection of programs that have the resource-aware noninterference property but are not constant resource. The second way is to prove constant resource usage locally by ensuring that every conditional that branches on secret values is constant time. However, this local approach is problematic because it is not compositional. Consider the following examples where rev is the reverse function. If we assume a cost model in which we count the number of function calls then the cost of rev(x) is |x|. So rev is constant resource w.r.t. its argument. Moreover, the expression if b then x else [] is constant resource. However, f1 is not constant resource. In contrast, the conditional in f2 is not constant resource. But f2 is a constant-resource function. The function f2 can be automatically analyzed with the constantresource type system from Section IV while f1 is correctly rejected. The idea of our type system for resource-aware noninterference is to allow both global and local reasoning about resource consumption as well as arbitrary intermediate levels.
We ensure that every expression that is typed in a high security context is part of a constant-resource expression. In this way, we get the benefits of local reasoning without losing compositionality.

D. Typing rules and soundness
We combine our type system for constant resource usage with a standard information flow type system which based on FlowCaml [32]. The interface between the two type systems is relatively light and the idea is applicable to other costanalysis methods as well as other security type systems.
In the type judgement, an expression is typed under a type context Γ s and a label pc. The pc label can be considered an upper bound on the security labels of all values that affect the control flow of the expression and a lower bound on the labels of the function's effects [32]. As mentioned earlier, we will simplify the technical development by assuming that the third and most-restrictive class is empty, that is, the typing rules here guarantee that well-typed expressions provably satisfy the resource-aware noninterference property w.r.t. changes in variables from the set [Γ s ] ◭k1 , say X. We define two type judgements of the form pc; Σ s ; Γ s const e : S and pc; Σ s ; Γ s e : S .
The judgement with the const annotation states that under a security configuration given by Γ s and the label pc, e has type S and it satisfies resource-ware noninterference w.r.t. changes in variables from X. The second judgement indicates that e satisfies the noninterference property but does not make any guarantees about resource-based side channels. Selected typing rules are given in Fig. 14. We implicitly assume that the security types and the resourceannotated counterparts have the same base types. We write [const] to denote it is optional, and const X (e) if e is welltyped in the constant-resource type system w.r.t. X (i.e., Σ r ; Γ r q q ′ e : A, ). We will discuss the constantresource type system in Section IV.
Note that the standard information flow typing rules [33], [32] can be obtained by removing the const annotations from all judgements. Consider for instance the rule SR:IF for conditional expressions. By executing the true or false branches, an adversary could gain information about the conditional value whose security label is k x . Therefore, the conditional expression must be type-checked under a security assumption at least as restrictive as pc and k x . This is a standard requirement in any information flow type system. In the following, we will focus on explaining how the rules restrict the observable resource usage instead of these classic noninterference aspects.
The most interesting rules are SR:C-GEN and the rules for let and if expressions, which block leakage over resource usage when branching on high security data. SR:C-GEN allows us to globally reason about constant resource usage for an arbitrary subexpression that has the noninterference property. For example, we can apply SR:IF, the standard rule for conditionals, first and then SR:C-GEN to prove that its super-expression is constant resource. Alternatively, we can  The reasoning is similar for SR:L-IF where we require that the variable x does not depend on high security data. Leaf expressions such as op ⋄ (x 1 , x 2 ) and cons(x h , x t ) have constant resource usage. Thus their judgements are always associated with the qualifier const as shown in the rule SR:B-OP. The rule SR:C-FUN states that if a function's body has the resource-aware noninterference property then the function application has the resource-aware noninterference property too. If the argument's label is low security data, bounded below by k 1 , then the function application has the resource-aware noninterference property since the value of the argument is always the same under any k-equivalent environments. It is reflected by rule SR:L-ARG. Example. Recall the functions compare and p compare in Fig. 1. Suppose the content of the first list is secret and the length is public. Thus it has type (L(int, h), ℓ). While the second list controlled by adversaries is public, hence it has type (L(int, ℓ), ℓ). Assume that the pc label is ℓ and The return value's label depends on the content of the elements of the first list whose label is h. Thus it must be assigned the label h to make the functions well-typed.
Here, both functions satisfy the noninterference property at security label ℓ. However, only p compare is a resourceaware noninterference function w.r.t. [Γ s ] ◭ℓ , or the secret list.
Example. Consider the following function cond rev in which rev is the standard reverse function.
We now prove the soundness of the type system w.r.t. the resource-aware noninterference property. It states that if e is a well-typed expression with the const annotation then e is a resource-aware noninterference expression at level k 1 .
The following two lemmas are needed in the soundness proof. The first lemma states that the type system satisfies the standard simple security property [34] and the second shows that the type system prove classic noninterference.
Lemma 3. Let pc; Σ s ; Γ s ⊢ e : S or pc; Σ s ; Γ s const e : S, and pc; Σ s ; Γ s const e : S then e is a resource-aware noninterference expression at k 1 .
Proof: The proof is done by induction on the structure of the typing derivation and the evaluation derivation. Let X be the set of variables We illustrate one case of the conditional expression. Suppose e is of the form if(x, e t , e f ), thus the typing derivation ends with an application of either the rule SR:L-IF or SR: By the hypothesis we have const X (e). Thus by Theorem 3, it follows

RESOURCE USAGE
We now discuss how to automatically and statically verify constant resource usage, upper bounds, and lower bounds. For upper bounds we rely on existing work on automatic amortized resource analysis [19], [21]. This technique is based on an affine type system. For constant resource usage and lower bounds we introduce two new sub-structural resource-annotated type systems: The type system for constant resource usage is linear and the one for lower bounds is relevant.

A. Background
Amortized analysis: To statically analyze a program with the potential method [35], a mapping from program points to potentials must be established. One has to show that the potential at every program point suffices to cover the cost of any possible evaluation step and the potential of the next program point. The initial potential is then an upper bound on the resource usage of the program. The worstcase number of ticks executed by fitler succ(ℓ) and fs twice(ℓ) is 8|ℓ| + 1 and 11|ℓ| + 2 respectively. In the best-case the functions execute 3|ℓ| + 1 and 6|ℓ| + 2 ticks, respectively. The resource consumption is not constant.
Linear potential for upper bounds: To automate amortized analysis, we fix a format of the potential functions and use LP solving to find the optimal coefficients. To infer linear potential functions, inductive data types are annotated with a non-negative rational numbers q [19]. For example, the type L q ( bool ) of Boolean lists with potential q defines potential q·n, where n is the number of list's elements.
This idea is best explained by example. Consider the function filter succ below that filters out positive numbers and increments non-positive numbers. As in RAML, we use OCaml syntax and tick commands to specify resource usage. If we filter out a number then we have a high cost (8 resource units) since x is, e.g., sent to an external device. If x is incremented we have a lower cost of 3 resource units. As a result, the worst-case resource consumption of filter succ(ℓ) is 8|ℓ| + 1 (where 1 is for the cost that occurs in the nil case of the match). The function fs twice(ℓ) applies filter succ twice, to ℓ and to the result of filter succ(ℓ). The worst-case behavior appears if no list element is filtered out in the first call and all elements are filtered out in the second call. The worst-case behavior is thus 11|ℓ|+2. These upper bounds can be expressed with the following annotated function types, which can be derived using local type rules in Fig. 8.
Intuitively, the first function type states that an initial potential of 8|ℓ| + 1 is sufficient to cover the cost of filter succ(ℓ) and there is 0|ℓ ′ |+0 potential left where ℓ ′ is the result of the computation. This is just one possible potential annotation of many. The right choice of the potential annotation depends on the use of the function result. For example, for the inner call of filter succ in fs twice we need the following annotation.
filter succ : It states that the initial potential of 11|ℓ| + 2 is sufficient to cover the cost of filter succ(ℓ) and there is 8|ℓ ′ |+1 potential left to be assigned to the returned list ℓ ′ . The potential of the result can then be used with the previous type of filter succ to pay for the cost of the outer call.
We can summarize all possible types of filter succ with a linear constraint system. In the type inference, we generate such a constraint system and solve it with an off-the-shelf LP solver. To obtain tight bounds, we perform a whole-program analysis and minimize the coefficients in the input potential. Surprisingly, this approach-as well as the new concepts we introduce here-can be extended to polynomial bounds [36], higher-order functions [37], [21], polymorphism [38], and user-defined inductive types [38], [21].

B. Resource annotations
The resource-annotated types are base types in which the inductive data types are annotated with non-negative rational numbers, called resource annotations.
is a partial mapping from variable identifiers to resource-annotated types. The underlying base type and context denoted by A, and Γ r respectively can be obtained by removing the annotations. We extend all definitions such as |v|, |= E : Γ and ≈ for base data types to resource-annotated data types by ignoring the annotations.
We now formally define the notation of potential. The potential of a value v of type A, written Φ(v : A), is defined by the function Φ : Val → Q + 0 as follows.
Let Γ r be a context and E be a well-formed environment w.
The following lemma states that the potential is the same under two well-formed size-equivalent environments.
Annotated first-order data types are given as follows, where q and q ′ are rational numbers.
is a partial mapping from function identifiers to a nonempty sets of annotated first-order types. That means a function can have different resource annotations depending on the context. The underlying base types are denoted by F . And the underlying base signature is denoted by Σ r where Σ r (f ) = Σ r (f ).

C. Type system for constant resource consumption
The typing rules of the constant-resource type system define judgements of the form: where e is an expression and q, q ′ ∈ Q + 0 . The intended meaning is that in the environment E, q + Φ E (Γ r ) resource units are sufficient to evaluate e to a value v with type A and there are exactly q ′ + Φ(v : A) resource units left over.
The typing rules form a linear type system. It ensures that every variable is used exactly once by allowing exchange but not weakening or contraction [39]. The rules can be organized into syntax directed and structural rules.
Syntax-directed rules: The syntax-directed rules are shared among all type systems and selected rules are listed in Fig. 8. Rules like A:VAR and A:B-OP for leaf expressions (e.g., variable, binary operations, pairs) have fixed costs as specified by the constants K x . Note that we require all available potential to be spent. The cost of the function call is represented by the constant K app in the rule A:FUN and the argument carries the potential to pay for the function execution. In the rule A:LET, the cost of binding is represented by the constant K let . The potentials carried by the contexts Γ r 1 and Γ r 2 are passed sequentially through the sub derivations. Note that the contexts are disjoint since our type system is linear. Multiple uses of variables must be introduced through the rule A:SHARE. Thus, the context split is deterministic. The rule A:IF is the key rule for ensuring constant resource usage. By using the same context Γ r for typing both e t and e f , we ensure that the conditional expression has the same resource usage in size-equivalent environments independent of the value of the Boolean variable x. The rules for inductive data types are crucial for the interaction of the linear potential annotations with the constant potential, in which A:CONS shows how constant potential can be associated with a new data structure. The dual is A:MATCH-L, which shows how potential associated with data can be released. It is important that these transitions are made in a linear fashion: potential is neither lost or gained.
Sharing relation: The share expression makes multiple uses of a variable explicit. While multiple uses of a variable seem to be in conflict with the linear type discipline, the sharing relation way. It apportions potential to ensure that the total potential associated with all uses is equal to the potential initially associated with the variable. This relation is only defined for structurally-identical types which differ in at most the resource annotations. Structural rules: To allow more programs to be typed we add two structural rules to the type system which can be applied to every expression. These rules are specific to the the constant-resource type system.
The rule C:RELAX reflects the fact that if it is sufficient to evaluate e with p available resource units and there are p ′ resource units left over then e can be evaluated with p + c resource units and there are exactly p ′ + c resource units left over, where c ∈ Q + 0 . Rule C:WEAKENING states that an extra variable can be added into the given context if its potential is zero. The condition is enforced by These rules can be used in branchings such as the conditional or the pattern match to ensure that subexpressions are typed using the same contexts and potential annotations. Example. Consider again the function p compare in Fig. 4 in which the nil case of the second matching on l is padded with tick(5.0); aux(false,xs,[]) and the resource consumption is defined using tick annotations. The resource usage of p compare(h, ℓ) is constant w.r.t. h, that is, it is exactly 5|h| + 1. This is reflected by the following type. Soundness: That soundness theorem states that if e is well-typed in the resource type system and evaluates to a value v then the difference between the initial and the final potential is the net resources usage. Moreover, if the potential annotations of the return value and all variables not belonging to a set X ⊆ dom(Γ r ) are zero then e is constant-resource w.r.t. X. Theorem 2. If |= E : Γ r , E ⊢ e ⇓ v, and Σ r ; Γ r q q ′ e : A, then for all p, r ∈ Q + 0 such that p = q + Φ E (Γ r ) + r, there exists p ′ ∈ Q + 0 satisfying E p p ′ e ⇓ v and p ′ = q ′ + Φ(v : A) + r.
Proof: The proof proceeds by a nested induction on the derivation of the evaluation judgement and the typing judgement, in which the derivation of the evaluation judgement takes priority over the typing derivation. We need to induct on both, evaluation and typing derivation. An induction on only the typing derivation would fail for the case of function application, which increases the size of the typing derivation, while the size of the evaluation derivation does not increase. An induction on only the evaluation judgement would fail because of structural rules such as C:WEAKENING. If such a rule is the final step in the derivation then the size of typing derivation decreases while the length of evaluation derivation is unchanged. The additional constant r is needed to make the induction case for the let rule work.
then e is constant resource w.r.t. X ⊆ dom(Γ r ).

D. Type system for upper bounds
If we treat potential as an affine resource then we arrive at the original amortized analysis for upper bounds [19]. To this end, we allow unrestricted weakening and a relax rule in which we can waste potential.
Additionally, we can use subtyping to waste linear potential [19]. (See the dual definition for subtyping for lower bounds below.) Similarly to Theorem 2, we can prove the following theorem.

E. Type system for lower bounds
The type judgements for lower bounds have the same form and data types as the type judgements for constant resource usage and upper bounds. However, the intended meaning of the judgement Σ r ; Γ r q q ′ e : A is the following. Under given environment E, less than q +Φ E (Γ) resource units are not sufficient to evaluate e to a value v so that more than q ′ + Φ(v : A) resource units are left over.
The syntax-directed typing rules are the same as the rules in the constant-resource type system as given in Fig. 8. In addition, we have the structural rules in Fig. 9. The rule L:RELAX is dual to U:RELAX. In L:RELAX, potential is treated as a relevant resource: We are not allowed to waste potential but we can create potential out of the blue if we ensure that we either use it or pass it to the result. The same idea is formalized for the linear potential with the sub-typing rules L:SUBTYPE and L:SUPERTYPE. The subtyping relation is defined as follows.
It holds that if A <: B then A = B and Φ(v : A) ≤ Φ(v : B). Suppose that it is not sufficient to evaluate e with p available resource units to get p ′ resource units left over. L:SUBTYPE reflects the fact that we also cannot evaluate e with p resources get more than p ′ resource units after the evaluation. L:SUPERTYPE says that we also cannot evaluate e with less than p and get p ′ resource units afterwards.
Example. Consider again the functions filter succ and fs twice given in Fig. 7 in which the resource consumption is defined using tick annotations. The best-case resource usage of filter succ(ℓ) is 3|ℓ| + 1 and best-case resource usage of (L:SUBTYPE) Σ r ; Γ r q q ′ e:A A<:B Σ r ; Γ r q q ′ e : B (L:SUPERTYPE) Σ r ; Γ r , x:B q q ′ e : C A<:B Σ r ; Γ r , x : A q q ′ e : C fs twice(ℓ) is 6|ℓ| + 2. This is reflected by the following function types for lower bounds.
filter succ : L 3 (int) fs twice : L 6 (int) To derive the lower bound for fs twice, we need the same compositional reasoning as for the derivation of the upper bound. For the inner call of filter succ we use the type filter succ : L 6 (int) It can be understood as follows. If the input list carries 6 potential units per element then, for each element, we can either use all 6 (if case) or we can use 3 and assign 3 to the output (else case).
The type system for lower bounds is a relevant type system [39]. That means every variable is used at least once by allowing exchange and contraction properties, but not weakening. However, as in the constant-time type system we allow a restricted form of weakening if the potential annotations are zero using the rule L:WEAKENING. The following lemma states formally the contraction property which is derived in Fig. 10.
The following theorems establish the soundness of the analysis. The proofs can be found in the TR [28]. Theorem 6 is proved by induction and Theorem 5 follows by contradiction.

F. Mechanization
We mechanized the soundness proofs for both the two new type systems as well as the classic AARA type system using the proof assistant Agda. The development is roughly 4000 lines of code, which includes the inference rules, the operational cost semantics, a proof of type preservation, and the soundness theorems for each type system.
One notable difference is our implementation of the typing contexts. In Agda our contexts are implemented as lists of pairs of variables and their types. Moreover, in our typing rules whenever a variable is added to the context we require the variable is fresh with respect to the existing context. This requirement is important as it allows us to preserve the invariant that the context is well formed with respect to the environment as we induct over typing and evaluation judgements in our soundness proofs. Furthermore, as our typing contexts are ordered lists we added an exchange rule to our typing rules.
Another important detail is in the implementation of potential. Potential Φ(v : A) for a value only is defined for well formed inputs. Inputs such as Φ( nil : bool) are not defined. Agda is total language and as such prohibits users from implementing partial functions. Thus we require in our Agda implementation that when calculating the potential of a value of a given type the user provide a derivation that the value is well formed with respect to that type. Similarly when calculating the potential of a context, Φ E (Γ r ), with respect to an environment we require that the user provide a derivation that the context is well formed with respect to that environment.
Lastly, whereas the type systems and proofs presented here used positive rational numbers, in the Agda implementation we use natural numbers. This deviation was simply due to the lacking support for rationals in the Agda standard library. By replacing a number of trivial lemmas, mostly related to associativity and commutativity, the proofs and embeddings could be transformed to use rational numbers instead.

V. QUANTIFYING AND TRANSFORMING OUT LEAKAGES
We present techniques to quantify the amount of information leakage through resource usage and transform leaky programs into constant resource programs. The quantification relies on the lower and upper bounds inferred by our resource type systems. The transformation pads the programs with dummy computations so that the evaluations consume the same amount of resource usage and the outputs are identical with the original programs. In the current implementation, these dummy computations are added into programs by users and the padding parameters are automatically added by our analyzer to obtain the optimal values. It would be straightforward to make the process fully automatic but the interactive flavor of our approach helps to get a better understanding of the system.

A. Quantification
Recall from Section III that we assume an adversary at level k 1 who is always able to observe 1) the values of variables in [Γ s ] ◭k1 , and 2) the final resource consumption of the program. For many programs, it may be the case that changes to the secret variables [Γ s ] ◭k1 effect observable differences in the program's final resource consumption, but only allow the attacker to learn partial information about the corresponding secrets. In this section, we show that the upper and lower-bound information provided by our type systems allow us to derive bounds on the amount of partial information that is leaked.
To quantify the amount of leaked information, we measure the number of distinct environments that the attacker could deduce as having produced a given resource consumption observation. However, because there may be an unbounded number of such environments, we parameterize this quantity on the size of the values contained in each environment. Let E N denote the space of environments with values of size characterized by N . Given an environment E and expression e, define U (E, e) = p δ such that E p p ′ e ⇓ v and p δ = p − p ′ . Then for an expression e and resource observation p δ , we define the set R N (e, p δ ) which captures the attacker's uncertainty about the environment which produced p δ : Notice that when |R N (e, p)| = 1, the attacker can deduce exactly which environment was used, whereas when this quantity is large little additional information is learned from p δ . This gives us a natural definition of leakage, which is obtained by aggregating the inverse of the cardinality of R N over the possible initial environments of e: corresponds to our intuition about leakage. When e leaks no information through resource consumption, then each term in the summation will be 1/|E sizes | giving C N (e) = 0, whereas if e leaks perfect information about its starting environment then each term will be 1, leading to C N (e) = |E N | − 1. Lemma 7. Assume that environments are sampled uniformrandomly from E N . Then the Shannon entropy of P e N is given by C N (e): H(P e N ) ≤ log 2 (C N (e) + 1) Lemma 6 leverages Theorem 7 to derive an upper-bound on leakage from upper and lower resource bounds. This result only holds when the resource observations of e are integral, which ensures the interval [l e (N ), u e (N )] ⊇ P e N is finite. Lemma 7 relates C N (e) to Shannon entropy, which is commonly used to characterize information leakage [40], [41], [42].

B. Transformation
To transform programs into constant resource programs we extend the type system for constant resource use from Section IV. Recall that the type system treats potential in a linear fashion to ensure that potential is not wasted. We will now add sinks for potential which will be able to absorb excess potential. At runtime the sinks will consume the exact amount of resources that have been statically-absorbed to ensure that potential is still treated in a linear way. The advantage of this approach is that the worst-case resource consumption is often not affected by the transformation. Additionally, we do not need to keep track of resource usage at runtime to pad the resource usage at the sinks, because the amount of resource that must be discarded is staticallydetermined by the type system. Finally, we automatically obtain a type derivation that serves as a proof that the transformation is constant resource.
More precisely, the sinks are represented by the syntactic form: consume (A,p) (x). Here, A is a resource-annotated type and p ∈ Q ≥0 is a non-negative rational number. The idea is that A and p define the resource consumption of the expression. In the implementation, the user only has to write consume(x), and the annotations are added via automatic syntax elaboration during the resource type inference.
Let E be a well-formed environment w.r.t. Γ r . For every x ∈ dom(Γ) with Γ r (x) = A, the expression consume (A,p) (x) consumes Φ(E(x) : A) + p resource units and evaluates to () . The evaluation and typing rules for sinks are: The extension of the proof of Theorem 2 to consume expressions is straightforward.
Adding consume expressions: Let e i be a subexpression of e and let e ′ i be the expression let(z, consume(x 1 , · · · , x n ), z.e i ) for some variables x i . Let e ′ be the expression obtained from e by replacing e i with e ′ i . We write e ֒→ e ′ for such a transformation. Note that additional share and let expressions have to be added to convert e ′ i into share-let normal form. Lemma 8. If Σ; Γ ⊢ e : T , E ⊢ e ⇓ v, and e ֒→ e ′ then Σ; Γ ⊢ e ′ : T and E ⊢ e ′ ⇓ v.
To transform an expression e into a constant resource expressions we perform multiple transformations e ֒→ e ′ which do not affect the type and semantics of e. This can be done automatically but in our implementation it works in an interactive fashion, meaning that users are responsible for the locations where consume expressions are put. The analyzer will infer the annotations A and constants p of the given consume expressions during type inference. If the inference is successful then we have const X (e ′ ) for the transformed program e ′ .
Example. Recall the function compare form Fig. 1. To turn compare into a constant resource function. We insert consume expressions as shown below. Users can insert many consume expressions and the analyzer will determine which consumes are actually needed. We automatically obtain the following typing of the transformed function and the consume expressions: The worst-case resource consumption of the unmodified function c compare is 1 + 5|h|. Thus the consumption of the first consume must be 5 + 5(|h| − 1 − |ℓ|) when h is longer than l. Otherwise, the consumption is zero. The second one consumes 1 + 5(|h 1 | − 1), where h 1 is the sub-list of h from the first node which is different from the corresponding node in l.

VI. IMPLEMENTATION AND EVALUATION
Type Inference: Type inference for the constant resource and lower bound systems are implemented in   [21]. RAML is integrated into Inria's OCaml compiler and supports polynomial bounds, user-defined inductive types, higher-order functions, polymorphism, arrays, and references. All features are implemented for the new type systems, as they are straightforward extensions of the simplified rules presented in this paper. The implementation is publicly available in an easy-to-use web interface [43].
The type inference is technically similar to the inference of upper bounds [19]. We first integrate the structural rules of the respective type system in the syntax directed rules. For example, weakening and relaxation is applied at branching points such as conditional. We then compute a type derivation in which all resource annotations are replace by (yet unknown) variables. For each type rule we produce a set of linear constraints that specify the properties of valid annotations. These linear constraints are then solved by the LP solver CLP to obtain a type derivation in which the annotations are rational numbers.
An interesting challenge lies in finding a solution for the linear constraints that leads to the best bound for a given function. For upper bounds, we simply disregard the potential of the result type and provide an objective function that minimizes the annotations of the arguments. The same strategy works the constant-time type systems. An interesting property is that the solution to the linear program is unique if we require that the potential of the result type is zero. To obtain the optimal lower bound we want to maximize the potential of the arguments and minimize the potential of the result. We currently simply maximize the potential of the arguments while requiring the potential of the result to be zero. Another approach would be to first minimize the output potential and then maximize the input potential.
Resource-aware noninterference: We are currently integrating our constant-time type system with FlowCaml [31]. The combined inference is based on the typing rules in Fig. 14. It is possible to derive a set of type inference rules in the same way as for FlowCaml [44], [32]. One of the challenges in the integration is interfacing Flow-Caml's type inference with our constant-time type system in rule SR:C-GEN. In the implementation, we intend for each application of SR:C-GEN to generate an intermediate representation of the expression in RAML for the expression under consideration, in which all types are annotated with fresh resource annotations along with the set of variables X. The expression is marked with the qualifier const if RAML can prove that it is constant time. The type inference algorithm always tries to apply the syntax-directed rules first before using SR:C-GEN.
Evaluation: Table I shows the verification and computation of constant resource usage, lower, and upper bounds for different functions, together with the lines of code (LOC) of the analyzed function and the run time of the analysis in seconds. Note that lower and upper bounds are identical when a function is constant. In the computed bounds, n is the size of the first argument, m = max 1≤i≤n m i where m i are the sizes of the first argument's elements, x is the size of the second argument, and z is the value of the third argument.
The cost models are specified by different cost metrics that are appropriate for the respective application, e.g., number of evaluation steps or number of multiplication operations. Note that the computed upper bounds are also the resource usages of functions which are padded using consume expressions. The experiments were run on a machine with Intel Core i5 2.4 GHz processor and 8GB RAM under OS X 10.11.5. The run time of the analysis varies from 0.02 to 14.34 seconds depending on the function's code complexity. The example programs that we analyzed consist of commonly-used primitives ( cond rev , trunc rev , compare , find , filter ), functions related to cryptography ( tea enc , tea dec , rsa ), and examples taken from Haeberlan et al. [8] ( ipquery , kmeans ). The full source code of the examples can be found in the technical report [28].
The encryption functions tea enc and tea dec correspond to the encryption and decryption routines of the Corrected Block Tiny Encryption Algorithm [45], a block cipher presented by Needham and Wheeler in an unpublished technical report in 1998. Our implementation correctly identifies these operations as constant-time in the number of primitive operations performed. We applied this cost model for the tea examples due to the presence of bitwise operations in the original algorithm, which are not currently supported in RAML. In order to derive a more meaningful bound, we implemented bitwise operations in the example source and counted them as single operations.
The two examples taken from Haeberlen et al. [8] were originally created in a study of timing attacks in differentially-private data processing systems. ipquery applies pattern matching to a database derived from Apache server logs, counting the number of matches and nonmatches. kmeans implements the k-means clustering algorithm [46], which partitions a set of geometric points into k clusters that minimize the total inter-cluster distance between points. Haeberlen et al. demonstrated that when a query applied to a dataset introduces attacker-observable timing variations, then the privacy guarantees provided by differential privacy are negated. To address this, they proposed a mitigation approach that enforces constant-time behavior by aborting or padding the query's runtime. Our implementation is able to determine that the queries, as we implemented them, were constant-time to begin with, and thus did not need black-box mitigation.

VII. RELATED WORK
Resource bounds: Our work builds on past research on automatic amortized resource analysis (AARA). AARA has been introduced by Hofmann and Jost for a strict first-order functional language with built-in data types to derive linear heap-memory bounds [19]. It has then been extended to polynomial bounds [47], [36], [48], [59], [60] for strict and higher-order [37], [21] functions. AARA has also been used to derive linear bounds for lazy functional programs [49], [50] and object-oriented programs [51], [52]. In another line of work, the technique has been integrated into separation logic [53] to derive bounds that depend on mutable datastructures, and into Hoare logic to derive linear bounds that depend on integers [54], [55]. Amortized analysis has also been used to manually verify the complexity of algorithms and data-structures using proof assistants [56], [57]. In contrast to our work, these techniques can only derive upper bounds and cannot prove constant resource consumption.
Automatic resource bound analysis is also actively studied for imperative languages using recurrence relations [72], [73], [74] and abstract interpretation [75], [76], [77], [78], [79]. While these techniques focus on worst-case bounds, it is possible to use similar techniques for deriving lower bounds [80]. The advantage of our method is that it is compositional, deals well with amortization effects, and works for language features such as user-defined data types and higher-order functions. Another approach to (worstcase) bound analysis is based on techniques from term rewriting [81], [82], [83], which mainly focus on upper bounds. One line of work [84] derives lower bounds on the worst-case behavior of programs which is different from our lower bounds on the best-case behavior.
Side channels: Analyzing and mitigating potential sources of side channel leakage is an increasingly wellstudied area. Several groups have proposed using type systems or other program analyses to transform programs into constant-time versions by padding with "dummy" commands [85], [86], [87], [40], [88], [16]. Because these systems do not account for timing explicitly, as is the case for our work, this approach will in nearly all cases introduce an unnecessary performance penalty. The most recent system by Zhang et al. [40] describes an approach for mitigating side channels using a combination of security types, hardware assistance, and predictive mitigation [89]. Unlike the type system in Section III, they do not guarantee that information is not leaked through timing. Rather, they show that the amount of this leakage is bounded by the variation of the mitigation commands.
Köpf and Basin [42] presented an information-theoretic model for adaptive side-channel attacks that occur over multiple runs of a program, and an automated analysis for measuring the corresponding leakage. Because their analysis is doubly-exponential in the number of steps taken by the attacker, they describe an approximate version based on a greedy heuristic. Mardziel et al. [90] later generalized this model to probabilistic systems, secrets that change over time, and wait-adaptive adversaries. Pasareanu et al. [91] proposed a symbolic approach for the multi-run setting based on MaxSAT and model counting. Doychev et al. [92] and Köpf et al. [41] consider cache side channels, and present analyses that over-approximate leakage using modelcounting techniques. While these analyses are sometimes able to derive useful bounds on the leakage produced by binaries on real hardware, they do not incorporate security labels to distinguish between different sources, and were not applied to verifying constant-time behavior.
FlowTracker [14] and ct-verif [13] are both constant-time analyses built on top of LLVM which reason about timing and other side-channel behavior indirectly through control and address-dependence on secret inputs. VirtualCert [15] instruments CompCert with a constant-time analysis based on similar reasoning about control and address-dependence.
These approaches are intended for code that has been written in "constant-time style", and thus impose effective restrictions on the expressiveness of the programs that they will work on. Because our approach reasons about resources explicitly, it imposes no a priori restrictions on program expressiveness.
Information flow: A long line of prior work looks at preventing undesired information flows using type systems. Sabelfeld and Myers [93] present an excellent overview of much of the early work in this area. The work most closely related to our security type system is FlowCaml [32], which provides a type system that enforces noninterference for a core of ML with references, exceptions, and letpolymorphism. The portion of our type system that applies to traditional noninterference coincides with the rules used in FlowCaml. However, the rules in our type system are not only designed to track flows of information, but they are also used to incorporate the information flow and resource usage behavior such as the rules SR:L-IF and SR:L-LET. Moreover, our type system constructs a flexible interface between FlowCaml and the resource type system, which means the rules can be easily adapted to integrate into any information-flow type system.
The primary difference between our work and the prior work on information-flow type systems is best summarized in terms of our attacker model. Whereas prior work assumes an attacker that can manipulate low-security inputs and observe low-security outputs, our type system enhances this attacker by granting the ability to observe the program's final resource consumption. This broadens the relevant class of attacks to include resource side channels, which we prevent by extending a traditional information flow type system with explicit reasoning about the resource behavior of the program.

VIII. DISCUSSION
The definition of resource-aware noninterference given in Definition 2 assumes an adversary whose observations of resource consumption match the cost semantics with respect to the cost model given in Section IV. Depending on how the costs are parameterized, this may not match the actual resource use in a physical environment on modern hardware. Architectural features such as caching and variable-duration instructions need to be accounted for in the cost semantics, or the guarantees might not hold in practice [94], [7], [95]. Moreover, additional artifacts of the compilation process can affect the constant-resource guarantees established by the type system. Certain optimization passes and garbage collectors might affect timing properties in ways that lead to vulnerabilities if not accounted for by the cost semantics.
The cost semantics used in this work is conceptually straightforward, and corresponds to the resource model encapsulated by the high-level programming language. Accordingly, our verifier is oblivious to the machine instructions and operand values that are eventually executed after the highlevel code is compiled. In particular, the fact that our cost model effectively counts the total number of language primitives that are executed, and not the corresponding processor instructions with caching and other micro-architectural effects accounted for, means that compiled programs may not satisfy resource-aware noninterference in practice despite being provable within our type system.
Although architectural timing channels are nominally invisible at the source-language level, it may be possible to incorporate these aspects into the cost semantics with specific assumptions about the target platform and compiler toolchain. Doing so with a high degree of precision is challenging, as the semantics may need to track extensive state to accurately reflect the timing behavior of the underlying platform. Another approach is to incorporate dependence on these features indirectly, as in Zhang et al. [40] where security labels are associated with hardware states to track information flow dependencies throughout the hardware environment. This approach is compatible with our resourceaware noninterference type system, but is less flexible for the programmer as it is subject to the same types of imprecision present in information-flow type systems. We leave as future work developing more precise models that remain faithful to the resource-consumption subtleties of hardware platforms.
Another limitation of this work follows from the imprecision of the information-flow type system that is integrated with our constant-resource type system to verify resourceaware noninterference. It is well-known that such type systems are more conservative than the semantics of allowed noninterference [24], [25], [26], and this applies to our work as well. In particular, a variable conservatively identified as high-security could influence resource usage, leading our verifier to conclude that a program which is constantresource in practice is not. Our approach mitigates this issue since imprecise information-flow tracking does not directly lead to rejections of secure programs but only increases the burden on constant-resource analysis. Another potential mitigation that applies in some cases is to simply prove that the program is constant-resource with respect to all variables. Another approach that we leave to future work is to incorporate declassification mechanisms into our system.

IX. CONCLUSION
We have introduced new sub-structural type systems for automatically deriving lower bounds and proving constant resource usage. The evaluation with the implementation in RAML shows that the technique extends beyond the core language that we study in this paper and works for realistic example programs. We have shown how the new type systems can interact with information-flow type systems to prove resource-aware noninterference. Moreover, the type system for constant resource can be used to automatically remove side-channel vulnerabilities from programs.
There are many interesting connections between security and (automatic) quantitative resource analysis that we plan to study in the future. Two concrete projects that we already started are the integration of the type systems for upper and lower bounds with information-flow type systems to precisely quantify the resource-based information leakage at certain security levels. Another direction is to more precisely characterize the amount of information that can be obtained about secrets by making one particular resourceusage observation.

Typing rules
The full typing rules of the resource-aware security type system are presented in Fig. 14.

Proof of Lemma 2
The proof is done by induction on the structure of the typing derivation.
SR:B-OP: Suppose the evaluation derivation ends with an application of the rule E:BIN, thus E 1 (x 1 ) ⋄ E 1 (x 2 ) = v 1 and E 2 (x 1 ) ⋄ E 2 (x 2 ) = v 2 . The typing derivation ends with an application of the rules SR:B-OP or SR:GEN. We have k x1 ⊳ S and k x2 ⊳ S. If S ◭ k 1 then k x1 ⊑ k 1 and k x2 ⊑ k 1 . By the hypothesis, we have SR The typing derivation ends with an application of the following rules.
• Case SR:L-LET. If S 2 ◭ k 1 , by the simple security lemma, it holds that S 1 ◭ k 1 . By induction for e 1 , we  If S 1 * S 2 ◭ k, then by the simple security lemma we have S 1 ◭ k 1 and S 2 ◭ k 1 . Hence it follows v 1 = v 2 .
SR:MATCH-P: Suppose the evaluation derivation ends with an application of the rule E:MATCH-P, thus The typing derivation ends with an application of the following rules.
• Case SR:MATCH-P. If S ◭ k 1 , then by the simple security lemma we have S 1 * S 2 ◭ k 1 . By the hypothesis, The typing derivation ends with an application of the rules SR:CONS or SR:GEN. If (L(S), k x ) ◭ k 1 then by the hypothesis we have v 1 SR:MATCH-L: Suppose e is of the form match(x, e 1 , (x h , x t ).e 2 ), the evaluation derivation ends with an application of the rule E:MATCH-N or the rule E:MATCH-L. The typing derivation ends with an application of the following rules.  Figure 13. Guards, collecting, and subtyping relations • Case SR:MATCH-L. If S 1 ◭ k 1 , then by the simple security lemma we have (L(S), k x ) ◭ k 1 . By the hypothesis we have E 1 (x) = E 2 (x). Assume that , by induction for e 2 , it holds that v 1 = v 2 if S 1 ◭ k 1 . It is similar for E 1 (x) = E 2 (x) = nil . • Case SR:C-MATCH-L.It is similar to the case SR:MATCH-L.
• Case SR:GEN and SR:C-GEN. It follows. SR:SUBTYPING: Suppose the typing derivation ends with the rule SR:SUBTYPING. If S ′ ◭ k 1 then S ◭ k 1 . Thus by induction for e in the premise it follows. It is similar for SR:C-SUBTYPING.
Hence, E ′ 1 ≈ X∪{xt,x h } E ′ 2 , by induction for e 2 which is resource-aware noninterference w.r.t X ∪ {x t , x h }, we have p 1 − K matchL − p ′ 1 = p 2 − K matchL − p ′ 2 , thus p 1 − p ′ 1 = p 2 − p ′ 2 . If E 1 (x) = E 2 (x) = nil then by induction for e 1 that is resource-aware noninterference w.r.t X, it follows. If x ∈ X then E 1 (x) = E 2 (x), it is similar. • Case SR:C-GEN. By the case SR:C-GEN it follows. SR:SUBTYPING: The typing derivation ends with an application of either the rule SR:C-SHARE or SR:C-GEN.
• Case SR:C-SUBTYPING. By induction for e in the premise, p 1 − p ′ 1 = p 2 − p ′ 2 . • Case SR:C-GEN. By the case SR:C-GEN it follows.

RESOURCE
The common syntax-directed typing rules for all of three type systems; upper bounds, constant resource, and lower bounds are represented in Fig. 15. While the different structural rules are shown in Fig. 16, Fig. 17, and Fig. 18. We can see that the relax rules are consistent among these type systems in sense of satisfying the following.
That means the constraints for upper bounds and lower bounds imply the constraints for constant resource and vice versa.
The type systems for upper bounds, constant resource, and lower bounds are affine, linear, and relevant sub-structural type systems, respectively.
• Type system for upper bounds allows exchange and weakening, but not contraction properties. • Type system for constant resource allows exchange but not weakening or contraction properties. • Type system for lower bounds allows exchange and contraction, but not weakening properties.

Proof of Theorem 2
The proof is done by induction on the length of the derivation of the evaluation judgement and the typing judgement with lexical order, in which the derivation of the evaluation judgement takes priority over the typing derivation. We need to do induction on the length of both evaluation and typing derivations since on one hand, an induction of only typing derivation would fail for the case of function application, which increases the length of the typing derivation, while the length of the evaluation derivation never increases. On the other hand, if the rule C:WEAKENING is the final step in the derivation, then the length of typing derivation decreases, while the length of evaluation derivation is unchanged.
A:SHARE: Assume that the typing derivation ends with an application of the rule A:SHARE, thus Σ r ; Γ r , x 1 : A 1 , x 2 : A 2 q q ′ e : B and (A|A 1 , A 2 ).
Since |= E : Γ r , x : A and following the property of the share relation we have |= E 1 : Γ r , x 1 : A 1 , x 2 : A 2 . By the induction hypothesis for e, it holds that for all p, r ∈ Q + 0 such that p = q + Φ E1 (Γ r , x 1 : A 1 , x 2 : A 2 ) + r, there exists p ′ ∈ Q + 0 satisfying E 1 p p ′ e ⇓ v and p ′ = q ′ +Φ(v : B)+r.
Since |= E : Γ r , x : A, it follows |= E : Γ r . By the induction hypothesis for e, it holds that for all p, r ∈ Q + 0 such that p = q+Φ E (Γ r )+r, there exists p ′ ∈ Q + 0 satisfying E p p ′ e ⇓ v and p ′ = q ′ + Φ(v : B) + r. By the property of the share relation, Φ(a : A) = 0, then we have p = q + Φ E (Γ r , x : A) + r, E p p ′ e ⇓ v and p ′ = q ′ + Φ(v : B) + r as required.