Order-Revealing Encryption (ORE) allows deriving the order of two plaintexts to facilitate database functions such as range queries and sorting. Ideally, nothing is observable to an adversary beyond the order of the messages. Unfortunately, Ideal ORE is challenging to implement, and a variation of it has then been developed. This variation, referred to as CLWW ORE, reveals the first differing bit position between every two plaintexts, in addition to the order.We provide a formal leakage analysis of these two ORE variations by applying the information-theoretic quantitative information flow (QIF) framework. We evaluate two threat models: (1) the Bayes scenario in which an adversary wishes to guess the secret entirely and (2) a bucketing scenario in which an adversary is content to simply guess the range of the plaintext. We provide security implications, usage guidelines, and a mitigation technique that improves the security of Ideal ORE. We find that while Ideal and CLWW ORE perform similarly under the Bayes scenario, CLWW ORE is fundamentally insecure under the bucketing scenario.

We investigate a problem in quantitative information flow, namely to find the maximum information leakage caused by n repeated independent runs of a channel C with b columns. While this scenario is of general interest, it is particularly motivated by the study of timing attacks on cryptography implemented using the countermeasures known as blinding and bucketing. We measure leakage in terms of multiplicative Bayes capacity (also known as min-capacity) and we prove tight bounds that greatly improve the previously-known ones. To enable efficient computation of our new bounds, we investigate them using techniques of analytic combinatorics, proving that they satisfy a useful recurrence and (when b = 2) a close connection to Ramanujan's Q-function.

Quantitative information flow aims to assess and control the leakage of sensitive information by computer systems. A key insight in this area is that no single leakage measure is appropriate in all operational scenarios, as a result, many leakage measures have been proposed, with many different properties. To clarify this complex situation, this paper studies information leakage axiomatically, showing important dependencies among different axioms. It also establishes a completeness result about the g-leakage family, showing that any leakage measure satisfying certain intuitively-reasonable properties can be expressed as a g-leakage.

A fundamental challenge in controlling the leakage of sensitive information by computer systems is the possibility of correlations between different secrets, with the result that leaking information about one secret may also leak information about a different secret. We explore such leakage, here called Dalenius leakage, within the context of the g-leakage family of leakage measures. We prove a fundamental equivalence between Dalenius min-entropy leakage under arbitrary correlations and g-leakage under arbitrary gain functions, and show how this equivalence increases the significance of the composition refinement relation. We also consider Dalenius leakage in the case when the marginal distributions induced by the correlation are known, giving techniques to compute stronger upper bounds in this case.

In computer security, it is frequently necessary in practice to accept some leakage of confidential information. This motivates the development of theories of Quantitative Information Flow aimed at showing that some leaks are "small" and therefore tolerable. We describe the fundamental view of channels as mappings from prior distributions on secrets to hyper-distributions, which are distributions on posterior distributions, and we show how g-leakage provides a rich family of operationally-significant measures of leakage. We also discuss two approaches to achieving robust judgments about leakage: notions of capacity and a robust leakage ordering called composition refinement.

A long-standing and fundamental issue in computer security is to control the flow of information, whether to prevent confidential information from being leaked, or to prevent trusted information from being tainted. While there have been many efforts aimed at preventing improper flows completely (see for example, the survey by Sabelfeld and Myers (2003)), it has long been recognized that perfection is often impossible in practice. A basic example is a login program – whenever it rejects an incorrect password, it unavoidably reveals that the secret password differs from the one that was entered. More subtly, systems may be vulnerable to side channel attacks, because observable characteristics like running time and power consumption may depend, at least partially, on sensitive information.

Protecting sensitive information from improper disclosure is a fundamental security goal. It is complicated, and difficult to achieve, often because of unavoidable or even unpredictable operating conditions that can lead to breaches in planned security defences. An attractive approach is to frame the goal as a quantitative problem, and then to design methods that measure system vulnerabilities in terms of the amount of information they leak. A consequence is that the precise operating conditions, and assumptions about prior knowledge, can play a crucial role in assessing the severity of any measured vunerability. We develop this theme by concentrating on vulnerability measures that are robust in the sense of allowing general leakage bounds to be placed on a program, bounds that apply whatever its operating conditions and whatever the prior knowledge might be. In particular we propose a theory of channel capacity, generalising the Shannon capacity of information theory, that can apply both to additive- and to multiplicative forms of a recently-proposed measure known as g-leakage. Further, we explore the computational aspects of calculating these (new) capacities: one of these scenarios can be solved efficiently by expressing it as a Kantorovich distance, but another turns out to be NP-complete. We also find capacity bounds for arbitrary correlations with data not directly accessed by the channel, as in the scenario of Dalenius's Desideratum.

