2025-11-25T11:37:18.016926

Augmenting Smart Contract Decompiler Output through Fine-grained Dependency Analysis and LLM-facilitated Semantic Recovery

Liao, Nan, Gao et al.
Decompiler is a specialized type of reverse engineering tool extensively employed in program analysis tasks, particularly in program comprehension and vulnerability detection. However, current Solidity smart contract decompilers face significant limitations in reconstructing the original source code. In particular, the bottleneck of SOTA decompilers lies in inaccurate method identification, incorrect variable type recovery, and missing contract attributes. These deficiencies hinder downstream tasks and understanding of the program logic. To address these challenges, we propose SmartHalo, a new framework that enhances decompiler output by combining static analysis (SA) and large language models (LLM). SmartHalo leverages the complementary strengths of SA's accuracy in control and data flow analysis and LLM's capability in semantic prediction. More specifically, \system{} constructs a new data structure - Dependency Graph (DG), to extract semantic dependencies via static analysis. Then, it takes DG to create prompts for LLM optimization. Finally, the correctness of LLM outputs is validated through symbolic execution and formal verification. Evaluation on a dataset consisting of 465 randomly selected smart contract methods shows that SmartHalo significantly improves the quality of the decompiled code, compared to SOTA decompilers (e.g., Gigahorse). Notably, integrating GPT-4o with SmartHalo further enhances its performance, achieving precision rates of 87.39% for method boundaries, 90.39% for variable types, and 80.65% for contract attributes.
academic

Augmentation de la sortie du décompilateur de contrats intelligents par analyse des dépendances à grain fin et récupération sémantique facilitée par LLM

Informations de base

  • ID de l'article : 2501.08670
  • Titre : Augmenting Smart Contract Decompiler Output through Fine-grained Dependency Analysis and LLM-facilitated Semantic Recovery
  • Auteurs : Zeqin Liao, Yuhong Nan, Zixu Gao, Henglong Liang, Sicheng Hao, Peifan Ren, Zibin Zheng
  • Classification : cs.SE (Génie logiciel)
  • Date de publication : Janvier 2025 (prépublication arXiv)
  • Lien de l'article : https://arxiv.org/abs/2501.08670

Résumé

Les décompilateurs de contrats intelligents sont des outils d'ingénierie inverse largement utilisés dans l'analyse de programmes, jouant un rôle important notamment dans la compréhension de programmes et la détection de vulnérabilités. Cependant, les décompilateurs actuels de contrats intelligents Solidity présentent des limitations significatives dans la reconstruction du code source original, se manifestant principalement par trois aspects : l'identification imprécise des fonctions, les erreurs de récupération des types de variables et l'absence d'attributs de contrats. Pour résoudre ces défis, cet article propose le cadre SmartHalo, qui combine l'analyse statique (SA) et les modèles de langage de grande taille (LLM) pour améliorer la sortie du décompilateur. SmartHalo exploite la précision de l'analyse statique dans l'analyse des flux de contrôle et de données, ainsi que la capacité des LLM dans la prédiction sémantique. Concrètement, le cadre construit une structure de données de graphe de dépendances (DG) pour extraire les relations de dépendances sémantiques, puis crée des invites LLM optimisées basées sur le DG, et enfin valide la correction de la sortie LLM par exécution symbolique et vérification formelle.

Contexte de recherche et motivation

Définition du problème

La décompilation de contrats intelligents fait face à trois problèmes fondamentaux :

  1. Identification imprécise des limites de fonctions : Les décompilateurs existants ne peuvent pas déterminer précisément les limites des fonctions, fusionnant souvent plusieurs fonctions en une seule ou omettant des fonctions importantes
  2. Erreurs de récupération des types de variables : Les erreurs de type produites par le décompilateur sont incompatibles avec les règles de domaine statique, comme la récupération incorrecte de la valeur de retour bytes32 de la fonction keccak256 en tant que type uint256
  3. Absence d'attributs de contrats : Les variables d'état dans les contrats intelligents enregistrent les attributs critiques des contrats (tels que les actifs, les identités, les routeurs), mais sont complètement absentes du code décompilé

Analyse de l'importance

Ces défauts entravent sérieusement les tâches en aval :

  • Affectent la précision de la détection de vulnérabilités, produisant des faux positifs et des faux négatifs
  • Réduisent l'efficacité de la compréhension de programmes
  • Limitent les tâches d'analyse avancées telles que l'analyse du flux d'appels entre contrats

