A l'occasion de la tenue des Assises nationales de la recherche en novembre 2007, l'Association tunisienne de la sécurité numérique (ATSN), présidée par le Dr Adel BOUHOULA*, a organisé, mercredi 24 octobre 2007, à la Cité Technologique des Communications, en collaboration avec l'Ecole supérieure des communications de Tunis et l'Institut national de recherche en informatique et automatique en France (INRIA), un workshop internatio nal sur le thème «Méthodes formelles pour la Sécurité des Systèmes et Réseaux », avec la participation de conférenciers professeurs et chercheurs de l'INRIA Futurs, de l'Université de Bordeaux et de l'Institut de Technologie de Tokyo. Le choix de ce thème s'inscrit dans le cadre des orientations présidentielles relatives au développement des associations permettant la vulgarisation de la culture numérique, vu leur contribution à l'essor de la Société de l'information, a expliqué Dr Bouhoula, maître de conférences à Sup'Com et président de l'ATSN Dr BOUHOULA, dans une allocution introductive. Le président de l'ASTN y a également précisé que l'association veut, à travers l'organisation de cette manifestation, valoriser davantage l'intelligence et la haute qualification des cadres tunisiens dans le domaine des technologies de l'information et de la communication. Dr BOUHOULA a ajouté que l'Association tunisienne de la sécurité numérique, de création récente, s'est fixé un programme ambitieux dans le but de réunir le plus grand nombre de compétences dans ce domaine des technologies de pointe, facilitant ainsi l'instauration d'une synergie fructueuse entre les différents facteurs d'incitation à l'innovation technologique. Le président de l'ASTN a ajouté que la sécurité numérique, d'une manière générale, est extrêmement complexe. Certifier un système d'information, un protocole, une carte à puce, ne peut pas se faire à la main et la moindre erreur peut être lourde de conséquence. C'est pour cette raison que les méthodes formelles, qui offrent la possibilité d'automatiser ce type de vérification, attirent aujourd'hui le monde de la recherche et même un grand nombre d'industriels. La conception de systèmes d'authentification réputés sûrs dans le domaine du paiement électronique par cartes et plus généralement des transactions bancaires, de la téléphonie mobile ou de la signature de documents, dépend des protocoles d'authentification utilisés. Ces protocoles sont de courts programmes d'échanges de messages partiellement chiffrés par lesquels des agents s'identifient mutuellement. Dr BOUHOULA a expliqué que lors de la conception des protocoles cryptographiques d'authentification, on admet toujours la présence des intrus qui ont un contrôle total sur les canaux de communications: un intrus est capable de lire, de modifier, d'intercepter, de créer et d'envoyer des messages. Un intrus est capable de réaliser toutes les opérations disponibles, tels que le chiffrement et le déchiffrement. Cette hypothèse rend la conception des protocoles cryptographiques une tâche difficile et très complexe, puisqu'un intrus peut par exemple détourner les messages chiffrés et les faire décrypter par d'autres suivant une combinaison astucieuse d'exécutions du protocole. Au cours de ces dernières années, de nombreux protocoles d'authentification se sont révélés défaillants, longtemps après leur utilisation, indépendamment des fonctions de chiffrement utilisées. Ainsi, le protocole d'authentification «Needham-Schroeder» a été considéré comme sûr pendant 17 ans et le protocole RSA, fondé sur le chiffrement par clés publiques, est connu pour être sujet à une variété d'attaques. Si pour des protocoles simples il est possible de construire une attaque à la main, pour les protocoles de nouvelle génération développés par VISA ou Mastercard, il est indispensable d'utiliser des systèmes basés sur des méthodes formelles. Durant cet atelier, Dr Florent JACQUEMARD, chercheur à l'INRIA, a présenté des travaux menés avec Dr Adel BOUHOULA et portant sur l'application à la vérification de protocoles de sécurité d'une méthode de preuve formelle. Cette méthode vise à automatiser des preuves par récurrence et, dans le cadre des protocoles, permet d'établir formellement la fiabilité d'un protocole, ou bien inversement, de dériver un contre-exemple, c'est-à-dire une attaque, qu'il conviendra de corriger. Ce travail a été réalisé dans le cadre du projet INRIA/DGRSRT 06/I09. Dr Olivier LY, Maître de Conférences à l'Université de Bordeaux, a exposé les résultats les plus récents travaux sur la Certification Sécuritaire dans le Contexte des Cartes à Puce et notamment sur les attaques par canaux cachés. Le problème de sécurité dans le cadre des systèmes distribués a été ensuite présenté par le Professeur Mohamed MOSBAH de l'Université de Bordeaux. Il a précisé en particulier que dès que nous nous connectons au réseau Internet, par exemple, nous interagissons avec d'autres ordinateurs, dont le nombre peut atteindre des millions en même temps ! Pour qu'un si grand nombre de machines puissent coopérer et que le réseau réalise une tâche donnée, comme diffuser une information, collecter des informations, détecter et auto-corriger une panne, maintenir la cohérence des données distribuées, il faut mettre au point des modèles très poussés. Mohamed MOSBAH s'intéresse par exemple aux virus. Chacun peut bien sûr installer un antivirus sur son ordinateur mais c'est une solution de protection individuelle qui ne permet pas résoudre ce problème sur le réseau. Ce chercheur crée des agents-robots, qui se baladent de machine en machine pour traquer les virus et les détruire. Professeur Mohamed MOSBAH dispose d'une plate-forme de simulation qui lui permet d'expérimenter ces robots et de retenir les solutions les plus performantes. Cet enseignant participe à plusieurs projets de coopération entre cette institution et des universités tunisiennes ; et co-encadre des thèses en cotutelle sur ces thèmes. En particulier, il co-encadre avec le Dr. Adel BOUHOULA une thèse sur la sécurité des systèmes distribués utilisant une approche langage dans le cadre d'une thèse en cotutelle entre l'Université de Bordeaux et Sup'com (Université du 7 Novembre à Carthage). Dr. Skander Hannachi, chercheur associé à l'Institut de Technologie de Tokyo, a parlé des algorithmes quantiques et de la possibilité de les simuler à travers la logique floue. Après un bref rappel de la mécanique quantique, suivi d'une introduction de l'informatique quantique et une explication de ses principaux résultats, professeur Hannachi a donné un aperçu sur la possibilité de simuler les algorithmes quantiques avec la logique floue en utilisant le concept des «fuzzy qubits». Finalement, il a parlé de la possibilité de simuler d'autres types d'algorithmes parallèles avec la logique floue. ---------------- * Ingénieur en informatique, diplômé (major de la promotion 1990) de la Faculté des Sciences de Tunis (il est aussi titulaire d'un DEA, d'un Doctorat (mention très honorable avec les félicitations du jury et d'une Habilitation à diriger des Recherches en informatique de l'Université Henri Poincaré de Nancy France), Adel BOUHOULA, détenteur d'un brevet européen, travaille en particulier sur la démonstration automatique, la certification des logiciels de télécommunications, la cryptographie et la sécurité des systèmes d'information et des réseaux. Des sujets qui ont fait l'objet de 9 publications dans des revues internationales et plus d'une soixantaine de publications dans des conférences et workshops internationaux, et d'interventions dans des séminaires dans plusieurs laboratoires et universités, notamment en France, en Grande-Bretagne, en Italie, en Allemagne, en Russie, en Australie, au Canada, aux USA et au Japon.
