WP3 - Security and Information Flow Properties
Partners Involved: INRIA / TUE / UNC / UBA
In today’s interconnected world, it is becoming increasingly easy to collect a huge amount of information about individuals. As a result, security mechanisms that protect the anonymity and privacy of users are of vital importance. Lately, the design of methods for information protection, and the frameworks for reasoning and verifying them, have considered probabilistic aspects. The reason is twofold. First, the data to be protected often range in domains naturally subject to statistical considerations. Second, those methods often use randomization to obfuscate the link between the information to be protected and the information which is publicly available. Many conceptual frameworks deal with the key issue of assessing the amount of information leaked by a system. One of the most successful approaches among these is based on Information Theory which provides the foundation for the concept of covert channel.
- A general framework for information leakage. We want to develop a conceptual framework to reason about probabilistic information leakage which can deal with different notions of adversaries and different ways to measure the success of an attack. We also intend to account for the possible extra knowledge or belief that an adversary may have. We plan to follow the lines of Köpf and Basin, who have proposed a general information-theoretic approach for the case of deterministic systems, where the kind of attack and its effectiveness is represented by the notion of entropy (a parameter in this approach).
- Relation with Differential Privacy. In recent years, differential privacy has emerged as a successful practical approach for ensuring user's privacy when releasing statistical information about a database. The goals in this area are closely related to those of information flow. We will investigate the relation between differential privacy and established notions for measuring information leakages from probabilistic information flow, (e.g., those based on information theory). In statistical queries the notion of utility plays an important role: we want to reveal a value as close as possible to the real answer, without sacrificing users' privacy. We will investigate methods to maximize utility while satisfying differential privacy.
- Restricting the knowledge of the scheduler. In security the handling of non- determinism via the notion of scheduler presents problems similar to those explained in WP1.3: some unrealistic schedulers may break the property that we want to verify. In the particular case of security, schedulers which have the (unrealistic) ability to peak at the secrets, may leak this information thus making every protocol unsafe. We plan to investigate a notion of partial-information scheduler that would at the same time be suitable in the context of security and allow for efficient verification. In particular we plan to investigate whether the problem of computing optimal conditional probabilities and/or reachability.
- Probabilistic analysis of voting and routing protocols. There exist many proposed voting schemes that are interesting to analyse with the formal framework proposed above. In particular, we plan to model and analyse schemes based on Chaum's mix-nets. In this setting, it is challenging to model and compute the specific probabilistic property of interest, voter privacy, under information leakage arising from both corrupt components and auditing processes that disclose partial information from the election (like RPC, randomized partial checking). We also plan to tackle other protocols based on mix- nets, like the anonymous routing protocol Tor.
- Probabilistic analysis of concrete implementations. The analysis of abstract models of probabilistic systems, as in the above objectives, provides foundational tools for modelling and verifying systems. We also plan to investigate the analysis of concrete, compiled randomized code, so that we can tackle the analysis of an actual protocol implementation like Tor. We plan to extend tools for symbolic execution like KLEE or bitblaze to being able to either extract a probabilistic model we can then verify, or to symbolically analyse a concrete program.
