Logique Épistémique Probabiliste pour la Protection des Données Privées – PRELAP

Afin de développer des logiques adaptées pour formaliser un problème, nous basons nos recherches sur des études de cas conçues avec des experts du domaine (ici, la vie privée). Pour nos études de cas, nous utilisons la logique épistémique probabiliste imprécise (IPEL) pour décrire les connaissances statistiques.
Afin de développer la sémantique de l'IPEL, nous utilisons une méthodologie récemment développée et utilisée sur la logique épistémique dynamique intuitionniste probabiliste. La stratégie consiste à définir d'abord la sémantique algébrique de la logique - ici la logique épistémique avec des probabilités imprécises - puis à utiliser la théorie de la dualité pour trouver la sémantique relationnelle de la logique.
Pour développer la théorie de la preuve de ces logiques, nous utilisons des calculs des séquents - plus précisément des display calculs. Nous avons déjà conçu des display calculs pour la logique épistémique dynamique, la logique dynamique propositionnelle et la logique des ressources et des capacités.Pour ce faire nous combinons différents display calculs avec de bonnes propriétés afin d'obtenir un système de preuve pour une logique plus complexe. Dans notre cas, nous avons déjà des display calculs pour la logique épistémique dynamique; par conséquent, l'étape clé est de développer des display calculs pour les probabilités imprécises.
Pendant tout le processus, des experts en protection de la vie privée valident la sémantique induite par le modèle.

Nous avons déjà publié des travaux sur les probabilités imprécises:
[1] présente les fondements théoriques du projet. Nous présentons une logique modale pour formaliser le raisonnement basé sur des informations probabilistes incomplètes et contradictoires.
[2] développe la théorie de Dempster-Shafer pour tous les treillis finis. Ce résultat pose les fondations pour développer la théorie de Dempster-Shafer pour les logiques substructurelles, y compris les logiques paraconsistantes.
[3] pose les fondations pour développer des logiques multi valuées capables de formaliser, entre autres, un raisonnement non classique basé sur des fonctions de croyances.

Nous travaillons actuellement sur
- l'implémentation de la preuve de concept pour la formalisation du cas d'étude sur l'exposition minimale;
- terminer l'article sur les tableaux pour les logiques introduites dans [1]. Les tableaux fournissent un algorithme efficace pour vérifier si une formule est vraie ou non dans une logique donnée;
- étudier la théorie de la preuve des logiques introduites dans [1], plus spécifiquement nous concevons des display calculs pour celles-ci;
- développer la théorie de Dempster-Shafer et les probabilités conditionnelles dans le cadre des raisonnements paraconsistant.

[1] Marta Bílková, Sabine Frittella, Ondrej Majer, Sajad Nazari: Belief Based on Inconsistent Information. DaLí 2020: 68-86.dali 2020. arxiv.org/abs/2003.12906

[2] Sabine Frittella, Krishna Manoorkar, Alessandra Palmigiano, Apostolos Tzimoulis, Nachoem Wijnberg: Toward a Dempster-Shafer theory of concepts, International Journal of Approximate Reasoning, Volume 125, 2020, Pages 14-25, ISSN 0888-613X, doi.org/10.1016/j.ijar.2020.05.004.

[3] Willem Conradie, Sabine Frittella, Krishna Manoorkar, Sajad Nazari, Alessandra Palmigiano, Apostolos Tzimoulis, Nachoem M. Wijnberg: Rough concepts, Information Sciences, 2020, ISSN 0020-0255, doi.org/10.1016/j.ins.2020.05.074.

La protection de la vie privée est un enjeu majeur de notre société numérique, comme en témoigne le récent scandale de Cambridge Analytica autour des dernières élections américaines. Avant les élections, la société a récolté des informations personnelles d’utilisateurs de Facebook à l’aide d’un test de personnalité. Ces utilisateurs n’avaient pas conscience qu’ils donnaient accès à leurs données privées et à celles que leurs amis leur avait partagées. La société a ensuite non seulement exploité les informations brutes partagées par les utilisateurs, mais également les connaissances qu’elle a pu en déduire. De données simples, elle a déduit des connaissances probabilistes telles que «Tom vote Républicain avec une probabilité de 1/3», puis des connaissances statistiques telles que «le groupe de personnes formé par les amis de Tom vote Démocrate avec une probabilité comprise entre 0,9 et 1”. Ces connaissances ont ensuite été utilisées pour identifier des groupes de citoyens spécifiques et influencer leurs votes par le biais de publicités ciblées. Des politiques encadrant l’utilisation des données privées existent, mais aucune d’elles ne prend en compte ce type d’attaque combinant données personnelles et connaissances statistiques. L'objectif de ce projet est de fournir des outils mathématiques et logiciels qui permettent d’estimer l’exposition de la vie privée et d'étudier de telles attaques.

Les logiques épistémiques permettent de modéliser les connaissances d’un attaquant, et l’automatisation de preuves pour celles-ci permet de déterminer ce que l’attaquant peut inférer : elles sont donc un outil idéal pour nous. Utilisées conjointement avec les probabilités imprécises, elles nous permettent de modéliser des connaissances statistiques. Les probabilités imprécises et les logiques épistémiques nous fournissent les outils mathématiques nécessaires à la modélisation et l’analyse de l’exposition de la vie privée pour nos cas d’études.

Combiner probabilités imprécises et logiques épistémiques consistera à associer les raisonnements logiques et probabilistes; c’est un sujet majeur de recherche en logique mathématique depuis les lois de Boole. À partir des années 1980, diverses logiques probabilistes ont été introduites et ont eu un impact inestimable dans divers domaines tels que la théorie de la décision ou la représentation et la mise à jour des connaissances et des croyances. Cependant, des problèmes demeurent non résolus: (1) il n'y a pas de logiques épistémiques pour les connaissances statistiques et (2) il n'existe pas de théorie de la preuve pour les logiques épistémiques probabilistes, ce qui rend impossible l'automatisation de preuves.

Le projet réunit une équipe unique d’experts en logique mathématique, théorie de la preuve, méthodes formelles et protection de la vie privée pour résoudre ces problèmes. Nous allons:
(1) développer des logiques épistémiques capables de modéliser les connaissances statistiques,
(2) Développer des systèmes de preuves pour les logiques probabilistes,
(3) implémenter des assistants de preuve basés sur ces systèmes de preuve,
(4) étudier deux cas réels - la minimisation du nombre de données récoltées via des formulaires et les politiques de confidentialité sur les réseaux sociaux - afin de pouvoir proposer des algorithmes et des politiques de protection de la vie privée.