Méthodes inductives et déductives d'analyse quantitative de l'opacité des systèmes communicants

 

Sofiène Tahar

Université Concordia

 

Domaine : technologies de l'information et des communications

Programme projet de recherche en équipe

Concours 2012-2013

Les attaques statistiques contre la confidentialité, l'anonymat et autres propriétés de sécurité des systèmes sont devenues un problème critique. Elles sont basées sur la capacité de l'attaquant d'inférer statistiquement un secret à partir d'observations. Elles illustrent le fait qu'évaluer la sécurité d'un système contre ce type d'attaques est une tâche difficile. Aussi, le développement de méthodes formelles visant à quantifier l'information ainsi inférée est devenu un domaine émergent de la recherche. Une motivation majeure de ce projet est de promouvoir un modèle dans lequel une telle évaluation peut être établie de manière rigoureuse. Ce modèle est celui de l'opacité généralisée aux systèmes de transitions probabilistes. L'opacité est un schéma générique de propriété qui permet de spécifier dans un contexte uniforme de nombreuses propriétés de sécurité. Ce projet vise à définir diverses mesures d'opacité dans ces systèmes de manière à caractériser la quantité d'information secrète qui peut être inférée par un attaquant. Pour ce faire, on propose le développement et l'intégration de méthodes formelles inductives et déductives. La principale contribution de ce projet sera la conception d'un prototype d'un outil d'analyse quantitative intégrant "model checking" et "theorem proving". On illustrera l'applicabilité de notre approche par l'analyse de l'anonymat d'un protocole d'encan électronique, le "Cocaine Auction Protocol". La complexité des requis sécuritaires de ce protocole ont tenu en échec les méthodes d'analyse proposées à ce jour. Ce projet contribua aussi à la formation de quatre personnels hautement qualifiés.