Sites Inria

Version française

COMETE Research team

Concurrency, Mobility and Transactions

Team presentation

In COMETE we study emerging concepts of the modern era of computing. Security and privacy are some of the fundamental concerns that arise in this setting: the frequent interaction between users and electronic devices, and the continuous connection between these devices and the internet, offer malicious agents the opportunity to gather and store huge amount of information without the individual even being aware of it. In addition to the security concerns, the problems of correctness, robustness and reliability are made more challenging by the complexity of modern systems, since they are highly concurrent and distributed. Despite being based on impressive engineering technologies, they are still prone to faulty behavior due to errors in the software design.

To address these challenges, we study formal frameworks for specifying these systems, theories for defining the desired properties of correctness and security and for reasoning about them, and methods and techniques for proving that a given system satisfies the intended properties. 

Research themes

  • Security and privacy: We are interested in the problem of the leakage of secret information through public observables. Ideally we would like systems to be completely secure, but in practice this goal is often impossible to achieve. Therefore, we need to reason about the amount of information leaked, the adversary's gain from this leakage and the trade-off between the privacy and the utility provided to the user.
  • Location privacy: we study the problem of accessing location-based systems while protecting the location of the user, by adding controlled noise to the reported position.
  • Expressiveness of Concurrent Formalisms: We study computational models and languages for distributed, probabilistic and mobile systems, with a particular attention to expressiveness issues. We aim at developing criteria to assess the expressive power of a model or formalism in a distributed setting, to compare existing models and formalisms, and to define new ones according to an intended level of expressiveness.
  • Concurrent constraint programming: a well established process calculus for modeling systems where agents interact by posting and asking information in a store. Our research focuses on the study of bisimulation semantics for ccp, as well as on the extension of ccp with constructs to capture emergent systems such as those in social networks and cloud computing.
  • Verification: We are interested in developing verification techniques for concurrent systems, with a focus on proving that a given system satisfies the intended security or privacy properties.

Software

  • Location Guard: a browser extension that allows to protect your location while using location-aware websites, by adding controlled noise to it.
  • libqif: The goal of libqif is to provide an efficient C++ toolkit implementing a variety of techniques and algorithms
    from the area of quantitative information flow and differential privacy.
  • D-SPACES: an implementation of constraint systems with space and extrusion operators. Constraint systems
    are algebraic models that allow for a semantic language-like representation of information in systems where
    the concept of space is a primary structural feature.

International and industrial relations

  • Collaboration with Renault, on privacy-preserving services for "connected" cars
  • Regular collaboration with several international partners, including: Geoffrey Smith (Florida International University, United States), Carroll Morgan (NICTA, Australia), Annabelle McIver (Maquarie University, Australia), Moreno Falaschi (University of Siena, Italy), Mario Ferreira Alvim Junior (Federal University of Minas Gerais, Brazil), Camilo Rueda (Universidad Javeriana Cali, Colombia)
  • Privacy-Friendly Services and Applications: project sponsored by Microsoft Research Lab, on methods to preserve privacy in
    web services and location-based services. International Partners: Microsoft Research Lab, Cambridge, UK
  • LOGIS: Logical and Formal Methods for Information Security, Inria associate team. International Partners: Keio University (Japan), AIST (Japan), JAIST (Japan), University of Tokyo (Japan)
  • REPAS: Reliable and Privacy-Aware Software Systems via Bisimulation Metrics, ANR project. International Partners: University
    of Bologna (Italy)
  • PACE: Beyond plain Processes: Analysis techniques, Coinduction and Expressiveness, ANR project. International Partners: University of Bologna (Italy), Shanghai Jiao Tong University (China)
  • LOCALI: Logical Approach to Novel Computational Paradigms, ANR project. International Partners: Chinese Academy of Science in Beijin (China)
  • MUSICAL: Music and Spatial Interaction with Constraints, Algebra and Logic: Foundations and Applications. International Partners: PUJ Cali (Colombia), Universidade Federal do Rio Grande do Norte (Brazil).
  • CLASSIC: Concurrency, Logic and Algebra for Social and Spatial Interactive Computation. International Partners: Universidade Federal do Rio Grande do Norte (Brazil).

 

Keywords: Models and Languages for Concurrent and Distributed Computation Security Formal Methods Implementation