Code auto-certifie par typage: Detection de code malicieux dans les programmes ANSI C (French text).
详细信息
文摘
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.