The ongoing deprecation of third-party cookies by web browser vendors has sparked the proposal of alternative methods to support more privacy-preserving personalized advertising on web browsers and applications. The Topics API is being proposed by Google to provide third-parties with "coarse-grained advertising topics that the page visitor might currently be interested in". In this paper, we analyze the re-identification risks for individual Internet users and the utility provided to advertising companies by the Topics API, i.e. learning the most popular topics and distinguishing between real and random topics. We provide theoretical results dependent only on the API parameters that can be readily applied to evaluate the privacy and utility implications of future API updates, including novel general upper-bounds that account for adversaries with access to unknown, arbitrary side information, the value of the differential privacy parameter ε, and experimental results on real-world data that validate our theoretical model.

The study of leakage measures for privacy has been a subject of intensive research and is an important aspect of understanding how privacy leaks occur in computer systems. Differential privacy has been a focal point in the privacy community for some years and yet its leakage characteristics are not completely understood. In this paper we bring together two areas of research -information theory and the g-leakage framework of quantitative information flow (QIF)- to give an operational interpretation for the epsilon parameter of local differential privacy. We find that epsilon emerges as a capacity measure in both frameworks; via (log)-lift, a popular measure in information theory; and via max-case g-leakage, which we introduce to describe the leakage of any system to Bayesian adversaries modelled using “worst-case” assumptions under the QIF framework. Our characterisation resolves an important question of interpretability of epsilon and consolidates a number of disparate results covering the literature of both information theory and Quantitative information flow.

We combine Kronecker products, and quantitative information flow, to give a novel formal analysis for the fine-grained verification of utility in complex privacy pipelines. The combination explains a surprising anomaly in the behaviour of utility of privacy-preserving pipelines - that sometimes a reduction in privacy results also in a decrease in utility. We use the standard measure of utility for Bayesian analysis, introduced by Ghosh at al. [1], to produce tractable and rigorous proofs of the fine-grained statistical behaviour leading to the anomaly. More generally, we offer the prospect of formal-analysis tools for utility that complement extant formal analyses of privacy. We demonstrate our results on a number of common privacy-preserving designs.

We study the privacy-utility trade-off in the context of metric differential privacy. Ghosh et al. introduced the idea of universal optimality to characterise the “best” mechanism for a certain query that simultaneously satisfies (a fixed) ε-differential privacy constraint whilst at the same time providing better utility compared to any other ε-differentially private mechanism for the same query. They showed that the Geometric mechanism is universally optimal for the class of counting queries. On the other hand, Brenner and Nissim showed that outside the space of counting queries, and for the Bayes risk loss function, no such universally optimal mechanisms exist. Except for the universal optimality of the Laplace mechanism, there have been no generalisations of these universally optimal results to other classes of differentially-private mechanisms. In this paper, we use metric differential privacy and quantitative information flow as the fundamental principle for studying universal optimality. Metric differential privacy is a generalisation of both standard (i.e., central) differential privacy and local differential privacy, and it is increasingly being used in various application domains, for instance in location privacy and in privacy-preserving machine learning. Similar to the approaches adopted by Ghosh et al. and Brenner and Nissim, we measure utility in terms of loss functions, and we interpret the notion of a privacy mechanism as an information-theoretic channel satisfying constraints defined by ε-differential privacy and a metric meaningful to the underlying state space. Using this framework we are able to clarify Nissim and Brenner’s negative results by (a) that in fact all privacy types contain optimal mechanisms relative to certain kinds of non-trivial loss functions, and (b) extending and generalising their negative results beyond Bayes risk specifically to a wide class of non-trivial loss functions. Our exploration suggests that universally optimal mechanisms are indeed rare within privacy types. We therefore propose weaker universal benchmarks of utility called privacy type capacities. We show that such capacities always exist and can be computed using a convex optimisation algorithm. Further, we illustrate these ideas on a selection of examples with several different underlying metrics.

