Une nouvelle approche pour la computation multipartite sécurisée en C

Le calcul multipartite sécurisé (SMC) permet à plusieurs personnes de calculer ensemble en utilisant leurs infos privées tout en gardant ces données secrètes les unes des autres. Ce processus est devenu super important dans des domaines comme la santé, l'armée et la finance. Mais écrire des applications SMC peut être compliqué car ça nécessite des techniques de codage avancées pour garantir la sécurité et la justesse.

Bien que pas mal de chercheurs aient bossé pour faciliter l'utilisation du SMC avec des méthodes formelles, la plupart de ces solutions se sont concentrées uniquement sur des langages de programmation spécifiques conçus pour le SMC. Cet article explore une approche générale qui peut être appliquée à des programmes écrits en C, un langage populaire en cryptographie. L'objectif est de créer un modèle qui conserve les caractéristiques clés du C tout en garantissant la sécurité des calculs multipartites.

#Pourquoi utiliser C pour le SMC

Le C est super prisé car il permet une programmation de bas niveau. C'est le seul langage polyvalent avec des compilateurs SMC existants. Ça veut dire que beaucoup de développeurs connaissent déjà le C, ce qui leur facilite l'écriture de programmes multipartites sécurisés. Notre approche se concentre sur des constructions C importantes, comme les branches conditionnelles basées sur des données privées et les pointeurs.

#Défis dans le SMC

Les développeurs font face à plusieurs défis pour maintenir la sécurité et la justesse. Les techniques de bas niveau pour implémenter le SMC, comme le partage secret ou les circuits embrouillés, peuvent mener à un code compliqué. Simplifier le SMC tout en s'assurant que les propriétés de sécurité et de justesse sont préservées est la motivation principale de cet article.

#Aperçu de notre contribution

Notre étude présente un modèle formel qui soutient les aspects clés du langage C pour le SMC. Nous comptons :

• Modéliser des systèmes SMC pour le C, y compris des branches privées, des tableaux mutables et des pointeurs vers des données privées.
• Créer des preuves formelles montrant que les techniques SMC établies garantissent la justesse et une forte non-interférence, ce qui signifie qu'aucune info privée n'est révélée durant les calculs.
• Développer une implémentation de ce modèle formel dans le compilateur SMC existant PICCO et faire un rapport sur sa performance à travers des tests.

#Travaux connexes

Le domaine des compilateurs SMC existe depuis 2004. Beaucoup d'outils ont été développés pour des calculs à deux ou plusieurs parties, mais ils reposent souvent sur des langages personnalisés, ce qui peut limiter leur utilisation. Il y a quelques exceptions, comme le compilateur CBMC-GC qui supporte les programmes C généraux mais qui manque d'une vérification formelle complète de son système de types. Notre recherche vise à combler cette lacune en fournissant un modèle formel pour des compilateurs SMC généraux.

#Les bases du calcul multipartite sécurisé

Le SMC permet à des groupes de participants de collaborer sur des calculs sans divulguer leurs données privées. Ce processus s'appuie souvent sur diverses techniques pour s'assurer que même si certains participants coopèrent pour obtenir des infos, ils ne pourront pas apprendre sur les données privées des autres. Ces méthodes incluent le partage secret, les circuits embrouillés et le chiffrement homomorphe.

#Travailler avec C : caractéristiques clés pour le SMC

Le langage C inclut des caractéristiques comme :

• Pointeurs : qui permettent de référencer et de manipuler des emplacements mémoire.
• Branches conditionnelles : comme les instructions if-else.
• Tableaux mutables : permettant la création et la gestion de structures de données dynamiques.

Ces caractéristiques sont cruciales pour permettre des calculs privés tout en garantissant la justesse.

#Formalisation du modèle SMC

Pour formaliser notre modèle, on définit un état où divers composants comme la mémoire et les variables interagissent selon des règles spécifiques. Chaque participant à un calcul opérera dans son propre environnement et sa mémoire. Au fur et à mesure que les participants s'engagent dans le calcul, ils évalueront une série de transformations basées sur la sémantique définie par notre modèle.

#Modèle d'environnement et de mémoire

Dans notre modèle, on utilise un environnement pour suivre les variables et leurs emplacements mémoire correspondants. Les blocs mémoire contiennent des données, et chaque bloc a des métadonnées, comme des infos de type et des permissions. Cette structure aide à maintenir la confidentialité tout en permettant un traitement efficace des données.

#Gestion de la mémoire : allocation et désallocation

La gestion dynamique de la mémoire est cruciale. Lorsque la mémoire est allouée, elle peut être spécifiquement destinée à des données privées. Des fonctions comme malloc pour les données publiques et pmalloc pour les données privées répondent à ces besoins. Si un emplacement mémoire n'est plus nécessaire, il peut être libéré en utilisant free et pfree, garantissant qu'aucune info privée résiduelle ne puisse être accessible.

#Opérations sur les pointeurs

Les pointeurs introduisent de la complexité. Ils référencent des emplacements mémoire et peuvent être modifiés. Dans notre modèle, on suit les changements de pointeurs pour maintenir la confidentialité des données. Cela garantit que lorsque les emplacements des pointeurs changent, le véritable emplacement reste caché, empêchant ainsi la fuite d'infos sur les données privées.

#Gestion des tableaux : opérations sûres et non sûres

Les tableaux doivent être manipulés avec soin, surtout s'ils contiennent des données privées. Notre modèle établit des règles qui contrôlent comment les tableaux peuvent être accédés et modifiés. Par exemple, écrire au-delà des limites d'un tableau (accès hors limites) peut mener à un comportement indéfini. Notre formalisation s'assure que de telles opérations sont gérées d'une manière qui ne compromet pas la sécurité.

#Non-interférence comme propriété de sécurité

La non-interférence est essentielle pour garantir que les données privées n'influencent pas les sorties publiques. Dans notre modèle formel, on montre spécifiquement que les changements dans les données privées ne révèlent pas d'infos sur ces données aux résultats publics. Cette propriété est critique pour maintenir la confidentialité des entrées privées durant tout le calcul.

#Évaluation des performances

Une fois le modèle implémenté dans le compilateur PICCO, nous avons réalisé des tests de performance en utilisant différents benchmarks pour évaluer l'efficacité. Nous avons observé qu'en minimisant le nombre de communications nécessaires entre les participants, le nouveau modèle pouvait améliorer significativement le temps d'exécution pour les calculs sécurisés.

#Conclusion

Dans cet article, nous avons introduit un modèle formel pour le calcul multipartite sécurisé qui s'intègre efficacement au langage de programmation C. Notre modèle permet d'utiliser toutes les fonctionnalités du C tout en garantissant que les propriétés de sécurité sont préservées. La recherche souligne la nécessité d'approches plus généralisées dans le SMC pour combler le fossé qui existe entre les solutions spécifiques aux langages et la programmation généraliste.

#Travaux futurs

Les améliorations futures à notre modèle pourraient inclure le support pour la déclassification explicite des données, où les données privées peuvent être marquées pour un accès public sous des conditions contrôlées. Nous prévoyons d'étendre notre sémantique pour accueillir cette fonctionnalité, enrichissant encore les capacités des calculs multipartites sécurisés.

En abordant ces domaines, nous visons à contribuer au domaine croissant du calcul sécurisé, le rendant plus accessible et pratique pour une large gamme d'applications dans le monde orienté données d'aujourd'hui.