Aujourd'hui le numérique s'installe dans toutes nos actions au quotidien, notamment pour la communication, l’échange des données, le contrôle d'accès, mais également la santé, la vie sociale et professionnelle. Pour garantir leur bon fonctionnement, toutes ces activités sont protégées par des protocoles cryptographiques.
Lorsque deux, ou plus, participants (objets connectés, ordinateurs, serveurs, systèmes, personnes, etc.) veulent communiquer,ils utilisent des protocoles. Le rôle des protocoles est d'échanger des messages entre ces participants afin de s'assurer qu'une propriété de sécurité souhaitée (confidentialité, authenticité, intégrité, etc.) est satisfaite.
Il est donc primordial d'être en capacité de vérifier que tous ces protocoles satisfont bien les propriétés de sécurité annoncées. C'est un travail très minutieux et long, bien qu'il existe des outils de vérification pour aider les spécialistes en sécurité, dans cette tâche.
Ces outils ne sont pas complets: pour certains protocoles, ils peuvent ne pas être concluant, car le problème de vérification de protocoles est en général non-décidable. C'est là que Cyclos intervient.
Cyclos est un logiciel qui permet de faire une pré-sélection en amont des outils de vérification existants, et évite ainsi la perte de temps engendrée par le test de protocoles de sécurité dont la vérification n'est pas concluante. Il existe en effet une classe de protocoles pour lesquels la vérification est décidable. L’objectif de Cyclos est de déterminer si le protocole appartient à cette classe ou non.
Avec Cyclos soyez sûr d’obtenir un résultat !
Des morceaux des messages échangés dans le protocole peuvent être reconstruits par un attaquant, en se basant sur les informations publiques qu’il est capable de récupérer. Ces liens possibles entre les informations récupérées et reconstruites sont appelés des dépendances, et elles forment ce qu'on appelle un graphe de dépendances.Les graphes de dépendances des protocoles dont la vérification est décidable sont acycliques. Démarche de Cyclos : créer le graphe de dépendance d’un protocole afin de tester s’il est acyclique.
En savoir plus !
Cyclos est une application Python et, pour profiter des spécificités de ce langage, elle utilise quelques librairies.
L'application est intégralement codée dans le langage Python.
Lark est un parser que l'on utilise pour lire les protocoles en entrée du programme.
NetworkX est une librairie permettant de gérer des graphes en Python, nous l'utilisons pour l'affichage et pour divers traitements.
Matplotlib est utilisé en complément avec NetworkX pour, entre autres, gérer l'affichage de ses graphes.
Pour assurer l'intégration continue de l'application, des tests unitaires sont indispensables. C'est ce qu'Unittest permet de faire en Python.
Qt est une bibliothèque largement répandue et compatible avec Python, que l'on utilise pour gérer l'affichage de notre IHM.
PySide est l'indispensable librairie qui nous permet de connecter Qt à Python.
Un groupe de 7 étudiants de l'INSA Rennes est en charge de ce projet pour l'année 2019/2020.
Nowadays, digital aspects are present in all of our daily activities: communication, data exchange, access control, and also health, social and professional life.
In order to ensure their good functionality, all these activities are protected by cryptographic protocols that exchange messages between the participants (computers, servers, smart devices, humans, etc.) and ensure that a required security property (for instance, confidentiality, authentication, integrity) is satisfied.
It is therefore crucial to be able to check whether a protocol satisfies a required security property. This, might be a long and meticulous process, so there exist some tools automating this task.
These tools however are not complete: for some protocols, they may provide no conclusive answer, because the problem of protocol verification is in general undecidable. This is where Cyclos comes into play.
Cyclos is computer software whose goal is to make a preliminary selection, and discard protocols whose verification is not conclusive. It thus allows to save time that would be spent on their analysis. Although, this is not the case in general, there exists a class of protocols for which the verification is decidable. The objective of Cyclos is to determine whether the protocol belongs to this class or not.
With Cyclos be sure to get a result!
By observing an execution of a protocol, an attacker can reconstruct parts of some messages using public data. The dependencies between public and reconstructed data can be represented in a form of a graph, called dependency graph. The protocols whose verification is decidable give rise to dependency graphs that are acyclic. Cyclos procedure: construct a protocol's dependency graph and determine whether it is acyclic.
Find out more !
Cyclos is a Python application and, to take advantage of the specificities of this language, it uses some libraries.
The application is made in Python.
Lark is a parser that is used to read the protocols at the input of the program..
NetworkX is a library to manage graphs in Python, we use it for display and various processing.
Matplotlib is used in conjunction with NetworkX to, among other things, manage the display of its graphs.
To ensure the continuous integration of the application, unit tests are essential. This is what Unittest allows to do in Python.
Qt is a widely used Python-compatible library used for manage the display of our HMI.
PySide is the indispensable library that allows us to connect Qt to Python.
A group of 7 students from INSA Rennes is in charge of this project during the year 2019/2020.