|
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.
|
