arXiv subjects

Mário S. Alvim

Publications and source records attributed to Mário S. Alvim.

26 records · Page 2Linked to original sources

arXiv2018

Leakage and Protocol Composition in a Game-Theoretic Perspective

In the inference attacks studied in Quantitative Information Flow (QIF), the adversary typically tries to interfere with the system in the attempt to increase its leakage of secret information. The defender, on the other hand, typically tries to decrease leakage by introducing some controlled noise. This noise introduction can be modeled as a type of protocol composition, i.e., a probabilistic choice among different protocols, and its effect on the amount of leakage depends heavily on whether or not this choice is visible to the adversary. In this work we consider operators for modeling visible and invisible choice in protocol composition, and we study their algebraic properties. We then formalize the interplay between defender and adversary in a game-theoretic framework adapted to the specific issues of QIF, where the payoff is information leakage. We consider various kinds of leakage games, depending on whether players act simultaneously or sequentially, and on whether or not the choices of the defender are visible to the adversary. Finally, we establish a hierarchy of these games in terms of their information leakage, and provide methods for finding optimal strategies (at the points of equilibrium) for both attacker and defender in the various cases. The full version of this paper can be found in arXiv:1803.10042

cs.CR↗

arXiv2017

Information Leakage Games

We consider a game-theoretic setting to model the interplay between attacker and defender in the context of information flow, and to reason about their optimal strategies. In contrast with standard game theory, in our games the utility of a mixed strategy is a convex function of the distribution on the defender's pure actions, rather than the expected value of their utilities. Nevertheless, the important properties of game theory, notably the existence of a Nash equilibrium, still hold for our (zero-sum) leakage games, and we provide algorithms to compute the corresponding optimal strategies. As typical in (simultaneous) game theory, the optimal strategy is usually mixed, i.e., probabilistic, for both the attacker and the defender. From the point of view of information flow, this was to be expected in the case of the defender, since it is well known that randomization at the level of the system design may help to reduce information leaks. Regarding the attacker, however, this seems the first work (w.r.t. the literature in information flow) proving formally that in certain cases the optimal attack strategy is necessarily probabilistic.

cs.CR↗

arXiv2017

Quantifying vulnerability of secret generation using hyper-distributions (extended version)

Traditional approaches to Quantitative Information Flow (QIF) represent the adversary's prior knowledge of possible secret values as a single probability distribution. This representation may miss important structure. For instance, representing prior knowledge about passwords of a system's users in this way overlooks the fact that many users generate passwords using some strategy. Knowledge of such strategies can help the adversary in guessing a secret, so ignoring them may underestimate the secret's vulnerability. In this paper we explicitly model strategies as distributions on secrets, and generalize the representation of the adversary's prior knowledge from a distribution on secrets to an environment, which is a distribution on strategies (and, thus, a distribution on distributions on secrets, called a hyper-distribution). By applying information-theoretic techniques to environments we derive several meaningful generalizations of the traditional approach to QIF. In particular, we disentangle the vulnerability of a secret from the vulnerability of the strategies that generate secrets, and thereby distinguish security by aggregation--which relies on the uncertainty over strategies--from security by strategy--which relies on the intrinsic uncertainty within a strategy. We also demonstrate that, in a precise way, no further generalization of prior knowledge (e.g., by using distributions of even higher order) is needed to soundly quantify the vulnerability of the secret.

cs.CR↗

arXiv2013

Computational Aspects of the Calculus of Structure

Logic is the science of correct inferences and a logical system is a tool to prove assertions in a certain logic in a correct way. There are many logical systems, and many ways of formalizing them, e.g., using natural deduction or sequent calculus. Calculus of structures (CoS) is a new formalism proposed by Alessio Guglielmi in 2004 that generalizes sequent calculus in the sense that inference rules can be applied at any depth inside a formula, rather than only to the main connective. With this feature, proofs in CoS are shorter than in any other formalism supporting analytical proofs. Although it is great to have the freedom and expressiveness of CoS, under the point of view of proof search more freedom means a larger search space. And that should be restricted when looking for complete automation of deductive systems. Some efforts were made to reduce this non-determinism, but they are all basically operational approaches, and no solid theoretical result regarding the computational behaviour of CoS has been achieved so far. The main focus of this thesis is to discuss ways to propose a proof search strategy for CoS suitable to implementation. This strategy should be theoretical instead of purely operational. We introduce the concept of incoherence number of substructures inside structures and we use this concept to achieve our main result: there is an algorithm that, according to our conjecture, corresponds to a proof search strategy to every provable structure in the subsystem of FBV (the multiplicative linear logic MLL plus the rule mix) containing only pairwise distinct atoms. Our algorithm is implemented and we believe our strategy is a good starting point to exploit the computational aspects of CoS in more general systems, like BV itself.

cs.LO↗

arXiv2012

Formal approaches to information hiding: An analysis of interactive systems, statistical disclosure control, and refinement of specifications