We study the privacy-utility trade-off in the context of metric differential privacy. Ghosh et al. introduced the idea of universal optimality to characterise the “best” mechanism for a certain query that simultaneously satisfies (a fixed)$\mathcal{E-}$differential privacy constraint whilst at the same time providing better utility compared to any other s-differentially private mechanism for the same query. They showed that the Geometric mechanism is universally optimal for the class of counting queries. On the other hand, Brenner and Nissim showed that outside the space of counting queries, and for the Bayes risk loss function, no such universally optimal mechanisms exist. Except for universal optimality of the Laplace mechanism, there have been no generalisations of these universally optimal results to other classes of differentially-private mechanisms. In this paper we use metric differential privacy and quantitative information flow as the fundamental principle for studying universal optimality. Metric differential privacy is a generali-sation of both standard (i.e., central) differential privacy and local differential privacy, and it is increasingly being used in various application domains, for instance in location privacy and in privacy preserving machine learning. As do Ghosh et al. and Brenner and Nissim, we measure utility in terms of loss functions, and we interpret the notion of a privacy mechanism as an information-theoretic channel satisfying constraints defined by ε-differcntlal privacy and a metric meaningful to the underlying state space. Using this framework we are able to clarify Nissim and Brenner's negative results by (a) that in fact all privacy types contain optimal mechanisms relative to certain kinds of non-trivial loss functions, and (b) extending and generalising their negative results beyond Bayes risk specifically to a wide class of non-trivial loss functions. Our exploration suggests that universally optimal mechanisms are indeed rare within privacy types. We therefore propose weaker universal benchmarks of utility called privacy type ca-pacities. We show that such capacities always exist and can be computed using a convex optimisation algorithm. We illustrate these ideas on a selection of examples with several different underlying metrics.

We present a systematic refactoring of the conventional treatment of privacy analyses, basing it on mathematical concepts from the framework of Quantitative Information Flow (QIF ). The approach we suggest brings three principal advantages: it is flexible, allowing for precise quantification and comparison of privacy risks for attacks both known and novel; it can be computationally tractable for very large, longitudinal datasets; and its results are explainable both to politicians and to the general public. We apply our approach to a very large case study: the Educational Censuses of Brazil, curated by the governmental agency inep, which comprise over 90 attributes of approximately 50 million individuals released longitudinally every year since 2007. These datasets have only very recently (2018–2021) attracted legislation to regulate their privacy — while at the same time continuing to maintain the openness that had been sought in Brazilian society. inep’s reaction to that legislation was the genesis of our project with them. In our conclusions here we share the scientific, technical, and communication lessons we learned in the process.

Differential Privacy protects individuals’ data when statistical queries are published from aggregated databases: applying "obfuscating" mechanisms to the query results makes the released information less specific but, unavoidably, also decreases its utility. Yet it has been shown that for discrete data (e.g. counting queries), a mandated degree of privacy and a reasonable interpretation of loss of utility, the Geometric obfuscating mechanism is optimal: it loses as little utility as possible [Ghosh et al. [1]].For continuous query results however (e.g. real numbers) the optimality result does not hold. Our contribution here is to show that optimality is regained by using the Laplace mechanism for the obfuscation.The technical apparatus involved includes the earlier discrete result [Ghosh op. cit.], recent work on abstract channels and their geometric representation as hyper-distributions [Alvim et al. [2]], and the dual interpretations of distance between distributions provided by the Kantorovich-Rubinstein Theorem.

No abstract available.

In this paper we study the relationship between privacy and accuracy in the context of correlated datasets. We use a model of quantitative information flow to describe the the trade-off between privacy of individuals' data and and the utility of queries to that data by modelling the effectiveness of adversaries attempting to make inferences after a data release. We show that, where correlations exist in datasets, it is not possible to implement optimal noise-adding mechanisms that give the best possible accuracy or the best possible privacy in all situations. Finally we illustrate the trade-off between accuracy and privacy for local and oblivious differentially private mechanisms in terms of inference attacks on medium-scale datasets.

This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.

We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. "super-martingales") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.

This article investigates the semantic intricacies of conditioning, a main feature in probabilistic programming. Our study is based on an extension of the imperative probabilistic guarded command language pGCL with conditioning. We provide a weakest precondition (wp) semantics and an operational semantics. To deal with possibly diverging program behavior, we consider liberal preconditions. We show that diverging program behavior plays a key role when defining conditioning. We establish that weakest preconditions coincide with conditional expected rewards in Markov chains—the operational semantics—and that the wp-semantics conservatively extends the existing semantics of pGCL (without conditioning). An extension of these results with nondeterminism turns out to be problematic: although an operational semantics using Markov decision processes is rather straightforward, we show that providing an inductive wp-semantics in this setting is impossible. Finally, we present two program transformations that eliminate conditioning from any program. The first transformation hoists conditioning while updating the probabilistic choices in the program, while the second transformation replaces conditioning—in the same vein as rejection sampling—by a program with loops. In addition, we present a last program transformation that replaces an independent identically distributed loop with conditioning.

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.

