TechFlow, une société de sécurité blockchain, a récemment mené une revue formelle de vérification des extensions de jetons Solana à l’aide de ses outils avancés de vérification formelle pour spécifier et valider les propriétés critiques du code. Les principales découvertes de l’équipe Certora incluent : l’identification d’une opportunité d’optimisation permettant d’améliorer les performances du programme de 20 % ; le développement de règles de vérification pour les mises à jour récentes de l’équipe Solana afin de renforcer les mesures de sécurité existantes ; ainsi que la rédaction de spécifications réutilisables permettant de vérifier plusieurs instructions, mettant au jour un problème passé inaperçu lors de toutes les audits précédents.
Plus précisément, Certora recommande de ne pas utiliser sol_memcmp, mais d’adopter à la place la méthode de comparaison indépendante de la plateforme fournie par Rust, amélioration qui réduit d’environ 20 % les unités de calcul de l’instruction TransferChecked.
Par ailleurs, la vérification effectuée par Certora a permis de découvrir et de confirmer la correction d’un problème relatif à la cohérence entre les transferts vérifiés et non vérifiés.
Enfin, l’équipe a constaté que la correction mise en œuvre pour les instructions de transfert faisait défaut dans les instructions de brûlage (Burn et BurnChecked). Ce problème a été confirmé puis corrigé par les développeurs SPL.
