Riepilogo Tecnico: Analisi Chirale dei Contratti Intelligenti

1. Definizione del Problema

Le vulnerabilità degli smart contract spesso non derivano da singole istruzioni insicure isolate, ma da inconsistenze relazionali tra percorsi di business che sono semanticamente accoppiati ma sintatticamente distinti. Esempi comuni includono discrepanze tra:

• Punti di ingresso singoli vs. batch.
• Flussi diretti vs. basati su adapter.
• Percorsi di preventivo (preview) vs. esecuzione.
• Operazioni inverse (es. acquisto vs. vendita, mint vs. burn).

Gli attuali analizzatori statici eccellono nel rilevare pattern sintattici locali, dipendenze di tipo taint e vulnerabilità di singola funzione (es. reentrancy, chiamate non controllate). Tuttavia, mancano di un "oracolo" per i bug relazionali: non sono in grado di determinare se due percorsi corrispondenti preservino le stesse guardie, transizioni di stato, flussi di valore o comportamenti di fallimento. Questi bug richiedono spesso il confronto della logica di un wrapper rispetto a una funzione core, o di un dispatcher batch rispetto a un percorso a operazione singola, per poter essere rilevati.

2. Metodologia: Analisi Chirale

Il documento introduce l'analisi chirale, un modello relazionale che tratta i percorsi di business semanticamente accoppiati come specifiche implicite l'uno per l'altro. Il termine "chirale" cattura operazioni che sono simili a specchio, alternative o legate al ciclo di vita (es. singolo/batch, wrapper/core) senza richiedere l'identità sintattica.

2.1 Il Modello di Vulnerabilità Chirale

Gli autori formalizzano una relazione chirale ($R_\chi$) come un analogo statico di una relazione metamorfica. Essa consiste in due percorsi ($p, q$), un tipo di relazione ($\tau$) e un insieme di obblighi indotti dalla relazione. Questi obblighi sono approssimazioni dei comportamenti attesi attraverso sette dimensioni semantiche:

1. Guard (Guardia): Modificatori, precondizioni e controlli di idoneità.
2. Actor (Attore): Identità di chiamanti, firmatari, pagatori e destinatari dei rimborsi.
3. State (Stato): Insiemi di lettura/scrittura, flag, contatori e delta di stato.
4. Value (Valore): Unità, commissioni, premi, trasferimenti e gestione dei rimborsi.
5. Order (Ordine): Sequenze check-effect-interaction e tempistiche di regolamento.
6. Failure (Fallimento): Comportamento di revert, semantica di successo parziale ed emissione di eventi.
7. External (Esterno): Utilizzo di oracle, callback e dipendenze cross-contract.

Una vulnerabilità chirale è definita come la violazione di tale obbligo che risulta in un impatto di sicurezza o di protocollo realizzabile (es. perdita di fondi, cambiamenti di stato non autorizzati o errori di contabilità).

2.2 La Pipeline ChiralDetector

Gli autori implementano questo modello in ChiralDetector, una pipeline a quattro stadi progettata per bilanciare richiamo (recall) e precisione gestendo i costi dei Large Language Models (LLM):