Hidden Markov Models, HMM's, are mathematical models of Markov processes whose state is hidden but from which information can leak via channels. They are typically represented as 3-way joint probability distributions. We use HMM's as denotations of probabilistic hidden-state sequential programs, after recasting them as “abstract” HMM's, i.e. computations in the Giry monad D, and equipping them with a partial order of increasing security. However to encode the monadic type with hiding over state X we use DX→D2X rather than the conventional X→DX. We illustrate this construction with a very small Haskell prototype. We then present uncertainty measures as a generalisation of the extant diversity of probabilistic entropies, and we propose characteristic analytic properties for them. Based on that, we give a “backwards”, uncertainty-transformer semantics for HMM's, dual to the “forwards” abstract HMM's. Finally, we discuss the Dalenius desideratum for statistical databases as an issue in semantic compositionality, and propose a means for taking it into account.

We use hidden Markov models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or ‘implements’ relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an ‘implementation’ program leaks no more than its ‘specification’ program. This joins two themes: we extend our earlier work, having iteration but only qualitative (Morgan 2009), by making it quantitative; and we extend our earlier quantitative work (McIver et al. 2010) by including iteration. We advocate stepwise refinement and source-level program algebra – both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.

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.

Abstract The Shadow Semantics (Morgan, Math Prog Construction, vol 4014, pp 359–378, 2006 ; Morgan, Sci Comput Program 74(8):629–653, 2009 ) is a possibilistic (qualitative) model for noninterference security. Subsequent work (McIver et al., Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, 2010 ) presents a similar but more general quantitative model that treats probabilistic information flow. Whilst the latter provides a framework to reason about quantitative security risks, that extra detail entails a significant overhead in the verification effort needed to achieve it. Our first contribution in this paper is to study the relationship between those two models (qualitative and quantitative) in order to understand when qualitative Shadow proofs can be “promoted” to quantitative versions, i.e. in a probabilistic context. In particular we identify a subset of the Shadow’s refinement theorems that, when interpreted in the quantitative model, still remain valid even in a context where a passive adversary may perform probabilistic analysis. To illustrate our technique we show how a semantic analysis together with a syntactic restriction on the protocol description, can be used so that purely qualitative reasoning can nevertheless verify probabilistic refinements for an important class of security protocols. We demonstrate the semantic analysis by implementing the Shadow semantics in Rodin, using its special-purpose refinement provers to generate (and discharge) the required proof obligations (Abrial et al., STTT 12(6):447–466, 2010 ). We apply the technique to some small examples based on secure multi-party computations.

We propose a novel domain-theoretic model for nondeterminism, probability and hidden state, with relations on it that compare information flow. One relation is Smyth-like, based on a structural, refinement-like order between semantic elements; the other is a testing order that generalises several extant entropy-based techniques. Our principal theorem is that the two orders are equivalent. The model is based on the Giry/Kantorovich monads, and it abstracts Partially Observable Markov Decision Processes by discarding observables' actual values but retaining the effect they had on an observer's knowledge. We illustrate the model, and its orders, on some small examples, where we find that our formalism provides the apparatus for comparing systems in terms of the information they leak.

In this paper we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Networks), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.

This paper describes a Continual And Explicit Comparison (CAEC) approach to overcoming proactive inhibition and amplifying proactive facilitation in a second year Java course. The approach utilizes continual and explicit comparison to students' prior learning (in this case C++ programming knowledge) in early stages of learning the new language in order to more rapidly build understanding and more definitively form concept boundaries between the two languages. The majority of students felt the approach supported learning of the second language (proactive facilitation) without causing any interference with second language learning (i.e. minimal proactive inhibition). Some students also indicated that the approach enhanced their understanding of the first language (retroactive facilitation) and overwhelmingly agreed that the approach did not interfere with their understanding of the first language (i.e. minimal retroactive inhibition). Students also indicated that their Java programming ability and their enjoyment of programming increased during the period that the continual and explicit comparison approach was applied.

Abstract A truly secure protocol is one which never violates its security requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guarantees, as far as they are possible, require formal, rigorous techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our rigorous technique is refinement , until recently not much applied to security. We argue its benefits by using refinement-based program algebra to develop several security case studies. That is one of our contributions here. The soundness of the technique follows from its compositional semantics, one which we defined (elsewhere) to support a specialisation of standard refinement by enriching standard semantics with information that tracks correlations between hidden state and visible behaviour. A further contribution is to extend the basic theory of secure refinement (Morgan in Mathematics of program construction, Springer, Berlin, vol. 4014, pp. 359–378, 2006 ) with special features required by our case studies, namely agent-based systems with complementary security requirements, and looping programs.