Limitations des méthodes existantes

  • SmartDagger : Ne peut que partiellement récupérer les attributs de contrats des variables d'état, basé sur des modèles d'apprentissage profond, avec une dégradation des performances sur les nouveaux contrats
  • Neural-FEBI : Ne supporte pas la récupération des limites pour les fonctions avec modificateurs ou fonctions héritées
  • SigRec/VarLifter/DeepInfer : Ne peuvent que partiellement récupérer les types de paramètres des signatures de fonctions connues, dépendant de règles heuristiques prédéfinies avec une couverture faible

Motivation de la recherche

Basée sur deux intuitions clés :

  1. Modèles naturels du logiciel : Les programmeurs tendent à utiliser des structures de code similaires, des attributs de contrats, des types de variables et des limites de fonctions dans des contextes similaires
  2. Amélioration synergique SA-LLM : L'analyse statique offre une haute précision dans le traitement des contraintes statiques complexes, tandis que les LLM offrent une flexibilité dans la prédiction de cibles manquant de contraintes statiques

Contributions principales

  1. Identification et analyse systématique des limitations clés de la sortie des décompilateurs de contrats intelligents actuels
  2. Proposition du cadre SmartHalo, combinant de manière innovante l'analyse statique et les modèles de langage de grande taille pour optimiser la sortie du décompilateur
  3. Conception de la structure de données de graphe de dépendances (DG), extrayant trois types de relations de dépendances sémantiques (dépendances d'état, dépendances de flux de contrôle, dépendances de type)
  4. Établissement d'un mécanisme rigoureux de vérification de correction, utilisant l'exécution symbolique et la vérification formelle pour traiter le problème des hallucinations des LLM
  5. Évaluation complète et validation de l'efficacité de SmartHalo dans la récupération des limites de fonctions, des types de variables et des attributs de contrats

Détails de la méthode

Définition de la tâche

Entrée : Pseudocode généré par le décompilateur Sortie : Code décompilé optimisé, contenant des limites de fonctions précises, des types de variables et des attributs de contrats Contraintes : Maintenir l'équivalence du comportement du programme, respecter les règles de typage statique Solidity

Architecture du modèle

SmartHalo adopte une architecture en trois étapes :

1. Extraction sémantique basée sur les relations de dépendances

  • Analyse du flux de contrôle : Utilisation de Tree-sitter pour construire l'arbre syntaxique, conversion en représentation intermédiaire à trois adresses, génération de graphes de flux de contrôle et de données
  • Identification des relations de dépendances :
    • Dépendances de type : Relations d'association entre les types de variables et d'autres variables ou expressions
    • Dépendances d'état : Relations de lecture-écriture entre variables d'état
    • Dépendances de flux de contrôle : Relations de dépendances des chemins d'exécution du programme
  • Construction du graphe de dépendances : DG = (Nc, Ec, Xe), où Nc est l'ensemble des nœuds (variables et expressions), Ec est l'ensemble des arêtes (trois types de dépendances), Xe est la fonction d'étiquetage

2. Amélioration sémantique pilotée par LLM

  • Génération de contexte de code :
    • Variables : Découpage de code basé sur DG, extraction de fragments de code liés à la variable cible
    • Fonctions : Recherche de la chaîne d'appels contenant la fonction cible
  • Génération de candidats d'inférence :
    • Candidats de type de variable : Types intégrés collectés à partir de la documentation Solidity
    • Candidats d'attributs de contrats : Limit, Fee, Flag, Address, Asset, Router, Others
  • Invites de chaîne de pensée (COT) : Conversion des relations de dépendances dans DG en descriptions d'étapes de raisonnement

3. Vérification de correction

  • Vérification d'équivalence du comportement du programme :
    • Exécution symbolique des fonctions originales et optimisées
    • Vérification formelle utilisant le solveur Z3
    • Assertion d'équivalence : Φ = ¬(s ⇔ s′)
  • Vérification de violation de règles statiques : Détection des erreurs d'inférence de type basée sur les règles de typage Solidity

Points d'innovation technique

  1. Analyse des dépendances à grain fin : Première extraction et utilisation systématique de trois types de relations de dépendances sémantiques
  2. Cadre de collaboration SA-LLM : Combinaison innovante de la précision de l'analyse statique et de la capacité de compréhension sémantique des LLM
  3. Garantie stricte de correction : Assurance de la correction des résultats d'optimisation par exécution symbolique et vérification formelle
  4. Conception universelle : Support pour l'intégration de différents LLM et décompilateurs

Configuration expérimentale

Ensemble de données

  • Ensemble d'évaluation : Sélection aléatoire de 500 fonctions du plus grand ensemble de données de contrats intelligents open-source, obtenant finalement 456 paires de code source et sortie décompilée
  • Ensemble de contrats complexes : Sélection aléatoire de 50 contrats intelligents (environ 900 fonctions) parmi 682 DApps réelles
  • Ensemble de données de détection de vulnérabilités : Contenant 81 étiquettes de vulnérabilités de réentrance, 18 paires de contrats d'attaque, 50 contrats de vulnérabilités de débordement d'entiers

Métriques d'évaluation

  • Correspondance des limites de fonctions : Correspondance complète des points de début et de fin avec les fonctions au niveau du code source
  • Correspondance de type : Correspondance complète du type prédit avec le type réel (y compris la disposition des données et les informations de champs)
  • Correspondance d'attributs de contrats : Correspondance complète de l'attribut prédit avec l'attribut réel
  • Taux d'échec de recompilation : Taux d'erreurs de compilation du code optimisé

Méthodes de comparaison

  • SmartDagger : Comparaison pour la récupération d'attributs de contrats
  • VarLifter : Comparaison pour l'inférence de types de variables
  • Décompilateur original : Gigahorse/Dedaub comme ligne de base

Détails d'implémentation

  • Environnement de développement : Python 3.8.10, 1799 lignes de code
  • Choix de LLM : Utilisation principale de GPT-3.5, support de GPT-4o mini, Llama-3, Deepseek-v3, Qwen-2.5-coder
  • Configuration matérielle : CPU Intel i9-10980XE, GPU RTX 3090, RAM 250GB

Résultats expérimentaux

Résultats principaux

Comparaison d'effet global (avec le décompilateur original)

MétriqueAmélioration de précisionAmélioration de rappel
Identification des limites de fonctions+20.30%+30.03%
Inférence de types de variables+30.02%+42.04%
Récupération d'attributs de contrats68.06%90.93%

Comparaison avec les méthodes SOTA

  • vs SmartDagger (attributs de contrats) : Amélioration de précision de 44.69%, amélioration de rappel de 80.86%
  • vs VarLifter (types de variables) : Amélioration de précision de 13.51%, amélioration de rappel de 77.08%

Comparaison de performance entre différents LLM

LLMLimites de fonctions(P/R)Types de variables(P/R)Attributs de contrats(P/R)
GPT-3.588.26%/80.51%92.27%/84.26%68.06%/90.93%
GPT-4o mini91.32%/87.38%90.40%/88.82%80.66%/91.78%
Llama-366.09%/55.11%62.41%/48.53%61.68%/60.34%

Études d'ablation

Comparaison entre l'utilisation isolée de SA, LLM et le cadre complet SmartHalo :

  • Contribution de SA : Fourniture d'extraction précise des relations de dépendances et vérification des contraintes
  • Contribution de LLM : Fourniture de compréhension sémantique et capacité de reconnaissance de modèles rares
  • Effet synergique : SmartHalo améliore de 19.23%/29.23% par rapport à l'utilisation isolée de LLM sur les limites de fonctions

Vérification de la capacité de généralisation

  • Entre décompilateurs : Améliorations significatives sur Heimdall, Panoramix
  • Contrats complexes : Maintien de bonnes performances sur les DApps réelles complexes
  • Analyse d'efficacité : Temps de traitement moyen 23.99 secondes, coût $0.00136/fonction

Effets sur les tâches en aval

  • Détection de vulnérabilités de réentrance : Précision améliorée de 72.16% à 80.41%
  • Identification d'attaques : Rappel amélioré de 83.33% à 100.00%
  • Détection de débordement d'entiers : Amélioration de précision de 21.96%, amélioration de rappel de 38.00%

Travaux connexes

Décompilation de contrats intelligents

  • Gigahorse/Elipmoc : Conversion du bytecode EVM en représentation de code à trois adresses
  • Erays/EtherSolve : Récupération du graphe de flux de contrôle à partir du bytecode EVM
  • SigRec/DeepInfer : Récupération des signatures de fonctions publiques

Optimisation de décompilation

  • Récupération d'informations sémantiques : DEBIN, OSPREY, BDA et autres récupèrent les dépendances de programmes par analyse statique
  • Optimisation de noms et types de variables : DIRE, DIRTY, DeGPT et autres utilisent l'apprentissage profond pour optimiser la sortie du décompilateur

Avantages de cet article

Comparé aux travaux existants, SmartHalo offre :

  1. Objectifs d'optimisation plus complets : Traitement simultané des limites de fonctions, des types de variables et des attributs de contrats
  2. Capacité de généralisation plus forte : Indépendant des données d'entraînement spécifiques, adaptation aux nouveaux contrats
  3. Garanties de correction strictes : Assurance de la correction des résultats d'optimisation par vérification formelle

Conclusion et discussion

Conclusions principales

  1. SmartHalo améliore significativement la qualité de la décompilation de contrats intelligents, réalisant des améliorations substantielles sur les trois indicateurs clés
  2. Le cadre de collaboration SA-LLM s'avère efficace, exploitant pleinement les avantages complémentaires des deux approches
  3. Le mécanisme rigoureux de vérification de correction contrôle avec succès le problème des hallucinations des LLM
  4. Le cadre possède une bonne capacité de généralisation, supportant plusieurs LLM et décompilateurs

Limitations

  1. Récupération des structures d'héritage : Impossible de récupérer les relations d'héritage au sein des contrats, car les informations de classe manquent au niveau du bytecode
  2. Taille de l'ensemble de données : L'ensemble de données d'évaluation est relativement petit (456 fonctions), mais comparable à la taille des recherches SOTA
  3. Évolution de l'API LLM : Peut affecter la reproductibilité des résultats
  4. Traitement de scénarios complexes : Performances limitées dans les scénarios d'appels de bas niveau, d'assemblage en ligne, de dépendances hors chaîne

Directions futures

  1. Récupération des structures d'héritage : Exploration du raisonnement des relations d'héritage basé sur la correspondance de modèles
  2. Évaluation à plus grande échelle : Validation de la robustesse de la méthode sur des ensembles de données plus grands
  3. Entraînement de modèles spécialisés : Entraînement de modèles spécialisés pour la compréhension de contrats intelligents
  4. Optimisation en temps réel : Support pour l'optimisation de décompilation en ligne

Évaluation approfondie

Points forts

  1. Définition claire du problème : Identification et analyse systématiques des problèmes fondamentaux de la décompilation de contrats intelligents
  2. Forte innovativité de la méthode : Première proposition d'un cadre de collaboration SA-LLM, conception ingénieuse de la structure de données de graphe de dépendances
  3. Solution technique complète : Formation d'une boucle fermée complète allant de l'extraction sémantique, l'amélioration de l'optimisation à la vérification de correction
  4. Évaluation expérimentale complète : Expériences de comparaison multidimensionnelles, incluant études d'ablation et validation de tâches en aval
  5. Valeur pratique élevée : 60.22% du code optimisé peut être directement recompilé, améliorant significativement l'utilité pratique

Insuffisances

  1. Analyse théorique insuffisante : Manque d'analyse approfondie des garanties théoriques de la méthode
  2. Analyse d'erreurs limitée : L'analyse des causes profondes des cas d'échec d'optimisation pourrait être plus approfondie
  3. Surcharge de calcul : L'exécution symbolique et la vérification formelle peuvent entraîner des coûts de calcul élevés
  4. Dépendance aux outils externes : Dépendance de la qualité des décompilateurs existants et des API LLM

Impact

  1. Contribution académique : Fournit un nouveau paradigme de recherche pour le domaine de l'analyse de contrats intelligents
  2. Valeur pratique : Peut être directement appliqué à l'audit de sécurité et à la compréhension de programmes de contrats intelligents
  3. Extensibilité : La conception du cadre supporte l'intégration de différents outils d'analyse et modèles
  4. Contribution open-source : Les auteurs s'engagent à rendre le code et les ensembles de données open-source, facilitant la reproduction de la recherche

Scénarios d'application

  1. Audit de sécurité de contrats intelligents : Amélioration de la lisibilité et de la précision du code décompilé
  2. Outils de détection de vulnérabilités : Utilisation comme étape de prétraitement pour améliorer la précision de la détection
  3. Outils de compréhension de programmes : Assistance aux développeurs dans la compréhension de la logique des contrats tiers
  4. Recherche académique : Fourniture de données de haute qualité pour la recherche en analyse de contrats intelligents

Références bibliographiques

L'article cite 96 références connexes, incluant principalement :

  • Analyse de contrats intelligents : Travaux classiques tels que Gigahorse, SmartDagger, VarLifter
  • Théorie de l'analyse de programmes : Littérature sur l'exécution symbolique et la vérification formelle
  • Application du machine learning : Application de l'apprentissage profond dans l'analyse de programmes
  • Techniques de décompilation : Méthodes et outils d'optimisation de décompilation traditionnels

Évaluation globale : Ceci est un article de recherche en génie logiciel de haute qualité, proposant une solution innovante à un problème important de décompilation de contrats intelligents. La conception de la méthode est raisonnable, l'évaluation expérimentale est suffisante, et la valeur pratique est remarquable. Bien qu'il existe certaines limitations, la contribution globale est significative et exerce un impact important sur le domaine de l'analyse de sécurité des contrats intelligents.