La vérification formelle est fondamentale en ingénierie logicielle pour garantir la correction des programmes grâce à des preuves mathématiques. Une technique couramment utilisée est la vérification de modèle borné (BMC), qui vérifie la justesse d’un programme dans des limites spécifiées. Python, apprécié pour sa simplicité et ses bibliothèques vastes, présente des défis uniques pour la vérification formelle en raison de sa nature dynamique et de l’absence d’informations de type explicites.
Les outils de vérification statique traditionnels peinent avec Python puisque ce dernier détermine les types à l’exécution. Sans annotations de type explicites, assurer la sécurité et la justesse des programmes Python, en particulier ceux touchant à des exigences critiques de sécurité, devient ardu. Cette difficulté s’accentue dans les grandes bases de code ou les applications où sécurité et fiabilité sont cruciales.
Des chercheurs de l’Université de Manchester et de TPV Technology ont introduit ESBMC-Python, un nouvel outil conçu pour vérifier les programmes Python. ESBMC-Python utilise le cadre ESBMC, un vérificateur de modèle borné basé sur SMT, pour vérifier formellement le code Python. Cet outil convertit les programmes Python en arbres de syntaxe abstraite (AST), ensuite annotés par types et formatés pour s’intégrer dans la chaîne de BMC. Cela permet de surmonter les difficultés posées par la typage dynamique de Python.
ESBMC-Python commence par analyser le code source Python pour générer un AST. Cet AST est ensuite annoté avec des informations de type, cruciales pour les étapes suivantes. L’AST annoté est traduit en une représentation intermédiaire que le cadre ESBMC peut traiter. Cette conversion implique la traduction des expressions et instructions Python en symboles adaptés à la structure de vérification de modèle du ESBMC. L’outil traite efficacement les fonctionnalités dynamiques de Python en les convertissant dans un format approprié pour la chaîne BMC, permettant de vérifier des propriétés comme la correction de type et la cohérence logique.
Les performances d’ESBMC-Python ont été rigoureusement évaluées avec une suite de 85 programmes Python couvrant de nombreuses fonctionnalités des applications Python réelles, comme des opérations arithmétiques, des conditionnelles, des boucles, des assertions utilisateur, des opérations bit à bit, des classes, de l’héritage et du polymorphisme. Les résultats d’évaluation sont impressionnants avec des temps de vérification moyens allant de 24,5 millisecondes à 49,1 millisecondes et une utilisation de mémoire entre 14,5 et 26,4 mégaoctets. Ces chiffres indiquent qu’ESBMC-Python est efficace et peut gérer de grandes bases de code et des ensembles de programmes étendus en périodes relativement courtes.
Un des succès remarquables d’ESBMC-Python a été d’identifier une erreur critique de division par zéro dans la spécification de consensus Ethereum. Cette spécification contrôle l’inclusion de nœuds, la validation et les processus de pénalité des validateurs de la blockchain Ethereum. L’erreur impliquait un dépassement d’entier non signé à zéro puis utilisé comme diviseur, ce qui aurait pu provoquer d’importantes interruptions de service et des vulnérabilités potentielles dans le réseau blockchain. L’identification réussie et la correction de cette erreur par ESBMC-Python soulignent son utilité pratique et son efficacité dans les applications réelles.
En conclusion, la capacité d’ESBMC-Python à identifier des erreurs critiques, comme celle dans la spécification de consensus Ethereum, met en lumière sa pertinence pratique et sa fiabilité. Cet outil assure la sécurité et la justesse des programmes Python et constitue un précieux repère pour les futurs outils de vérification. L’équipe de recherche envisage d’étendre les capacités d’ESBMC-Python en incluant davantage de fonctionnalités et en améliorant l’algorithme d’inférence de types pour gérer des flux de programmes plus complexes.