Interference and dependence are closely related concepts: interference being the observable phenomenon connected with dependence. Essentially, interference means that the behaviour of some parts of a dynamic system may influence the behaviour of other parts of the same system, while dependence specifies how the semantics of sub-components of a dynamic system are related. Identifying, measuring and controlling interference is essential in many aspects of modern computer science, in particular, in security, program analysis and verification, debugging, systems specification, model checking, program manipulation, program slicing, reverse engineering, data mining, distributed databases and systems biology. In all these fields, dependency and interference play a key role in designing suitable abstractions or in partitioning complex systems into simpler ones. Reasoning about dependency and interference requires theories, models and semantics, as well as algorithms and tools for their analysis. Beginning in 2004, the series of Programming Language Interference and Dependence (PLID) workshops has been devoted to promoting and spreading cutting-edge research in this field, with a particular emphasis on unpublished results with great impact on the theoretical basis. PLID2007, which was held at the The Technical University of Denmark on 21 August 2007, was particularly successful, and constituted the ideal forum for announcing a call for papers for a special journal issue on programming language interference and dependence, which would not necessarily be restricted to PLID2007 contributions. From the many expressions of interest, we selected six contributions by leading researchers in the field, some of which had been presented at the PLID2007 workshop. The selected papers focus on foundational aspects of dependency and interference, with applications in language-based security, data-base management systems and program slicing.

With the emergence of the new possibilities offered by global computing, new security issues follow from the fact that these possibilities can be equally exploited by parties with malicious intentions. Many attacks arise at the application level, and can be tackled by means of programming language techniques. For instance, confidentiality can be violated during the execution of programs that reveal secret information. This kind of program behaviour can be avoided by information flow analyses that detect the encoding of illegal flows.

This paper studies information flows that occur in distributed programs with code mobility from a language-based security perspective. New forms of security leaks that are introduced by code mobility, which we call migration leaks, are presented and compared with well-known forms of illegal flow. We propose an information flow property that is adequate for networks consisting of a generalisation of the non-disclosure policy. We design a type and effect system for enforcing it on an expressive distributed calculus, and explain a soundness proof methodology in detail.

In secure information flow analysis, the classic Denning restrictions allow a program's termination to be affected by the values of its H variables, 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 of fast probabilistic simulation on 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.

Information flow policies are confidentiality policies that control information leakage through program execution. A common way to enforce secure information flow is through information flow type systems. Although type systems are compositional and usually enjoy decidable type checking or inference, their extensibility is very poor: type systems need to be redefined and proved sound for each new variation of security policy and programming language for which secure information flow verification is desired.

In contrast, program logics offer a general mechanism for enforcing a variety of safety policies, and for this reason are favoured in Proof Carrying Code, which is a promising security architecture for mobile code. However, the encoding of information flow policies in program logics is not straightforward because they refer to a relation between two program executions.

The purpose of this paper is to investigate logical formulations of secure information flow based on the idea of self-composition, which reduces the problem of secure information flow of a program P to a safety property for a program derived from P by composing P with a renaming of itself. Self-composition enables the use of standard techniques for information flow policy verification, such as program logics and model checking, that are suitable in Proof Carrying Code infrastructures.

We illustrate the applicability of self-composition in several settings, including different security policies such as non-interference and controlled forms of declassification, and programming languages including an imperative language with parallel composition, a non-deterministic language and, finally, a language with shared mutable data structures.

This paper explores a three dimensional characterisation of a declassification-based non-interference policy and its consequences. Two of the dimensions consist of specifying:

1. (a) the power of the attacker, that is, what public information a program has that an attacker can observe; and

2. (b) what secret information a program has that needs to be protected.

1. (c) the choice of program semantics, for example, trace semantics or denotational semantics, or any semantics in Cousot's semantics hierarchy.

Provenance is information recording the source, derivation or history of some information. Provenance tracking has been studied in a variety of settings, particularly database management systems. However, although many candidate definitions of provenance have been proposed, the mathematical or semantic foundations of data provenance have received comparatively little attention. In this paper, we argue that dependency analysis techniques familiar from program analysis and program slicing provide a formal foundation for forms of provenance that are intended to show how (part of) the output of a query depends on (parts of) its input. We introduce a semantic characterisation of such dependency provenance for a core database query language, show that minimal dependency provenance is not computable, and provide dynamic and static approximation techniques. We also discuss preliminary implementation experience with using dependency provenance to compute data slices, or summaries of the parts of the input relevant to a given part of the output.

Given a program, a quotient can be obtained from it by deleting zero or more statements. The field of program slicing is concerned with computing a quotient of a program that preserves part of the behaviour of the original program. All program slicing algorithms take account of the structural properties of a program, such as control dependence and data dependence, rather than the semantics of its functions and predicates, and thus work, in effect, with program schemas. The dynamic slicing criterion of Korel and Laski requires only that program behaviour is preserved in cases where the original program follows a particular path, and that the slice/quotient follows this path. In this paper we formalise Korel and Laski's definition of a dynamic slice as applied to linear schemas, and also formulate a less restrictive definition in which the path through the original program need not be preserved by the slice. The less restrictive definition has the benefit of leading to smaller slices. For both definitions, we compute complexity bounds for the problems of establishing whether a given slice of a linear schema is a dynamic slice and whether a linear schema has a non-trivial dynamic slice, and prove that the latter problem is NP-hard in both cases. We also give an example to prove that minimal dynamic slices (whether or not they preserve the original path) need not be unique.