Par Grigore Rosu, Everett Hildenbrandt, Daejun Park, Shuvendu Lahiri
« Les tests montrent la présence, pas l'absence de bugs » (Dijkstra, 1969). Bien que des progrès remarquables aient été réalisés dans le domaine des tests au cours des 50 dernières années, les tests exhaustifs restent encore irréalisables dans la plupart des cas et nous avons appris, parfois à nos dépens, que les bugs restants peuvent avoir des conséquences catastrophiques.
La nature de la blockchain, où le code qui accède à un état partagé est public et peut être invoqué par quiconque depuis n'importe où, amplifie à la fois la rapidité avec laquelle les hackers trouvent des bugs et les conséquences de leurs exploits. Les tests sont donc tout simplement insuffisants ici. La vérification formelle est la seule alternative viable connue.
Cette présentation expliquera ce qu'est la vérification formelle dans le contexte des contrats intelligents, des tokens et des protocoles blockchain, pourquoi elle devient de plus en plus critique, comment elle est réalisée et quels outils sont disponibles. Plusieurs approches sont couvertes, des méthodes automatisées et légères qui trouvent des bugs aux méthodes interactives et complètes qui analysent tous les comportements, du code source de haut niveau que les développeurs écrivent et comprennent au bytecode de bas niveau qui est exécuté par les clients de nœud.
Cette présentation vise également à sensibiliser le public au fait que, contrairement à une idée reçue où la vérification formelle est confondue avec l'audit de code, il faut beaucoup plus d'efforts pour vérifier formellement un programme que pour écrire le programme en premier lieu. Pensez à 9 fois plus ! En effet, une règle empirique à la NASA est que 20 % du budget d'un projet est consacré à l'écriture de code et 80 % à la vérification et à la validation ; et le code de la NASA n'est pas public et personne d'autre que la NASA ne peut l'invoquer une fois déployé.