Differentially private mechanisms enjoy a variety of composition properties. Leveraging these, McSherry introduced PINQ (SIGMOD 2009), a system empowering non-experts to construct new differentially private analyses. PINQ is an LINQ-like API which provides automatic privacy guarantees for all programs which use it to mediate sensitive data manipulation. In this work we introduce featherweight PINQ, a formal model capturing the essence of PINQ. We prove that any program interacting with featherweight PINQ's API is differentially private.

Differential privacy enjoys increasing popularity thanks to both a precise semantics for privacy and effective enforcement mechanisms. Many tools have been proposed to spread its use and ease the task of the concerned data scientist. The most promising among them completely discharge the user of the privacy concerns by transparently taking care of the privacy budget. However, their implementation proves to be delicate, and introduce flaws by falsifying some of the theoretical assumptions made to guarantee differential privacy. Moreover, such tools rely on assumptions leading to over-approximations which artificially reduce utility. In this paper we focus on a key mechanism that tools do not support well: sampling. We demonstrate an attack on PINQ (McSherry, SIGMOD 2009), one of these tools, relying on the difference between its internal mechanics and the formal theory for the sampling operation, and study a range of sampling methods and show how they can be correctly implemented in a system for differential privacy.

Environmental noise (e.g. heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance - a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high deployment cost - special hardware might be required to implement it - and provides weak statistical guarantees. It is also based on the assumption that faults are rare. In this paper we consider scenarios where security, rather than functional correctness, is the main asset to be protected. Our contribution is twofold. Firstly, we develop a theory for expressing confidentiality of data in the presence of transient faults. We show that the natural probabilistic definition of security in the presence of faults can be captured by a possibilistic definition. Furthermore, the possibilistic definition is implied by a known bisimulation-based property, called Strong Security. Secondly, we illustrate the utility of these results for a simple RISC architecture for which only the code memory and program counter are assumed fault-tolerant. We present a type-directed compilation scheme that produces RISC code from a higher-level language for which Strong Security holds - i.e. well-typed programs compile to RISC code which is secure despite transient faults. In contrast with fault-tolerance solutions, our technique assumes relatively little special hardware, gives formal guarantees, and works in the presence of an active attacker who aggressively targets parts of a system and induces faults precisely.

Information flow policies are often dynamic, the security concerns of a program will typically change during execution to reflect security-relevant events. A key challenge is how to best specify, and give proper meaning to, such dynamic policies. A large number of approaches exist that tackle that challenge, each yielding some important, but unconnected, insight. In this work we synthesise existing knowledge on dynamic policies, with an aim to establish a common terminology, best practices, and frameworks for reasoning about them. We introduce the concept of facets to illuminate subtleties in the semantics of policies, and closely examine the anatomy of policies and the expressiveness of policy specification mechanisms. We further explore the relation between dynamic policies and the concept of declassification.

Security policies are naturally dynamic. Reflecting this, there has been a growing interest in studying information-flow properties which change during program execution, including concepts such as declassification, revocation, and role-change. A static verification of a dynamic information flow policy, from a semantic perspective, should only need to concern itself with two things: 1 the dependencies between data in a program, and 2 whether those dependencies are consistent with the intended flow policies as they change over time. In this paper we provide a formal ground for this intuition. We present a straightforward extension to the principal flow-sensitive type system introduced by Hunt and Sands POPL'06, ESOP'11 to infer both end-to-end dependencies and dependencies at intermediate points in a program. This allows typings to be applied to verification of both static and dynamic policies. Our extension preserves the principal type system's distinguishing feature, that type inference is independent of the policy to be enforced: a single, generic dependency analysis typing can be used to verify many different dynamic policies of a given program, thus achieving a clean separation between 1 and 2. We also make contributions to the foundations of dynamic information flow. Arguably, the most compelling semantic definitions for dynamic security conditions in the literature are phrased in the so-called knowledge-based style. We contribute a new definition of knowledge-based progress insensitive security for dynamic policies. We show that the new definition avoids anomalies of previous definitions and enjoys a simple and useful characterisation as a two-run style property.

Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge. Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction. This paper is about a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy (PDP). In PDP each individual has its own personal privacy level. We describe ProPer, a interactive system for implementing PDP which maintains a privacy budget for each individual. When a primitive query is made on data derived from individuals, the provenance of the involved records determines how the privacy budget of an individual is affected: the number of records derived from Alice determines the multiplier for the privacy decrease in Alice's budget. This offers some advantages over previous systems, in particular its fine-grained character allows better utilisation of the privacy budget than mechanisms based purely on the concept of global sensitivity, and it applies naturally to the case of a live database where new individuals are added over time. We provide a formal model of the ProPer approach, prove that it provides personalised differential privacy, and describe a prototype implementation based on McSherry's PINQ system.

This tutorial provides an introduction to Paragon, a programming language that allows specification of security concerns on the data that is manipulated, as an integral part of the code. The target audience are programmers, as the end users of the programming language. The goal of the tutorial is to learn how to write information-flow secure programs in Paragon, without prior knowledge of theories, enforcement mechanisms and meta-properties underlying the field of information flow research.

This paper is about ensuring security in unreliable systems. We study systems which are subject to transient faults -– soft errors that cause stored values to be corrupted. The classic problem of fault tolerance is to modify a system so that it works despite a limited number of faults. We introduce a novel variant of this problem. Instead of demanding that the system works despite faults, we simply require that it remains secure: wrong answers may be given but secrets will not be revealed. We develop a software-based technique to achieve this fault- tolerant non-interference property. The method is defined on a simple assembly language, and guarantees security for any assembly program provided as input. The security property is defined on top of a formal model that encompasses both the fault-prone machine and the faulty environment. A precise characterization of the class of programs for which the method guarantees transparency is provided.

Conventional security policies for software applications are adequate for managing concerns on the level of access control. But standard abstraction mechanisms of mainstream programming languages are not sufficient to express how information is allowed to flow between resources once access to them has been obtained. In practice we believe that such control - information flow control - is needed to manage the end-to-end security properties of applications. In this paper we present Paragon, a Java-based language with first-class support for static checking of information flow control policies. Paragon policies are spec- ified in a logic-based policy language. By virtue of their explicitly stateful nature, these policies appear to be more expressive and flexible than those used in previous languages with information-flow support. Our contribution is to present the design and implementation of Paragon, which smoothly integrates the policy language with Java’s object-oriented setting, and reaps the benefits of the marriage with a fully fledged programming language.

Broberg and Sands (POPL'10) introduced a logic-based policy language, Paralocks, suitable for static information-flow control in programs. Although Paralocks comes with a precise information-flow semantics for programs, the logic-based semantics of policies, describing how policies are combined and compared, is less well developed. This makes the algorithms for policy comparison and computation ad-hoc, and their security guarantees less intuitive. In this paper we provide a new semantics for Paralocks policies based on Datalog. By doing so we are able to show that the ad-hoc semantics from earlier work coincides with the natural Datalog interpretation. Furthermore we show that by having a Datalog-inspired semantics, we can borrow language extensions and algorithms from Datalog for the benefit of Paralocks. We explore how these extensions and algorithms interact with the design and implementation of Paragon, a language combining Paralocks with Java.

Security or privacy-critical applications often require access to sensitive information in order to function. But in accordance with the principle of least privilege -– or perhaps simply for legal compliance -– such applications should not retain said information once it has served its purpose. In such scenarios, the timely disposal of data is known as an information erasure policy. This paper studies software-level information erasure policies for the data manipulated by programs. The paper presents a new approach to the enforcement of such policies. We adapt ideas from dynamic taint analysis to track how sensitive data sources propagate through a program and erase them on demand. The method is implemented for Python as a library, with no modifications to the runtime system. The library is easy to use, and allows programmers to indicate information-erasure policies with only minor modifications to their code.

We consider the problem of logical data erasure, contrasting with physical erasure in the same way that end-to-end information flow control contrasts with access control. We present a semantic hierarchy for erasure policies, using a possibilistic knowledge-based semantics to define policy satisfaction such that there is an intuitively clear upper bound on what information an erasure policy permits to be retained. Our hierarchy allows a rich class of erasure policies to be expressed, taking account of the power of the attacker, how much information may be retained, and under what conditions it may be retained. While our main aim is to specify erasure policies, the semantic framework allows quite general information-flow policies to be formulated for a variety of semantic notions of secrecy.

The idea of building secure systems by plugging together “secure” components is appealing, but this requires a definition of security which, in addition to taking care of top-level security goals, is strengthened appropriately in order to be compositional. This approach has been previously studied for information-flow security of shared-variable concurrent programs, but the price for compositionality is very high: a thread must be extremely pessimistic about what an environment might do with shared resources. This pessimism leads to many intuitively secure threads being labelled as insecure. Since in practice it is only meaningful to compose threads which follow an agreed protocol for data access, we take advantage of this to develop a more liberal compositional security condition. The idea is to give the security definition access to the intended pattern of data usage, as expressed by assumption-guarantee style conditions associated with each thread. We illustrate the improved precision by developing the first flow-sensitive security type system that provably enforces a noninterference-like property for concurrent programs.

Hunt and Sands (POPL'06) studied a flow sensitive type (FST) system for multi-level security, parametric in the choice of lattice of security levels. Choosing the powerset of program variables as the security lattice yields a system which was shown to be equivalent to Amtoft and Banerjee's Hoare-style independence logic (SAS'04). Moreover, using the powerset lattice, it was shown how to derive a principal type from which all other types (for all choices of lattice) can be simply derived. Both of these earlier works gave "algorithmic" formulations of the type system/program logic, but both algorithms are of exponential complexity due to the iterative typing of While loops. Later work by Hunt and Sands (ESOP'08) adapted the FST system to provide an erasure type system which determines whether some input is correctly erased at a designated time. This type system is inherently exponential, requiring a double typing of the erasure-labelled input command. In this paper we start by developing the FST work in two key ways: (1) We specialise the FST system to a form which only derives principal types; the resulting type system has a simple algorithmic reading, yielding principal security types in polynomial time. (2) We show how the FST system can be simply extended to check for various degrees of termination sensitivity (the original FST system is completely termination insensitive, while the erasure type system is fully termination sensitive).We go on to demonstrate the power of these techniques by combining them to develop a type system which is shown to correctly implement erasure typing in polynomial time. Principality is used in an essential way to reduce type derivation size from exponential to linear.

Security or privacy-critical applications often require access to sensitive information in order to function. But in accordance with the principle of least privilege - or perhaps simply for legal compliance - such applications should not retain said information once it has served its purpose. In such scenarios, the timely disposal of data is known as an information erasure policy. This paper studies software-level information erasure policies for the data manipulated by programs. The paper presents a new approach to the enforcement of such policies. We adapt ideas from dynamic taint analysis to track how sensitive data sources propagate through a program and erase them on demand. The method is implemented for Python as a library, with no modifications to the runtime system. The library is easy to use, and allows programmers to indicate information-erasure policies with only minor modifications to their code.

Phung et al (ASIACCS'09) describe a method for wrapping built-in methods of JavaScript programs in order to enforce security policies. The method is appealing because it requires neither deep transformation of the code nor browser modification. Unfortunately the implementation outlined suffers from a range of vulnerabilities, and policy construction is restrictive and error prone. In this paper we address these issues to provide a systematic way to avoid the identified vulnerabilities, and make it easier for the policy writer to construct declarative policies - i.e. policies upon which attacker code has no side effects.

This paper presents Paralocks, a language for building expressive but statically verifiable fine-grained information flow policies. Paralocks combine the expressive power of Flow Locks (Broberg & Sands, ESOP'06) with the ability to express policies involving run-time principles, roles (in the style of role-based access control), and relations (such as “acts-for” in discretionary access control). We illustrate the Paralocks policy language by giving a simple encoding of Myers and Liskov's Decentralized Label Model (DLM). Furthermore - and unlike the DLM - we provide an information flow semantics for full Paralock policies. Lastly we illustrate how Paralocks can be statically verified by providing a simple programming language incorporating Paralock policy specifications, and a static type system which soundly enforces information flow security according to the Paralock semantics.

Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems - in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a program intentionally makes a tradeoff between security and efficiency and leaks some information through a side channel? In this paper we study such tradeoffs using ideas from recent research on declassification. We present a semantic model of security for programs which allow for declassification through side channels, and show how side-channel declassification can be verified using off-the-shelf software model checking tools. Finally, to make it simpler for verifiers to check that a program conforms to a particular side-channel declassification policy we introduce a further tradeoff between efficiency and verifiability: by writing programs in a particular “manifest form” security becomes considerably easier to verify.

Dynamic information flow policies, such as declassification, are essential for practically useful information flow control systems. However, most systems proposed to date that handle dynamic information flow policies suffer from a common drawback. They build on semantic models of security which are inherently flow insensitive, which means that many simple intuitively secure programs will be considered insecure.

In this paper we address this problem in the context of a particular system, flow locks. We provide a new flow sensitive semantics for flow locks based on a knowledge-style definition (following Askarov and Sabelfeld), in which the knowledge gained by an actor observing a program run is constrained according to the flow locks which are open at the time each observation is made. We demonstrate the applicability of the definition in a soundness proof for a simple flow lock type system. We also show how other systems can be encoded using flow locks, as an easy means to provide these systems with flow sensitive semantics.

This paper introduces a method to control JavaScript execution. The aim is to prevent or modify inappropriate behaviour caused by e.g. malicious injected scripts or poorly designed third-party code. The approach is based on modifying the code so as to make it self-protecting: the protection mechanism (security policy) is embedded into the code itself and intercepts security relevant API calls. The challenges come from the nature of the JavaScript language: any variables in the scope of the program can be redefined, and code can be created and run on-the-fly. This creates potential problems, respectively, for tamper-proofing the protection mechanism, and for ensuring that no security relevant events bypass the protection. Unlike previous approaches to instrument and monitor JavaScript to enforce or adjust behaviour, the solution we propose is lightweight in that (i) it does not require a modified browser, and (ii) it does not require any run-time parsing and transformation of code (including dynamically generated code). As a result, the method has low run-time overhead compared to other methods satisfying (i), and the lack of need for browser modifications means that the policy can even be applied on the server to mitigate some effects of cross-site scripting bugs.

Hunt and Sands (ESOP'08) studied a notion of information erasure for systems which receive secrets intended for limited-time use. Erasure demands that once a secret has fulfilled its purpose the subsequent behaviour of the system should reveal no information about the erased data. In this paper we address a shortcoming in that work: for erasure to be possible the user who provides data must also play his part, but previously that role was only specified informally. Here we provide a formal model of the user and a collection of requirements called erasure friendliness. We prove that an erasure-friendly user can be composed with an erasing system (in the sense of Hunt and Sands) to obtain a combined system which is jointly erasing in an appropriate sense. In doing so we identify stronger requirements on the user than those informally described in the previous work.

Tools for analysing secure information flow are almost exclusively based on ideas going back to Denning's work from the 70's. This approach embodies an imperfect notion of security which turns a blind eye to information flows which are encoded in the termination behaviour of a program. In exchange for this weakness many more programs are deemed “secure”, using conditions which are easy to check. Previously it was thought that such leaks are limited to at most one bit per run. Recent work by Askarov et al (ESORICS'08) offers some bad news and some good news: the bad news is that for programs which perform output, the amount of information leaked by a Denning style analysis is not bounded; the good news is that if secrets are chosen to be sufficiently large and sufficiently random then they cannot be effectively leaked at all. The problem addressed in this paper is that secrets cannot always be made sufficiently large or sufficiently random. Contrast, for example, an encryption key with an “hasHIV”-field of a patient record. In recognition of this we develop a notion of secret-sensitive noninterference in which “small” secrets are handled more carefully than “big” ones. We illustrate the idea with a type system which combines a liberal Denning-style analysis with a more restrictive system according to the nature of the secrets at hand.

Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended? While the security community has recognised the importance of the problem, the state-of-the-art in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released and when information can be released. With a general declassification framework as a long-term goal, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful “sanity checks" for emerging models.

Current tools for analysing information flow in programs build upon ideas going back to Denning's work from the 70's. These systems enforce an imperfect notion of information flow which has become known as termination-insensitive noninterference. Under this version of noninterference, information leaks are permitted if they are transmitted purely by the program's termination behaviour (i.e., whether it terminates or not). This imperfection is the price to pay for having a security condition which is relatively liberal (e.g. allowing while-loops whose termination may depend on the value of a secret) and easy to check. But what is the price exactly? We argue that, in the presence of output, the price is higher than the “one bit” often claimed informally in the literature, and effectively such programs can leak all of their secrets. In this paper we develop a definition of termination-insensitive noninterference suitable for reasoning about programs with outputs. We show that the definition generalises “batch-job” style definitions from the literature and that it is indeed satisfied by a Denning-style program analysis with output. Although more than a bit of information can be leaked by programs satisfying this condition, we show that the best an attacker can do is a brute-force attack, which means that the attacker cannot reliably (in a technical sense) learn the secret in polynomial time in the size of the secret. If we further assume that secrets are uniformly distributed, we show that the advantage the attacker gains when guessing the secret after observing a polynomial amount of output is negligible in the size of the secret.

The lifecycle mismatch between vehicles and their IT system poses a problem for the automotive industry. Such systems need to be open and extensible to provide customised functionalities and services. What is less clear is how to achieve this with quality and security guarantees. Recent studies in language-based security - the use of programming language technology to enforce application specific security policies - show that security policy enforcement mechanisms such as inlined reference monitors provide a potential solution for security in extensible systems. In this paper we study the implementation of security policy enforcement using aspect-oriented programming for the OSGi (Open Services Gateway initiative) framework. We identify classes of reference monitor-style policies that can be defined and enforced using AspectJ, a well-known aspect-oriented programming language. We demonstrate the use of security states to describe history-based policies. We also introduce and implement various levels of security states in Java to describe session level history versus global application level history. We illustrate the effectiveness of the implementation by deploying the security policy enforcement solution in an example scenario of software downloading in a standard vehicle system.

There are many settings in which sensitive information is made available to a system or organisation for a specific purpose, on the understanding that it will be erased once that purpose has been fulfilled. A familiar example is that of online credit card transactions: a customer typically provides credit card details to a payment system on the understanding that the following promises are kept: (i) Noninterference (NI): the card details may flow to the bank (in order that the payment can be authorised) but not merchant; to other users of the system; (ii) Erasure: the payment system will not retain any record of the card details once the transaction is complete. This example shows that we need to reason about NI and erasure in combination, and that we need to consider interactive systems: the card details are used in the interaction between the principals, and then erased; without the interaction, the card details could be dispensed with altogether and erasure would be unnecessary. The contributions of this paper are as follows. (i) We show that an end-to-end erasure property can be encoded as a “flow sensitive” noninterference property. (ii) By a judicious choice of language construct to support erasure policies, we successfully adapt this result to an interactive setting. (iii) We use this result to design a type system which guarantees that well typed programs are properly erasing. Although erasure policies have been discussed in earlier papers, this appears to be the first static analysis to enforce erasure.

A common theoretical assumption in the study of information flow security in Java-like languages is that pointers are opaque - i.e., that the only properties that can be observed of pointers are the objects to which they point, and (at most) their equality. These assumptions often fail in practice. For example, various important operations in Java's standard API, such as hashcodes or serialization, might break pointer opacity. As a result, information-flow static analyses which assume pointer opacity risk being unsound in practice, since the pointer representation provides an unchecked implicit leak. We investigate information flow in the presence of non-opaque pointers for an imperative language with records, pointer instructions and exceptions, and develop an information flow aware type system which guarantees noninterference.

This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice. By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it provides a principal typing from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04). In general, some lattices are more expressive than others. Despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself. Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.

Security is rarely a static notion. What is considered to be confidential or untrusted data varies over time according to changing events and states. The static verification of secure information flow has been a popular theme in recent programming language research, but information flow policies considered are based on multilevel security which presents a static view of security levels. In this paper we introduce a very simple mechanism for specifying dynamic information flow policies, flow locks, which specify conditions under which data may be read by a certain actor. The interface between the policy and the code is via instructions which open and close flow locks. We present a type and effect system for an ML-like language with references which permits the completely static verification of flow lock policies, and prove that the system satisfies a semantic security property generalising noninterference. We show that this simple mechanism can represent a number of recently proposed information flow paradigms for declassification.

Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended? While the security community has recognised the importance of the problem, the state-of-the-art in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released and when information can be released. With a general declassification framework as a long-term goal, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful “sanity checks” for emerging models.

Common protection mechanisms fail to provide end-to-end security; programs with legitimate access to secret information are not prevented from leaking this to the world. Information-flow aware analyses track the flow of information through the program to prevent such leakages, but often ignore information flows through covert channels even though they pose a serious threat. A typical covert channel is to use the timing of certain events to carry information. We present a timing-aware information-flow type system for a low-level language similar to a non-trivial subset of a sequential Java bytecode. The type system is parameterized over the time model of the instructions of the language and over the algorithm enforcing low-observational equivalence, used in the prevention of implicit and timing flows.

Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feasible, these approaches suffer from the need for abstraction and the high cost of building dedicated tools for real programming languages. We recast the information flow problem in a general program logic rather than a problem-specific one. We investigate the feasibility of this approach by showing how a general purpose tool for software verification can be used to perform information flow analyses. We are able to prove security and insecurity of programs including advanced features such as method calls, loops, and object types for the target language Java Card. In addition, we can express declassification of information

Traditional noninterference cannot cope with common features of secure systems like channel control, information filtering, or explicit downgrading. Recent research has addressed the derivation and use of weaker security conditions that could support such features in a language-based setting. However, a fully satisfactory solution to the problem has yet to be found. A key problem is to permit exceptions to a given security policy without permitting too much. In this article, we propose an approach that draws its underlying ideas from intransitive noninterference, a concept usually used on a more abstract specification level. Our results include a new bisimulation-based security condition that controls tightly where downgrading can occur and a sound security type system for checking this condition.

The notion of a context is widely used in programming language semantics - for example in the definition of operational equivalences, or program transformation, and in certain styles of operational semantics definitions. This tutorial describes how the use of a higher-order syntax representation of contexts combines smoothly with higher-order syntax for evaluation rules, so that definitions can be extended to work over contexts. This provides "for free" - without the development of any new language-specific context calculi - evaluation rules for contexts which commute with hole-filling. We have found this to be a useful technique for directly reasoning about operational equivalence. Some illustrations of the utility of this technique will be given.

The powerful abstraction mechanisms of functional programming languages provide the means to develop domain-specific programming languages within the language itself. Typically, this is realised by designing a set of combinators (higher-order reusable programs) for an application area, and by constructing individual applications by combining and coordinating individual combinators. This paper is concerned with a successful example of such an embedded programming language, namely Fudgets, a library of combinators for building graphical user interfaces in the lazy functional language Haskell. The Fudget library has been used to build a number of substantial applications, including a web browser and a proof editor interface to a proof checker for constructive type theory. This paper develops a semantic theory for the non-deterministic stream processors that are at the heart of the Fudget concept. The interaction of two features of stream processors makes the development of such a semantic theory problematic: (i) the sharing of computation provided by the lazy evaluation mechanism of the underlying host language, and (ii) the addition of non-deterministic choice needed to handle the natural concurrency that reactive applications entail. We demonstrate that this combination of features in a higher-order functional language can be tamed to provide a tractable semantics theory and induction principles suitable for reasoning about contextual equivalence of Fudgets.

The equational theories at the core of most functional programming are variations on the standard lambda calculus. The best known of these is the call-by-value lambda calculus whose core is the value-beta computation rule. This paper investigates the transformational power of this core theory of functional programming. The main result is that the equational theory of the call-by-value lambda calculus cannot speed up (or slow down) programs by more than a constant factor. The corresponding result also holds for call-by-need but we show that it does not hold for call-byname: there are programs for which a single beta reduction can change the program's asymptotic complexity.

Innocent-looking program transformations can easily change the space complexity of lazy functional programs. The theory of space improvement seeks to characterise those local program transformations which are guaranteed never to worsen asymptotic space complexity of any program. Previous work by the authors introduced the space improvement relation and showed that a number of simple local transformation laws are indeed space improvements. This paper seeks an answer to the following questions: is the improvement relation inhabited by interesting program transformations, and, if so, how might they be established? We show that the asymptotic space improvement relation is semantically badly behaved, but that the theory of strong space improvement possesses a fixed-point induction theorem which permits the derivation of improvement properties for recursive definitions. With the help of this tool we explore the landscape of space improvement by considering a range of classical program transformations.

Recent interest in methods for certifying programs for secure information flow (noninterference) have failed to raise a key question: can efficient algorithms be written so as to satisfy the requirements of secure information flow? In this paper we discuss how algorithms for searching and sorting can be adapted to work on collections of secret data without leaking any confidential information, either directly, indirectly, or through timing behaviour. We pay particular attention to the issue of timing channels caused by cache behaviour, and argue that it is necessary to disable the effect of the cache in order to construct algorithms manipulating pointers to objects in such a way that they satisfy the conditions of noninterference.

This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature, and connections to other forms of program analysis. The approach is inspired by (and equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and “partially confidential data”. We extend the approach to handle nondeterminism by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics.

Keywords: computer programming - congresses; programming languages (electronic computers) - congresses

A program which has access to your sensitive data presents a security threat. Does the program keep your secrets secret? To answer the question one must specify what it means for a program to be secure, and one may wish to verify the security specification before executing the program. We present a probability-sensitive security specification (probabilistic noninterference) for multi-threaded programs based on a probabilistic bisimulation. Some previous approaches to specifying confidentiality rely on a particular scheduler for executing program threads. This is unfortunate since scheduling policy is typically outside the language specification for multi-threaded languages. We describe how to generalise noninterference in order to define robust security with respect to any particular scheduler used and show, for a simple imperative language with dynamic thread creation, how the security condition satisfies compositionality properties which facilitates a straightforward proof of correctness of e.g. security type systems.

We introduce a space-improvement relation on programs which guarantees that whenever M is improved by N, replacement of M by N in a program can never lead to asymptotically worse space (heap or stack) behaviour, for a particular model of garbage collection. This study takes place in the context of a call-by-need programming language. For languages implemented using call-by-need, e.g, Haskell, space behaviour is notoriously difficult to predict and analyse, and even innocent-looking equivalences like x + y = y + x can change the asymptotic space requirements of some programs. Despite this, we establish a fairly rich collection of improvement laws, with the help of a context lemma for a finer-grained improvement relation. We briefly consider an application of the theory; we prove that inlining of affine-linear bindings (as introduced by a certain class of “used-once” type-systems) is work- and space-safe. We also show that certain weaker type systems for usage do not provide sufficient conditions for space-safe inlining.

Pure functional programming languages have been proposed as a vehicle to describe, simulate and manipulate circuit specifications. We propose an extension to Haskell to solve a standard problem when manipulating data types representing circuits in a lazy functional language. The problem is that circuits are finite graphs - but viewing them as an algebraic (lazy) datatype makes them indistinguishable from potentially infinite regular trees. However, implementations of Haskell do indeed represent cyclic structures by graphs. The problem is that the sharing of nodes that creates such cycles is not observable by any function which traverses such a structure. In this paper we propose an extension to call-by-need languages which makes graph sharing observable. The extension is based on non updatable reference cells and an equality test (sharing detection) on this type. We show that this simple and practical extension has well-behaved semantic properties, which means that many typical source-to-source program transformations, such as might be performed by a compiler, are still valid in the presence of this extension.

The standard implementation technique for lazy functional languages is call-by-need, which ensures that an argument to a function in any given call is evaluated at most once. A significant problem with call-by-need is that it is difficult - even for compiler writers - to predict the effects of program transformations. The traditional theories for lazy functional languages are based on call-by-name models, and offer no help in determining which transformations do indeed optimize a program.

In this article we present an operational theory for call-by-need, based upon an improvement ordering on programs: M is improved by N if in all program-contexts C, when C[M] terminates then C[N] terminates at least as cheaply.

We show that this improvement relation satisfies a "context lemma", and supports a rich inequational theory, subsuming the call-by-need lambda calculi of Ariola et al. The reduction-based call-by-need calculi are inadequate as a theory of lazy-program transformation since they only permit transformations which speed up programs by at most a constant factor (a claim we substantiate); we go beyond the various reduction-based calculi for call-by-need by providing powerful proof rules for recursion, including syntactic continuity - the basis of fixed-point-induction style reasoning, and an Improvement Theorem, suitable for arguing the safetey and correctness of recursion-based program transformations.

This article describes how the use of a higher-order syntax representation of contexts [due to A. Pitts] combines smoothly with higher-order syntax for evaluation rules, so that definitions can be extended to work over contexts. This provides "for free" - without the development of any new language-specific context calculi - evaluation rules for contexts which commute with hole-filling. We have found this to be a useful technique for directly reasoning about operational equivalence. A small illustration is given based on a unique fixed-point induction principle for a notion of guarded context in a functional language.

Gamma is a minimal language based on local multiset rewriting with an elegant chemical reaction metaphor. The virtues of this paradigm in terms of systematic program construction and design of parallel programs have been argued in previous papers. Gamma can also be seen as a notation for coordinating independent programs in a larger application. In this paper, we study a notion of refinement for programs involving parallel and sequential composition operators, and derive a number of programming laws. The calculus thus obtained is applied in the development of a generic "pipelining" transformation, which enables certain sequential compositions to be refined into parallel compositions.

An improvement theory is a variant of the standard theories of observational approximation (or equivalence) in which the basic observations made of a functional program's execution include some intensional information about, for example, the program's computational cost. One program is an improvement of another if its execution is more efficient in any program context. In this article we give an overview of our work on the theory and applications of improvement. Applications include reasoning about time properties of functional programs, and proving the correctness of program transformation methods. We also introduce a new application, in the form of some bisimulation-like proof techniques for equivalence, with something of the flavour of Sangiorgi's “bisimulation up-to expansion and context”.

Structural Operational Semantics (SOS) is a widely used formalism for specifying the computational meaning of programs, and is commonly used in specifying the semantics of functional languages. Despite this widespread use there has been relatively little work on the “metatheory” for such semantics. As a consequence the operational approach to reasoning is considered ad hoc since the same basic proof techniques and reasoning tools are reestablished over and over, once for each operational semantics specification. This paper develops some metatheory for a certain class of SOS language specifications for functional languages. We define a rule format, Globally Deterministic SOS (GDSOS), and establish some proof principles for reasoning about equivalence which are sound for all languages which can be expressed in this format. More specifically, if the SOS rules for the operators of a language conform to the syntax of the GDSOS format, then (i) a syntactic analogy of continuity holds, which relates a recursive function to its finite unwindings, and forms the basis of a Scott-style fixed-point induction technique; (ii) a powerful induction principle called improvement induction holds for a certain class of instrumented GDSOS semantics; (iii) a useful bisimulation-based coinductive proof technique for operational approximation (and its “instrumented” variants) is sound.

This paper shows how the Improvement Theorem-a semantic condition for establishing the total correctness of program transformation on higher-order functional programs-has practical value in proving the correctness of automatic techniques. To this end we develop and study a family of automatic program transformations. The root of this family is a well-known and widely studied transformation called deforestation; descendants include generalisations to richer input languages (e.g. higher-order functions), and more powerful transformations, including a source-level representation of some of the techniques known from Turchin's supercompiler.

Techniques for reasoning about extensional properties of functional programs are well-understood, but methods for analysing the underlying intensional, or operational properties have been much neglected. This paper begins with the development of a simple but useful calculus for time analysis of non-strict functional programs with lazy lists. One limitation of this basic calculus is that the ordinary equational reasoning on functional programs is not valid. In order to buy back some of these equational properties we develop a non-standard operational equivalence relation called cost equivalence, by considering the number of computation steps as an “observable” component of the evaluation process. We define this relation by analogy with Park's definition of bisimulation in ccs. This formulation allows us to show that cost equivalence is a contextual congruence (and thus is substitutive with respect to the basic calculus) and provides useful proof techniques for establishing cost-equivalence laws.

It is shown that basic evaluation time can be derived by demonstrating a certain form of cost equivalence, and we give a axiomatisation of cost equivalence which complete is with respect to this application. This shows that cost equivalence subsumes the basic calculus.

Finally we show how a new operational interpretation of evaluation demands can be used to provide a smooth interface between this time analysis and more compositional approaches, retaining the advantages of both.

Keywords: binding time, ideal model, partial evaluation, safety, topped domains, monovariance

Summary: We investigate the soundness of a specialisation technique due to Scherlis, expression procedures, in the context of a higher-order non-strict language. An expression procedure is a generalised procedure construct which provides a means of expressing contextual properties of functions, and thereby facilitates the manipulation and contextual specialisation of programs. Generalised programs provide a route to the correct specialisation of recursive functions, are transformed by means of three basic transformation rules: composition, application and abstraction. In this paper we show that the expression procedure approach is correct for call-by-name evaluation, including lazy data structures and higher order functions.

We consider operational semantics of contexts (terms with holes) in the setting of lazy functional languages, with the aim of providing a balance between operational and compositional reasoning, and a framework for semantics-based program analysis and manipulation.

The salient feature of the composition operators for Gamma programs is that for termination, the parallel composition operator demands that its operands must terminate synchronously. This paper studies the inequational partial correctness properties of the combination of sequential and parallel composition operators for Gamma programs, provable from a particular compositional semantics (Brookes-style transition traces) and shows that the “residual program” input-output laws originally described by Hankin et al. are also verified by the model.

We present a set of primitive program schemes, which together with just two basic combining forms provide a suprisingly expressive parallel programming language. The primitive program schemes (called tropes) take the form of parameterised conditional rewrite rules, and the computational model is a variant of the Gamma style, in which computation proceeds by nondeterministic local rewriting of a global multiset.

We consider a number of examples which illustrate the use of tropes and we study the algebraic properties of the sequential and parallel combining forms. Using the examples we illustrate the application of these properties in the verification of some simple program transformations.

Keywords: Parallel Programming Languages: Language Constructs, Semantics.

Given a description of the parameters in a program that will be known at partial evaluation time, a binding time analysis must determine which parts of the program are dependent solely on these known parts (and therefore also known at partial evaluation time). In this paper a binding time analysis for the simply typed lambda calculus is presented. The analysis takes the form of an abstract interpretation and uses a novel formalisation of the problem of binding time analysis, based on the use of partial equivalence relations. A simple proof of correctness is achieved by the use of logical relations.

In this paper we address the technical foundations essential to the aim of providing a semantic basis for the formal treatment of relative efficiency in functional languages. For a general class of “functional” computation systems, we define a family of improvement preorderings which express, in a variety of ways, when one expression is more efficient than another. The main results of this paper build on Howe's study of equality in lazy computation systems, and are concerned with the question of when a given improvement relation is subject to the usual forms of (in)equational reasoning (so that, for example, we can improve an expression by improving any sub-expression). For a general class of computation systems we establish conditions on the operators of the language which guarantee that an improvement relation is a precongruence. In addition, for a particular higher-order nonstrict functional language, we show that any improvement relation which satisfies a simple monotonicity condition with respect to the rules of the operational semantics has the desired congruence property.

Techniques for reasoning about extensional properties of functional programs are well-understood, but methods for analysing the underlying intensional, or operational properties have been much neglected. This thesis presents the development of several calculi for time analysis of functional programs.

We focus on two features, higher-order functions and lazy evaluation, which contribute much to the expressive power and semantic elegance of functional languages, but serve to make operational properties more opaque.

Analysing higher-order functions is problematic because complexity is dependent not only on the cost of computing, but also on the cost of applying function-valued expressions. Techniques for statically deriving programs which compute time-cost in the presence of arbitrary higher-order functions are developed. The key to this process is the introduction of syntactic structures called cost-closures, which enable intensional properties to be carried by functions. The approach is formalised by the construction of an appropriate cost-model, against which the correctness of the derivation is proved. A specific factorisation tactic for reasoning about higher-order functions out of context is illustrated.

Reasoning about lazy evaluation (ie call-by-name, or more usually, call-by-need) is problematic because the cost of evaluating an expression cannot be understood simply from the costs of its sub-expressions. A direct calculus for reasoning about a call-by-name language with lazy lists is derived from a simple operational model. In order to extend this calculus with a restricted form of equational reasoning, a nonstandard notion of operational approximation called cost-simulation is developed, by analogy with (bi)simulation in CCS.

The problem with calculi of the above form, based directly on an operational model, is that they do not yield a compositional description of cost, and cannot model lazy evaluation (graph-reduction) easily. We show how a description of the context in which a function is evaluated can be used to parameterise two types of time-equation: sufficient-time equations and necessary-time equations, which together provide bounds on the exact time-cost of lazy evaluation. This approach is extended to higher-order functions using a modification of the cost-closure technique.

This paper is concerned with the time-analysis of functional programs. Techniques which enable us to reason formally about a program's execution costs have had relatively little attention in the study of functional programming. We concentrate here on the construction of equations which compute the time-complexity of expressions in a lazy higher-order language.

The problem with higher-order functions is that complexity is dependent on the cost of applying functional parameters. Structures called cost-closures are introduced to allow us to model both functional parameters and the cost of their application.

The problem with laziness is that complexity is dependent on context.Projections are used to characterise the context in which an expression is evaluated, and cost-equations are parameterised by this context-description to give a compositional time-analysis. Using this form of context information we introduce two types of time-equation: sufficient-time equations and necessary-time equations, which together provide bounds on the exact time-complexity.

The aim of program transformation is to increase efficiency whilst preserving meaning. Techniques which enable us to reason formally about a program's execution costs are therefore potentially useful for assisting the program transformation process. This paper is concerned with the time-analysis of functional programs. We show how techniques for deriving equations which compute the time-complexity of a functional program can be extended to handle arbitrary higher-order functions. The derivation yields a functional program, is mechanisable, and thus forms the basis for an analysis tool for higher-order languages.