💻 computer science

Chiral Analysis of Smart Contracts: Detecting Vulnerabilities from Relational Inconsistencies Across Business Paths

Ce document introduit l'« analyse chirale », un modèle d'analyse statique relationnelle implémenté dans l'outil ChiralDetector qui détecte les vulnérabilités des contrats intelligents en identifiant les incohérences entre des chemins métier sémantiquement appariés, révélant ainsi efficacement des bogues de logique complexes que les analyseurs traditionnels à fonction unique ne parviennent pas à détecter.

Auteurs originaux : Yue Xue

Publié 2026-07-21

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yue Xue

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le dilemme du détective : quand le code ment par omission

Imaginez que vous êtes un détective tentant de résoudre un mystère dans une ville bouillonnante. Habituellement, vous cherchez une arme du crime : une fenêtre brisée, une empreinte de pas boueuse ou une note suspecte. Dans le monde du code informatique, plus précisément des « smart contracts » qui font fonctionner les blockchains, les outils de sécurité traditionnels agissent comme ce détective. Ils scannent le code ligne par ligne, à la recherche d'erreurs évidentes comme une serrure manquante sur une porte ou une erreur de calcul mathématique. Ces outils sont excellents pour trouver des bugs « locaux » — ceux qui se produisent dans une seule pièce.

Mais et si le crime ne se trouvait pas du tout dans la pièce ? Et si le mystère était que la porte d'entrée est verrouillée, mais que la porte arrière est grande ouverte, et que les deux portes étaient censées faire partie du même système de sécurité ? En informatique, c'est ce qu'on appelle un problème « relationnel ». Il ne s'agit pas d'une pièce cassée, mais de deux pièces qui devraient correspondre mais ne le font pas. Ce document explore une nouvelle façon de débusquer ces bugs sournois en comparant des paires de chemins de code, en les traitant comme des images miroirs qui doivent refléter la même vérité. Si un chemin dit « stop » et l'autre dit « go », le système est défectueux, même si « stop » et « go » semblent parfaitement corrects individuellement.

L'article : Analyse chirale et le test du miroir

Cet article présente une nouvelle méthode ingénieuse appelée Analyse chirale. Le mot « chiral » vient de la chimie et décrit des objets qui sont l'image l'un de l'autre dans un miroir mais qui ne peuvent pas être parfaitement superposés (comme votre main gauche et votre main droite). Dans le monde des smart contracts, les auteurs proposent que de nombreuses opérations commerciales viennent par paires : un échange « simple » et un échange « par lot », un « achat » et une « vente », ou un « aperçu » d'un prix et l'« exécution » de ce prix. Ces paires sont les jumeaux chiraux du code.

L'idée centrale est simple mais puissante : traiter ces paires comme si elles vérifiaient les devoirs de l'autre. Si un utilisateur achète un article, le code doit lui facturer des frais. Si ce même utilisateur vend l'article plus tard, le code doit gérer l'argent d'une manière cohérente avec l'achat original. Si le chemin d'« achat » facture des frais en dollars, mais que le chemin de « vente » rembourse accidentellement dans une devise différente, ou si la version « par lot » oublie de rembourser l'argent que la version « simple » restitue, un bug existe. L'article soutient que ces bugs sont invisibles pour les scanners standards car chaque ligne de code individuelle semble correcte. L'erreur n'apparaît que lorsque vous tenez les deux chemins face au miroir et constatez qu'ils ne correspondent pas.

Pour trouver ces erreurs invisibles, les auteurs ont construit un prototype d'outil appelé ChiralDetector. Voyez cet outil comme un stagiaire super intelligent qui a une fiche de poste spécifique. D'abord, il lit l'ensemble du code source et cartographie chaque « chemin métier » possible (comme tracer chaque itinéraire qu'un client peut emprunter dans un magasin). Ensuite, il utilise un « classificateur statique » — un ensemble de règles simples — pour deviner quels chemins pourraient être des jumeaux chiraux. Par exemple, il pourrait chercher une fonction nommée buy et une autre nommée sell qui touchent le même compte bancaire.

Une fois qu'il a une liste de jumeaux potentiels, il fait appel au poids lourd : un Modèle de Langage Étendu (LLM), un type d'IA qui comprend le langage humain et le code. L'IA ne se contente pas de chercher des erreurs ; elle agit comme un logicien. Elle demande : « Si ces deux chemins sont censés être des miroirs, quelles règles doivent-ils suivre ? » Elle vérifie sept dimensions spécifiques :