1. Estrazione dei Percorsi e Riassunto:

   • Costruisce un grafo delle chiamate a livello di progetto dal codice sorgente Solidity.
   • Estrae i "percorsi di business" (funzioni singole, catene dall'ingresso alla foglia e segmenti di fork).
   • Genera un riassunto dei fatti semantici ($\Phi(p)$) per ogni percorso, catturando letture/scritture di storage, trasferimenti di valore, modificatori e chiamate esterne. Questa astrazione è intenzionalmente lossy ma orientata alla relazione.

2. Riduzione delle Coppie Candidate:

   • Evita confronti esaustivi $O(n^2)$ utilizzando un classificatore statico.
   • Valuta le coppie di percorsi in base a footprint di storage condivisi, sovrapposizione di chiamate esterne, indizi nei nomi (es. "claim" vs "batchClaim") e somiglianze tra attori e flussi di valore.
   • Prioritizza le coppie probabilmente destinate a formare una relazione chirale senza eliminare segnali ad alto richiamo incerti.

3. Filtraggio Semantico e Rilevamento (basato su LLM):

   • Filtro Semantico: Determina se una coppia forma plausibilmente una relazione chirale e assegna un tipo di relazione (es. inversa, wrapper/core). È istruito ad accettare coppie con lunghezze di percorso differenti o direzioni economiche opposte.
   • Rilevatore Consapevole della Relazione: Data una relazione confermata, l'LLM identifica gli obblighi specifici violati, fornisce prove dal codice sorgente e formula una tesi d'impatto. I prompt sono strutturati come "contratti" per forzare un ragionamento esplicito piuttosto che conclusioni vaghe.

4. Validazione Rigorosa e Deduplicazione:

   • Un validatore rigoroso tenta di falsificare i risultati verificando se la relazione è giustificata, se esiste evidenza e se percorsi di codice alternativi invalidano l'impatto.
   • La deduplicazione della causa radice unisce molteplici report che condividono lo stesso difetto sottostante e la probabile correzione, distinguendo tra rumore a livello di coppia e problemi a livello di radice.

3. Contributi Chiave

• Modello di Analisi Chirale: Un framework di vulnerabilità relazionale che tratta i percorsi di business corrispondenti come specifiche implicite, andando oltre l'analisi di singola funzione.
• Formalizzazione: Definizione delle relazioni chirali come analoghi metamorfici statici e derivazione di sette dimensioni specifiche di obbligo.
• Implementazione di ChiralDetector: Una pipeline prototipale che integra analisi statica, classificazione statica delle coppie, rilevamento semantico tramite LLM, validazione della falsificazione rigorosa e deduplicazione della causa radice.
• Evidenza Empirica: Una valutazione preliminare sul protocollo Phi che dimostra il rilevamento di inconsistenze nella logica di business difficili da esprimere come regole di singola funzione.

4. Risultati della Valutazione

Gli autori hanno valutato ChiralDetector sul protocollo Phi, un progetto Solidity contenente diverse forme di relazione (claim/batch, adapter/factory, quote/execution).

• Metriche a Imbuto:

  • È partito da 3.217 coppie candidate classificate staticamente.
  • Ridotto a 1.643 coppie per il rilevamento semantico.
  • Prodotto 201 risultati puliti/candidati sospetti.
  • Collassato in 101 gruppi deduplicati localmente.
  • 44 gruppi sono sopravvissuti alla validazione rigorosa.
  • La deduplicazione manuale finale della causa radice ha prodotto 13 problemi unici effettivi.

• Risultati Rappresentativi:

  • M10: Riutilizzo di prove Merkle cross-art (violazione di flusso/guardia simile).
  • M13: Discrepanza nelle unità di commissione (basis points vs wei) (violazione di valore/unità).
  • M12: Helper di tracciamento pubblici che corrompono lo stato del curatore (violazione di stato/accesso).
  • M05/M02/M04: Lacune nella propagazione dei rimborsi e asimmetrie delle guardie tra percorsi singoli e batch (violazioni di flusso di valore tra wrapper/core e singolo/batch).

• Analisi dei Costi:

  • L'esecuzione completa è costata circa 212,70 CNY (esclusi i tempi umani).
  • Il costo dominante è stato l'inferenza LLM (filtraggio semantico, rilevamento e validazione), non l'analisi statica.
  • Il validatore rigoroso ha ridotto significativamente il rumore, rifiutando 57 dei 101 gruppi deduplicati localmente.

5. Significato e Rivendicazioni

Il documento sostiene che l'analisi chirale espone una classe di bug — le inconsistenze relazionali — che sono naturalmente difficili da esprimere come regole di singola funzione ma critiche per la sicurezza del protocollo.

• Insight: Molti bug della logica di business esistono perché due percorsi correlati non concordano su come gestire un oggetto di business condiviso (es. un destinatario di un rimborso o un calcolo di una commissione), piuttosto che perché una singola funzione sia localmente insicura.
• Utilizzo Strutturato degli LLM: Il documento argomenta che l'uso degli LLM all'interno di una pipeline strutturata (riduzione statica $\to$ filtraggio semantico $\to$ validazione rigorosa) è più efficace ed efficiente in termini di costi rispetto all' "audit diretto tramite agent" (lettura non restrittiva del codice). La pipeline esternalizza le decisioni intermedie (coppie, relazioni, obblighi), rendendo l'analisi ispezionabile e debuggabile.
• Modestia: Gli autori dichiarano esplicitamente che la valutazione attuale è un caso di studio preliminare su un singolo protocollo. Non pretendono di aver stabilito metriche di richiamo o precisione generali. Riconoscono i limiti, inclusa l'approssimazione della semantica Solidity nella fase di estrazione dei percorsi, il potenziale di allucinazioni degli LLM e la mancanza di generazione automatica di testimoni (transazioni di prova di concetto eseguibili).

Il lavoro si posiziona come un passo verso il rendere l'analisi della logica di business esplicita e ripetibile nell'audit degli smart contract, offrendo un vocabolario per descrivere perché specifiche inconsistenze siano rilevanti.