This paper introduces g-leakage, a rich generalization of the min-entropy model of quantitative information flow. In g-leakage, the benefit that an adversary derives from a certain guess about a secret is specified using a gain function g. Gain functions allow a wide variety of operational scenarios to be modeled, including those where the adversary benefits from guessing a value close to the secret, guessing a part of the secret, guessing a property of the secret, or guessing the secret within some number of tries. We prove important properties of g-leakage, including bounds between min-capacity, g-capacity, and Shannon capacity. We also show a deep connection between a strong leakage ordering on two channels, C1and C2, and the possibility of factoring C1into C2C3, for some C3. Based on this connection, we propose a generalization of the Lattice of Information from deterministic to probabilistic channels.

In secure information flow analysis, the classic Denning restrictions allow a program's termination to be affected by the values of itsHvariables, resulting in potential information leaks. In an effort to quantify such leaks, in this paper we study a simple imperative language with random assignments. As a thought experiment, we propose a ‘stripping’ operation on programs, which eliminates all ‘high computation’, and prove the fundamental property that stripping cannot decrease the probability of any low outcome. To prove this property, we first introduce a new notion offast probabilistic simulationon Markov chains and show that it implies a key reachability property. Viewing the stripping function as a binary relation, we then prove that stripping is a fast simulation. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic non-interference property, provided that their probability of non-termination is small.

We establish formal bounds for the number of min-entropy bits that can be extracted in a timing attack against a cryptosystem that is protected by blinding, the state-of-the art countermeasure against timing attacks. Compared with existing bounds, our bounds are both tighter and of greater operational significance, in that they directly address the key’s one-guess vulnerability. Moreover, we show that any semantically secure public-key cryptosystem remains semantically secure in the presence of timing attacks, if the implementation is protected by blinding and bucketing. This result shows that, by considering (and justifying) more optimistic models of leakage than recent proposals for leakage-resilient cryptosystems, one can achieve provable resistance against side-channel attacks for standard cryptographic primitives.

With the variables of a program classified as L (low, public) or H (high, private), the secure information flow problem is concerned with preventing the program from leaking information from H variables to L variables. In the context of a multi-threa

To be practical, systems for ensuring secure information flow must be as permissive as possible. To this end, the author recently proposed a type system for multi-threaded programs running under a uniform probabilistic scheduler; it allows the running times of threads to depend on the values of H variables, provided that these timing variations cannot affect the values of L variables. But these timing variations preclude a proof of the soundness of the type system using the framework of probabilistic bisimulation, because probabilistic bisimulation is too strict regarding time. To address this difficulty, this paper proposes a notion of weak probabilistic bisimulation for Markov chains, allowing two Markov chains to be regarded as equivalent even when one "runs" more slowly that the other. The paper applies weak probabilistic bisimulation to prove that the type system guarantees the probabilistic noninterference property. Finally, the paper shows that the language can safely be extended with a fork command that allows new threads to be spawned.

With the variables of a program classified as L (low, public) or H (high, private), we wish to prevent the program from leaking information about H variables into L variables. Given a multi-threaded imperative language with probabilistic scheduling, the goal can be formalized as a property called probabilistic noninterference. Previous work identified a type system sufficient to guarantee probabilistic noninterference, but at the cost of severe restrictions: to prevent timing leaks, H variables were disallowed from the guards of while loops. Here we present a new type system that gives each command a type of the form τ1 cmd τ2; this type says that the command assigns only to variables of level τ1 (or higher) and has running time that depends only on variables of level τ2 (or lower). Also we use types of the form τ cmd n for commands that terminate in exactly n steps. With these typings, we can prevent timing leaks by demanding that no assignment to an L variable may sequentially follow a command whose running time depends on H variables. As a result, we can use H variables more flexibly; for example, under the new system a thread that involves only H variables is always well typed. The soundness of the type system is proved using the notion of probabilistic bisimulation. 1

