Sites Inria

English version

Equipe de recherche COMETE

Concurrence, Mobilité et Transactions

Présentation de l'équipe

L'équipe-projet COMETE étudie les concepts émergeant de l'ère moderne de l'informatique. La sécurité et la protection de la vie privée sont parmi les préoccupations fondamentales qui se posent dans ce contexte: l'interaction fréquente entre les utilisateurs et les appareils électroniques, et la connexion continue entre ces appareils et l'Internet, offrent aux agents malveillants la possibilité de recueillir et stocker une énorme quantité d'informations sans même que les utilisateurs soient conscients. En plus des problèmes de sécurité, les problèmes de la correction, de robustesse et de fiabilité sont rendus plus difficiles par la complexité des systèmes modernes, car ils sont très concurrents et distribués. En dépit d'être basés sur des technologies d'ingénierie impressionnantes, ils sont toujours sujet à un comportement défectueux en raison d'erreurs dans la conception du logiciel.
 
Pour faire face à ces défis, nous étudions des cadres formels pour la spécification de ces systèmes, des théories permettant de définir les propriétés souhaitées de correction et de sécurité, ainsi que des méthodes et des techniques pour prouver qu'un système satisfait ces propriétés.

Axes de recherche

  • Sécurité et protection de la vie privée: Nous sommes intéressés par le problème de la fuite d'informations secrètes à travers des observables publics. Idéalement, on voudrait que les systèmes soient complètement sécurisés, mais dans la pratique cet objectif est souvent impossible à atteindre. Par conséquent, nous avons besoin de raisonner sur la quantité d'informations divulguées, le gain de l'adversaire de cette fuite et le compromis entre la vie privée et l'utilité fournie à l'utilisateur.
  • Vie privée et géolocalisation: nous étudions le problème de l'accès aux systèmes basés sur la localisation tout en protégeant l'emplacement de l'utilisateur, en ajoutant du bruit contrôlé à la position rapportée.
  • Expressivité des formalismes concomitants: Nous étudions les modèles et les langages computationnels pour les systèmes distribués, probabilistes et mobiles, en accordant une attention particulière aux questions d'expressivité. Nous cherchons à développer des critères pour évaluer le pouvoir expressif d'un modèle ou d'un formalisme dans un cadre distribué, comparer des modèles et des formalismes existants, et en définir des nouveaux selon le niveau d'expressivité souhaité.
  • Programmation concurrente par contraintes: un modèle bien établi pour la spécification de systèmes concurrents où les agents ajoutent de l'information ou interrogent si certains faits peuvent être déduits. Notre recherche se concentre sur l'étude de la sémantique de bisimulation pour ccp, ainsi que sur l'extension de ccp avec des constructions pour capturer des systèmes émergeants tels que ceux dans les réseaux sociaux et le cloud computing.
  • Verification: on s'intéresse à développer des techniques de verification pour des systèmes concurrents, en mettant l'accent sur la preuve qu'un système satisfait les propriétés de sécurité ou de vie privée souhaitées.

Logiciels

  • Location Guard: une extension de navigateur qui permet de protéger votre position lors de l'utilisation de sites web avec géolocalisation intégrée, en y ajoutant du bruit contrôlé.
  • libqif: L'objectif de libqif est de fournir une boîte à outils C++ efficace mettant en œuvre une variété de techniques et d'algorithmes dans les domaines de "quantitative information flow" et de "differential privacy".
  • D-SPACES: Une implémentation de systèmes de contraintes avec des opérateurs d'espace et d'extrusion.

Relations industrielles et internationales

  • Collaboration avec Renault sur la protection de la vie privée des voitures "connectées"
  • Une collaboration régulière avec plusieurs partenaires internationaux, parmi lesquels: 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: projet financé par Microsoft Research Lab, sur les méthodes de préservation de la vie privée dans les services Web et les services de localisation. Partenaires internationaux: Microsoft Research Lab, Cambridge, UK
  • LOGIS: Logical and Formal Methods for Information Security, Equipe Associée Inria. Partenaires internationaux: Keio University (Japan), AIST (Japan), JAIST (Japan), University of Tokyo (Japan)
  • REPAS: Reliable and Privacy-Aware Software Systems via Bisimulation Metrics, projet ANR. Partenaires internationaux: University
    of Bologna (Italy)
  • PACE: Beyond plain Processes: Analysis techniques, Coinduction and Expressiveness, projet ANR. Partenaires internationaux: University of Bologna (Italy), Shanghai Jiao Tong University (China)
  • LOCALI: Logical Approach to Novel Computational Paradigms, projet ANR. Partenaires internationaux: Chinese Academy of Science in Beijin (China)
  • MUSICAL: Music and Spatial Interaction with Constraints, Algebra and Logic: Foundations and Applications. Partenaires internationaux: PUJ Cali (Colombia), Universidade Federal do Rio Grande do Norte (Brazil).
  • CLASSIC: Concurrency, Logic and Algebra for Social and Spatial Interactive Computation. Partenaires internationaux: Universidade Federal do Rio Grande do Norte (Brazil).

 

Mots-clés : Modèles et Languages pour le Calcul Concurrent et Distribué Sécurité Méthodes Formelles Implementation

Suivez Inria tout au long de son 50e anniversaire et au-delà !