Une synergie entre les méthodes formelles et la sécurité informatique

点击翻译按钮获取中文摘要

Depuis l'avènement de Internet, la liste d'intrusions dans les systèmes informatiques et des  vols  d'information  via  ce  réseau ne cesse de s'allonger. Internet a non seulement donné une   parfaite vitrine aux commerçants du monde entier qui y trouvent l'occasion de profiter  d'un marché virtuel  mondial,  mais a aussi suscité de nombreuses idées chez tous ceux qui cherchent de l'argent facile et ceux qui trouvent un grand plaisir à saccager les sites informatiques des autres.  Il  est par  ailleurs  très inquiétant de savoir qu'une faille, aussi infime soit-elle, dans un protocole de communication   ou  dans  n'importe  quel  autre  logiciel  peut  engendrer  des  conséquences  très indésirables et parfois catastrophiques et irréversibles tant sur le plan humain  que  sur  le  plan financier.  Bien  que  l'ampleur  du  danger  soit  souvent connu d'avance, nous n'avons pas réussi à maintes reprises d'empêcher l'indésirable de se produire, et ce malgré la présence de la volonté  et des  moyens.  Ceci est dû souvent, d'un côté, à la subtilité et la complexité des problèmes auxquels nous en faisons face et d'un autre côté à l'absence de méthodes formelles bien  établies  permettant de  garantir  la  correction  de nos logiciels. Les protocoles de commerce électronique qui sont par exemple   utilisés   pour   répondre   à   des  besoins  sécuritaires  (confidentialité,  intégrité, authentification, non-répudiation, anonymat, atomicité des biens  et  de  l'argent,  etc.)  ont  été souvent conçus par des spécialistes dans le domaine. Cependant, nombreux sont les protocoles qui ont été démontrés défaillants plusieurs années après leur utilisation.     L'objectif de la recherche ci-proposée  consiste  à  établir  une  synergie  harmonieuse  entre  les méthodes formelles du génie logiciel et la sécurité informatique, et ce d'un côté pour la conception de protocoles de commerce électronique sans failles et d'un autre côté pour garantir, dans la mesure de  possible,  qu'un  programme  ne  viole  pas une politique de sécurité donnée.