Systems that authenticate a user based on a shared secret (such as a password or PIN) normally allow anyone to query whether the secret is a given value. For example, an ATM machine allows one to ask whether a string is the secret PIN of a (lost or stolen) ATM card. Yet such queries are prohibited in any model whose programs satisfy an information-flow property like Noninterference. But there is complexity-based justification for allowing these queries. A type system is given that provides the access control needed to prove that no well-typed program can leak secrets in polynomial time, or even leak them with nonnegligible probability if secrets are of sufficient length and randomly chosen. However, there are well-typed deterministic programs in a synchronous concurrent model capable of leaking secrets in linear time.

In previous work (Smith and Volpano, Proceedings 25th Symposium on Principles of Programming Languages, San Diego, CA, 1998, pp. 355–364), we give a type system that guarantees that well-typed multi-threaded programs are possibilistically noninterfer

The authors previously give a type system that guarantees that well-typed multi-threaded programs are possibilistically noninterfering. If thread scheduling is probabilistic, however, then well-typed programs may have probabilistic timing channels. They describe how they can be eliminated without making the type system more restrictive. They show that well-typed concurrent programs are probabilistically noninterfering if every total command with a high guard executes atomically. The proof uses the concept of a probabilistic state of a computation, following the work of Kozen (1981).

Previously, we developed a type system to ensure secure information flow in a sequential, imperative programming language [VSI96]. Program variables are classified as either high or low security; intuitively, we wish to prevent information from flowing from high variables to low variables. Here, we extend the analysis to deal with a multithreaded language. We show that the previous type system is insufficient to ensure a desirable security property called noninterference. Noninterference basically means that the final values of low variables are independent of the initial values of high variables. By modifying the sequential type system, we are able to guarantee noninterference for concurrent programs. Crucial to this result, however, is the use of purely nondeterministic thread scheduling. Since implementing such scheduling is problematic, we also show how a more restrictive type system can guarantee noninterference, given a more deterministic (and easily implementable) scheduling policy, such as round-robin time slicing. Finally, we consider the consequences of adding a clock to the language.

Advanced polymorphic type systems have come to play an important role in the world of functional programming. But, so far, these type systems have had little impact upon widely used imperative programming languages like C and C++. We show that ML-style polymorphism can be integrated smoothly into a dialect of C, which we call Polymorphic C. It has the same pointer operations as C, including the address-of operator &, the dereferencing operator ∗, and pointer arithmetic. We give a natural semantics for Polymorphic C, and prove a type soundness theorem that gives a rigorous and useful characterization of what can go wrong when a well-typed Polymorphic C program is executed. For example, a well-typed Polymorphic C program may fail to terminate, or it may abort due to a dangling pointer error. Proving such a type soundness theorem requires a notion of an attempted program execution; we show that a natural semantics gives rise quite naturally to a transition semantics, which we call a natural transition semantics, that models program execution in terms of transformations of partial derivation trees. This technique should be generally useful in proving type soundness theorems for languages defined using natural semantics.

A type system is given that eliminates two kinds of covert flows in an imperative programming language. The first kind arises from nontermination and the other from partial operations that can raise exceptions. The key idea is to limit the source of nontermination in the language to constructs with minimum typings, and to evaluate partial operations within expressions of try commands which also have minimum typings. A mutual progress theorem is proved that basically states that no two executions of a well-typed program can be distinguished on the basis of nontermination versus abnormal termination due to a partial operation. The proof uses a new style of programming language semantics which we call a natural transition semantics. 1. Introduction In [9], we gave a type system for secure information flow in a core imperative language. The type system is composed of a set of types and typing rules for deducing the types of expressions and commands. Types correspond to partially-ordered s...

Ensuring secure information flow within programs in the context of multiple sensitivity levels has been widely studied. Especially noteworthy is Denning's work in secure flow analysis and the lattice model [6,7]. Until now, however, the soundness of

In this article we consider the polymorphic type checking of an imperative language. Our language contains variables , first-class references (pointers), and first-class functions. Variables, as in traditional imperative languages, are implicitly dereferenced, and their addresses ( L -values) are not first-class values. Variables are easier to type check than references and, in many cases, lead to more general polymorphic types. We present a polymorphic type system for our language and prove that it is sound. Programs that use variables sometimes require weak types, as in Tofte's type system for Standard ML, but such weak types arise far less frequently with variables than with references