The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qM μ extends to include probabilistic choice.We make two major contributions to the theory of such systems. The first is to show that for a finite-state system, the logical interpretation of qM μ, via fixed points in a domain of real-valued functions into [0, 1], is equivalent to an operational interpretation given as a turn-based gambling game between two players.The second contribution is to show that each player in the gambling game has an optimal memoryless strategy---that is, a strategy which is independent of the game's history, and with which a player can achieve his optimal expected reward however his opponent chooses to play. Moreover, since qM μ is expressive enough to encode stochastic parity games , our result implies the existence of memoryless strategies in that framework, as well.As an additional feature, we include an extensive case study demonstrating the aforementioned duality between games and logic. Among other things, it shows that the use of algorithmic verification techniques is mathematically justified in the practical computation of probabilistic system properties.

Wireless networks consist of small (possibly) portable devices which combine battery-operated computing power and wireless communications. There are a number of technical challenges associated with their operation. These are addressed in part by emerging protocols which attempt to make trade-offs between the various network phenomena in order to optimise overall performance relative to an intended application. Central to the protocol design process is the availability of rigorous tools and techniques for quantifying any putative performance advantage gained by a particular protocol, and the degree to which its use degrades overall network functionality. The tools performing this important task today are simulators but the results from them are often not realistic as they have not been validated against empirical data (D. Cavin et al.). In this paper we explore the benefits of a formal approach to the analysis of wireless networks; in particular we investigate how a careful mix of model checking and proof may be used both to validate design decisions, and to provide a full profile of quantitative performance-style behaviours. Moreover the counterexample facility of model checking can illustrate clearly the limitations of some standard protocols. We demonstrate the methods on flooding and communications protocols.

Summary form only given. Recent work in probabilistic programming semantics has provided a relatively simple probabilistic extension to predicate transformers, making it possible to treat small imperative probabilistic programs containing both demonic and angelic nondeterminism. That work in turn has extended to provide a probabilistic basis for the modal /spl mu/-calculus of Kozen (1983), and leads to a quantitative /spl mu/-calculus. Standard (non-probabilistic) /spl mu/-calculus can be interpreted either 'normally', over its semantic domain, or as a two-player game between an 'angel' and a 'demon' representing the two forms of choice. Stirling (1995) has argued that the two interpretations correspond. Quantitative p-calculus too can be interpreted both ways, with the novel interpretation being the second: a probabilistic game involving an angel and a demon. Each player seeks a strategy to maximise (resp. minimise) the game's 'outcome', with the steps in the game now being stochastic. That suggests a connection with Markov decision processes, in which players compete for high (resp. low) 'rewards' over a Markov transition system. In this paper we explore that connection, showing how for example discounted Markov decision processes (MDP's) and terminating MDP's can be written as quantitative p-formulae. The 'normal' interpretation of those formulae (i.e. over the semantic domain) then seems to give a much more direct access to existence theorems than the presentation usually associated with MDP's. Our technical contribution is to explain the coding of MDP's as quantitative p-formulae, to discuss the extension of the latte in incorporate 'rewards', and to illustrate the resulting reformulation of several existence theorems. In an appendix we give an algebraic characterisation of the new quantitative-with-reward form of the calculus.

Abstract Jones and Plotkin give a general construction for forming a probabilistic powerdomain over any directed-complete partial order [Jon90, JoP89]. We apply their technique to the failures/divergences semantic model for Communicating Sequential Processes [Hoa85]. The resulting probabilistic model supports a new binary operator, probabilistic choice, and retains all operators of CSP including its two existing forms of choice. An advantage of using the general construction is that it is easy to see which CSP identities remain true in the probabilistic model. A surprising consequence however is that probabilistic choice distributes through all other operators; such algebraic mobility means that the syntactic position of the choice operator gives little information about when the choice actually must occur. That in turn leads to some interesting interaction between probability and nondeterminism. A simple communications protocol is used to illustrate the probabilistic algebra, and several suggestions are made for accommodating and controlling nondeterminism when probability is present.

Probabilistic predicates generalize standard predicates over a state space; with probabilistic predicate transformers one thus reasons about imperative programs in terms of probabilistic pre- and postconditions. Probabilistic healthiness conditions generalize the standard ones, characterizing “real” probabilistic programs, and are based on a connection with an underlying relational model for probabilistic execution; in both contexts demonic nondeterminism coexists with probabilistic choice. With the healthiness conditions, the associated weakest-precondition calculus seems suitable for exploring the rigorous derivation of small probabilistic programs.