In this thesis we consider the problem of information hiding in the scenarios of interactive systems, statistical disclosure control, and refinement of specifications. We apply quantitative approaches to information flow in the first two cases, and we propose improvements for the usual solutions based on process equivalences for the third case. In the first scenario we consider the problem of defining the information leakage in interactive systems where secrets and observables can alternate during the computation and influence each other. We show that the information-theoretic approach which interprets such systems as (simple) noisy channels is not valid. The principle can be recovered if we consider channels with memory and feedback. We also propose the use of directed information from input to output as the real measure of leakage in interactive systems. In the second scenario we consider the problem of statistical disclosure control, which concerns how to reveal accurate statistics about a set of respondents while preserving the privacy of individuals. We focus on the concept of differential privacy, a notion that has become very popular in the database community. We show how to model the query system in terms of an information-theoretic channel, and we compare the notion of differential privacy with that of min-entropy leakage.In the third scenario we address the problem of using process equivalences to characterize information-hiding properties. We show that, in the presence of nondeterminism, this approach may rely on the assumption that the scheduler "works for the benefit of the protocol", and this is often not a safe assumption. We present a formalism in which we can specify admissible schedulers and, correspondingly, safe versions of complete-trace equivalence and bisimulation, and we show that safe equivalences can be used to establish information-hiding properties.

cs.CR↗

arXiv2011

On the relation between Differential Privacy and Quantitative Information Flow

Differential privacy is a notion that has emerged in the community of statistical databases, as a response to the problem of protecting the privacy of the database's participants when performing statistical queries. The idea is that a randomized query satisfies differential privacy if the likelihood of obtaining a certain answer for a database $x$ is not too different from the likelihood of obtaining the same answer on adjacent databases, i.e. databases which differ from $x$ for only one individual. Information flow is an area of Security concerned with the problem of controlling the leakage of confidential information in programs and protocols. Nowadays, one of the most established approaches to quantify and to reason about leakage is based on the Rényi min entropy version of information theory. In this paper, we analyze critically the notion of differential privacy in light of the conceptual framework provided by the Rényi min information theory. We show that there is a close relation between differential privacy and leakage, due to the graph symmetries induced by the adjacency relation. Furthermore, we consider the utility of the randomized answer, which measures its expected degree of accuracy. We focus on certain kinds of utility functions called "binary", which have a close correspondence with the Rényi min mutual information. Again, it turns out that there can be a tight correspondence between differential privacy and utility, depending on the symmetries induced by the adjacency relation and by the query. Depending on these symmetries we can also build an optimal-utility randomization mechanism while preserving the required level of differential privacy. Our main contribution is a study of the kind of structures that can be induced by the adjacency relation and the query, and how to use them to derive bounds on the leakage and achieve the optimal utility.

cs.LO↗

arXiv2011

Differential Privacy: on the trade-off between Utility and Information Leakage

Differential privacy is a notion of privacy that has become very popular in the database community. Roughly, the idea is that a randomized query mechanism provides sufficient privacy protection if the ratio between the probabilities that two adjacent datasets give the same answer is bound by e^epsilon. In the field of information flow there is a similar concern for controlling information leakage, i.e. limiting the possibility of inferring the secret information from the observables. In recent years, researchers have proposed to quantify the leakage in terms of Rényi min mutual information, a notion strictly related to the Bayes risk. In this paper, we show how to model the query system in terms of an information-theoretic channel, and we compare the notion of differential privacy with that of mutual information. We show that differential privacy implies a bound on the mutual information (but not vice-versa). Furthermore, we show that our bound is tight. Then, we consider the utility of the randomization mechanism, which represents how close the randomized answers are, in average, to the real ones. We show that the notion of differential privacy implies a bound on utility, also tight, and we propose a method that under certain conditions builds an optimal randomization mechanism, i.e. a mechanism which provides the best utility while guaranteeing differential privacy.

cs.CR↗

arXiv2010

Differential Privacy versus Quantitative Information Flow

Differential privacy is a notion of privacy that has become very popular in the database community. Roughly, the idea is that a randomized query mechanism provides sufficient privacy protection if the ratio between the probabilities of two different entries to originate a certain answer is bound by e^ε. In the fields of anonymity and information flow there is a similar concern for controlling information leakage, i.e. limiting the possibility of inferring the secret information from the observables. In recent years, researchers have proposed to quantify the leakage in terms of the information-theoretic notion of mutual information. There are two main approaches that fall in this category: One based on Shannon entropy, and one based on Rényi's min entropy. The latter has connection with the so-called Bayes risk, which expresses the probability of guessing the secret. In this paper, we show how to model the query system in terms of an information-theoretic channel, and we compare the notion of differential privacy with that of mutual information. We show that the notion of differential privacy is strictly stronger, in the sense that it implies a bound on the mutual information, but not viceversa.

cs.IT↗