Les sémantiques formelles des contrats intelligents sur blockchain constituent la base de la vérification formelle. Elles peuvent être utilisées pour établir des modèles formels afin de vérifier la sécurité des contrats et aider les développeurs à comprendre les règles d'exécution spécifiques des contrats. Cependant, la logique mathématique impliquée dans ce type de modélisation pose une barrière d'entrée élevée et ne peut pas être intégrée directement avec d'autres méthodes d'analyse de programmes. Cet article propose une approche de génération de graphes sémantiques, KSG, pour les contrats intelligents sur blockchain. Tout d'abord, les règles sémantiques du langage des contrats sont formellement définies, et un interprète sémantique et un prouveur sont construits pour transformer automatiquement le code des contrats intelligents en un graphe sémantique évolutif. Ce graphe incorpore des informations sur le flux de contrôle sémantique, le flux de données sémantique, les règles d'exécution et les contraintes de vérification. Ensuite, le graphe sémantique généré peut être utilisé pour la détection de vulnérabilités et l'exécution symbolique, et prend en charge l'optimisation itérative basée sur les résultats d'analyse. Enfin, le processus détaillé de génération et d'analyse de graphes sémantiques est démontré à travers la vérification du contrat de réentrance et du contrat de leurre.
Li et al. (ven,) ont étudié cette question.