Garde (Guards) : Les deux chemins ont-ils vérifié les mêmes mots de passe ou permissions ?
Acteurs (Actors) : La même personne a-t-elle payé et reçu de l'argent dans les deux cas ?
État (State) : Les deux chemins ont-ils mis à jour la base de données de la même manière ?
Valeur (Value) : Ont-ils géré les frais et les remboursements de manière cohérente ?
Ordre (Order) : Ont-ils effectué les choses dans la même séquence ?
Échec (Failure) : Si les choses tournent mal, est-ce que les deux chemins plantent ou se rétablissent de la même façon ?
Externe (External) : Ont-ils fait confiance aux mêmes sources externes ?

Si l'IA trouve une discordance, elle ne se contente pas de crier « Bug ! » immédiatement. Elle transmet sa découverte à un « validateur strict ». Ce validateur est un éditeur sceptique qui tente de prouver que l'IA a tort. Il demande : « Est-ce vraiment un bug, ou est-ce simplement un choix de conception ? » Enfin, l'outil regroupe les découvertes similaires afin qu'au lieu de signaler 100 petites erreurs, il signale la cause racine majeure.

Les résultats : Trouver les dysfonctionnements cachés

Les auteurs ont testé ce système sur un projet réel appelé le protocole Phi. Les résultats suggèrent que cette approche fonctionne, bien qu'elle soit encore un travail en cours.

Voici ce qui s'est passé lors de leur expérience :

L'outil a commencé par examiner 3 217 paires de chemins de code.
Après avoir filtré celles qui n'étaient manifestement pas liées, il en a conservé 1 643 pour une investigation approfondie.
Le détecteur IA a trouvé 201 problèmes potentiels (un mélange de candidats « suspects » et « confirmés »).
Après le regroupement des rapports similaires et la suppression des doublons, ce nombre est tombé à 101 groupes.
Un validateur strict a réduit ce chiffre davantage pour arriver à 44 positifs confirmés.
Enfin, après examen des causes racines par un expert humain, l'équipe a identifié 13 problèmes uniques et effectifs.

Ces 13 problèmes étaient de ceux que les outils standards manquent. Par exemple :

Le mélange de « Preuve » : Un système permettait de réutiliser une preuve de propriété pour un article différent parce que les chemins « achat » et « réclamer » ne liaient pas correctement la preuve à l'article spécifique.
La confusion sur les frais : Une partie du système calculait les frais en « points de base » (une unité de pourcentage) tandis qu'une autre partie traitait le même nombre comme des « wei » (une minuscule unité de monnaie), entraînant des erreurs financières massives.
Le piège du remboursement : Lorsqu'un utilisateur payait trop, le chemin de transaction « simple » remboursait l'utilisateur, mais le chemin de transaction « par lot » envoyait accidentellement le remboursement à un contrat intermédiaire, laissant l'utilisateur sans rien.

Les auteurs suggèrent que cette méthode est particulièrement efficace pour attraper les bugs de « logique métier » — des erreurs dans la façon dont le système pense l'argent et les règles — plutôt que de simples fautes de frappe. Ils notent que le processus n'est pas parfait ; il a généré beaucoup de « bruit » (fausses alertes) qui ont dû être nettoyées, et qu'il repose sur la capacité de l'IA à être assez intelligente pour repérer la relation. Cependant, le fait qu'elle ait trouvé 13 problèmes distincts à fort impact que les autres outils ont manqués suggère que regarder le code sous l'angle des « paires chirales » est une nouvelle direction prometteuse.

L'article conclut que, bien que ce ne soit pas une baguette magique capable de résoudre tous les problèmes de sécurité, cela offre une manière structurée de trouver les bugs qui se cachent dans les interstices entre les lignes de code. En traitant les chemins de code comme des images miroirs, nous pouvons enfin voir les fissures qui apparaissent lorsque le reflet ne correspond pas à l'objet.

Résumé Technique : Analyse Chirale des Smart Contracts

1. Énoncé du Problème

