| La question qui consiste à savoir si un logiciel, ou tout bout de code exécutable, est sécuritaire, revêt beaucoup d'importance de nos jours, notamment avec l'usage accru du code mobile et des réseaux comme Internet. Comme complément aux méthodes traditionnelles d'analyse statique et dynamique, on propose ici le code auto-certifié par typage pour assurer la sûreté (intégrité de la mémoire, de la pile, etc.) d'un programme écrit en langage ANSI C et exécuté par un consommateur qui ne fait pas nécessairement confiance au producteur qui l'a compilé: un compilateur-certificateur adjoint des annotations de types au code compilé puis un vérificateur analyse le tout pour assurer la sûreté du code. En s'inspirant d'autres travaux de recherche, on développe un compilateur-certificateur et un vérificateur pour appliquer ces principes au langage C et actuellement, une bonne partie du langage est typée est vérifiée, bien qu'on ne couvre pas encore entièrement ANSI C. |
