Securite logicielle et detection de code malicieux par model-checking

La sécurité informatique est un sujet chaud et plusieurs organisations en ont récemment fait une priorité. L'augmentation rapide des coûts engendrés par les attaques de codes malicieux, qui ont atteint plus de 17 milliards de dollars (USD) en 2000, est la cause principale de toute cette agitation. Notre société est devenue très dépendante de systèmes informatique et logiciels de toutes sortes. La complexité croissante, les impératifs de productivité imposés par le marché ainsi que l'avènement d'Internat ont eu des effets importants sur le niveau de qualité de ces logiciels et sur les problèmes causés par les failles de sécurité qu'ils contiennent.;Le principal objectif de cette recherche est l'élaboration de méthodes et d'outils pratiques, fondés sur des aspects théoriques robustes, pour la certification de composantes logicielles. Le projet SPCheck a conduit à l'élaboration d'un langage de spécification de propriétés de sécurité, basé sur le mu-calcul modal, ainsi qu'à l'implantation d'un environnement de vérification de logiciels utilisant le model-checking.