Les vulnérabilités des smart contracts découlent fréquemment non pas d'instructions isolées non sécurisées, mais d'incohérences relationnelles entre des parcours métier qui sont sémantiquement appariés mais syntaxiquement distincts. Les exemples courants incluent les écarts entre :

Points d'entrée simples vs par lots (batch).
Flux directs vs flux via adaptateurs.
Parcours de devis (aperçu) vs parcours d'exécution.
Opérations inverses (ex: achat vs vente, frappe/mint vs destruction/burn).

Les analyseurs statiques existants excellent dans la détection de motifs syntaxiques locaux, de dépendances de type "taint" et de vulnérabilités de fonction unique (ex: réentrance, appels non vérifiés). Cependant, ils manquent d'un « oracle » pour les bugs relationnels : ils ne peuvent pas déterminer si deux parcours correspondants préservent les mêmes gardes, transitions d'état, flux de valeurs ou comportements d'échec. Ces bugs nécessitent souvent de comparer la logique d'un wrapper avec une fonction centrale, ou un répartiteur de lots avec un parcours d'opération simple, pour être détectés.

2. Méthodologie : Analyse Chirale

Le papier introduit l'analyse chirale, un modèle relationnel traitant les parcours métier sémantiquement appariés comme des spécifications implicites les uns pour les autres. Le terme « chiral » capture des opérations qui sont miroirs, alternatives ou liées au cycle de vie (ex: simple/lot, wrapper/cœur) sans nécessiter d'identité syntaxique.

2.1 Le Modèle de Vulnérabilité Chirale

Les auteurs formalisent une relation chirale ( $R_\chi$ ) comme un analogue statique d'une relation métamorphique. Elle consiste en deux parcours ( $p, q$ ), un type de relation ( $\tau$ ), et un ensemble d'obligations induites par la relation. Ces obligations sont des approximations des comportements attendus à travers sept dimensions sémantiques :

Garde (Guard) : Modificateurs, préconditions et vérifications d'éligibilité.
Acteur (Actor) : Identités des appelants, signataires, payeurs et destinataires de remboursements.
État (State) : Ensembles de lecture/écriture, drapeaux (flags), compteurs et deltas d'état.
Valeur (Value) : Unités, frais, récompenses, transferts et gestion des remboursements.
Ordre (Order) : Séquences check-effect-interaction et timing de règlement.
Échec (Failure) : Comportement de revert, sémantique de succès partiel et émission d'événements.
Externe (External) : Utilisation d'oracles, callbacks et dépendances inter-contrats.

Une vulnérabilité chirale est définie comme une violation d'une telle obligation entraînant un impact de sécurité ou de protocole réalisable (ex: perte de fonds, changement d'état non autorisé ou erreurs de comptabilité).

2.2 Le Pipeline ChiralDetector

Les auteurs implémentent ce modèle dans ChiralDetector, un pipeline en quatre étapes conçu pour équilibrer le rappel (recall) et la précision tout en gérant les coûts des LLM :

Extraction de Parcours et Résumé :
- Construit un graphe d'appel au niveau du projet à partir du code source Solidity.
- Extrait les « parcours métier » (fonctions uniques, chaînes d'entrée à feuille, et segments de bifurcation).
- Génère un résumé de faits sémantiques ( $\Phi(p)$ ) pour chaque parcours, capturant les lectures/écritures de stockage, les transferts de valeur, les modificateurs et les appels externes. Cette abstraction est intentionnellement perte de données (lossy) mais orientée vers la relation.
Réduction des Paires de Candidats :
- Évite les comparaisons exhaustives en $O(n^2)$ en utilisant un classificateur statique.
- Évalue les paires de parcours basées sur des empreintes de stockage partagées, des appels externes chevauchants, des indices de nommage (ex: "claim" vs "batchClaim") et des similitudes d'acteurs/flux de valeur.
- Priorise les paires susceptibles de former une relation chirale sans supprimer les signaux à haut rappel incertains.
Filtrage Sémantique et Détection (basés sur le LLM) :
- Filtre Sémantique : Détermine si une paire forme une relation chirale plausible et assigne un type de relation (ex: inverse, wrapper/cœur). Il est instruit d'accepter des paires ayant des longueurs de chemin différentes ou des directions économiques opposées.
- Détecteur Sensible à la Relation : Étant donné une relation confirmée, le LLM identifie les obligations spécifiques violées, fournit des preuves sources et formule une thèse d'impact. Les prompts sont structurés comme des « contrats » pour forcer un raisonnement explicite plutôt que des conclusions vagues.
Validation Stricte et Déduplication :
- Un validateur strict tente de falsifier les découvertes en vérifiant si la relation est justifiée, si des preuves existent, et si d'autres chemins de code invalident l'impact.
- La déduplication de cause racine fusionne les multiples rapports partageant le même défaut sous-jacent et la correction probable, distinguant le bruit au niveau de la paire des problèmes au niveau de la racine.

3. Contributions Clés

Modèle d'Analyse Chirale : Un cadre de vulnérabilité relationnelle qui traite les parcours métier correspondants comme des spécifications implicites, allant au-delà de l'analyse de fonction unique.
Formalisation : Définition des relations chirales comme analogues métamorphiques statiques et dérivation de sept dimensions d'obligations spécifiques.
Implémentation de ChiralDetector : Un prototype de pipeline intégrant l'analyse statique, le classement statique de paires, la détection sémantique par LLM, la validation par falsification stricte et la déduplication de cause racine.
Preuve Empirique : Une évaluation préliminaire sur le protocole Phi démontrant la détection d'incohérences de logique métier difficiles à exprimer via des règles de fonction unique.

4. Résultats d'Évaluation

Les auteurs ont évalué ChiralDetector sur le protocole Phi, un projet Solidity contenant diverses formes de relations (claim/batch, adapter/factory, quote/execution).

Métriques de l'Entonnoir :
- Départ de 3 217 paires de candidats classées statiquement.
- Réduction à 1 643 pires pour la détection sémantique.
- Production de 201 découvertes nettoyées/candidats suspects.
- Réduction à 101 groupes localement dédupliqués.
- 44 groupes ont survécu à la validation stricte.
- La déduplication finale manuelle des causes racines a produit 13 problèmes uniques effectifs.
Exemples de Découvertes Représentatives :
- M10 : Réutilisation de preuve Merkle inter-art (Violation de flux/garde similaire).
- M13 : Incohérence d'unité de frais (points de base vs wei) (Violation de valeur/unité).
- M12 : Helpers de suivi publics corrompant l'état du curateur (Violation d'état/accès).
- M05/M02/M04 : Écarts de propagation de remboursement et asymétries de garde entre les chemins simples et par lots (Violations de flux de valeur wrapper/cœur et simple/lot).
Analyse des Coûts :
- L'exécution complète a coûté environ 212,70 CNY (hors temps humain).
- Le coût dominant était l'inférence LLM (filtrage sémantique, détection et validation), non l'analyse statique.
- Le validateur strict a considérablement réduit le bruit, rejetant 57 des 101 groupes localement dédupliqués.

5. Signification et Revendications

Le papier affirme que l'analyse chirale expose une classe de bugs — les incohérences relationnelles — qui sont naturellement difficiles à exprimer via des règles de fonction unique mais qui sont critiques pour la sécurité des protocoles.

Insight : De nombreux bugs de logique métier existent parce que deux parcours liés ne s'accordent pas sur la gestion d'un objet métier partagé (ex: un destinataire de remboursement ou un calcul de frais), plutôt que parce qu'une fonction est localement non sécurisée.
Utilisation Structurée du LLM : Le papier soutient que l'utilisation des LLM au sein d'un pipeline structuré (réduction statique $\to$ filtrage sémantique $\to$ validation stricte) est plus efficace et rentable que l'« audit d'agent direct » (lecture non restreinte du code). Le pipeline externalise les décisions intermédiaires (paires, relations, obligations), rendant l'analyse inspectable et débogable.
Modestie : Les auteurs précisent explicitement que l'évaluation actuelle est une étude de cas préliminaire sur un seul protocole. Ils ne prétendent pas avoir établi des mesures de rappel ou de précision générales. Ils reconnaissent les limites, notamment l'approximation de la sémantique Solidity dans l'extraction de parcours, le potentiel d'hallucination des LLM et l'absence de génération automatique de témoins (transactions de preuve de concept exécutables).

Ce travail se positionne comme une étape vers la rendre le raisonnement de la logique métier explicite et répétable dans l'audit de smart contracts, offrant un vocabulaire pour décrire pourquoi des incohérences spécifiques sont importantes.