Technisch Overzicht: Chirale Analyse van Smart Contracts

1. Probleemstelling

Kwetsbaarheden in smart contracts ontstaan vaak niet door geïsoleerde onveilige instructies, maar door relationele inconsistenties tussen bedrijfspaden die semantisch aan elkaar gekoppeld zijn maar syntactisch verschillend. Veelvoorkomende voorbeelden zijn discrepanties tussen:

• Single vs. batch entry points (enkele versus batch-toegangspunten).
• Directe vs. adapter-gebaseerde flows.
• Quote (preview) vs. execution paths (offerte versus uitvoering).
• Inverse operaties (bijv. kopen vs. verkopen, minten vs. burnen).

Bestaande statische analysers blinken uit in het detecteren van lokale syntactische patronen, taint-stijl afhankelijkheden en single-function kwetsbaarheden (bijv. reentrancy, ongecontroleerde calls). Ze missen echter een "orakel" voor relationele bugs: ze kunnen niet bepalen of twee corresponderende paden dezelfde guards, state-transities, waarde-flows of foutgedragingen behouden. Deze bugs vereisen vaak het vergelijken van de logica van een wrapper met een kernfunctie, of een batch-dispatcher met een single-operation pad, om gedetecteerd te worden.

2. Methodologie: Chirale Analyse

Het paper introduceert chirale analyse, een relationeel model dat semantisch gekoppelde bedrijfspaden behandelt als impliciete specificaties voor elkaar. De term "chiraal" vangt operaties die spiegelbeeldig, alternatief of lifecycle-gerelateerd zijn (bijv. single/batch, wrapper/core) zonder dat syntactische identiteit vereist is.

2.1 Het Chirale Kwetsbaarheidsmodel

De auteurs formaliseren een chirale relatie ($R_\chi$) als een statische analogie van een metamorfische relatie. Het bestaat uit twee paden ($p, q$), een relatietype ($\tau$), en een set van relatie-geïnduceerde verplichtingen. Deze verplichtingen zijn benaderingen van verwacht gedrag over zeven semantische dimensies:

1. Guard: Modifiers, preconditions en eligibility checks.
2. Actor: Identiteiten van aanroepers, signers, betalers en ontvangers van terugbetalingen.
3. State: Read/write sets, flags, counters en state delta's.
4. Value: Eenheden, fees, beloningen, transfers en afhandeling van terugbetalingen.
5. Order: Check-effect-interaction sequenties en settlement timing.
6. Failure: Revert-gedrag, partial success semantiek en event emissie.
7. External: Oracle-gebruik, callbacks en cross-contract afhankelijkheden.

Een chirale kwetsbaarheid wordt gedefinieerd als een schending van een dergelijke verplichting die resulteert in een haalbare beveiligings- of protocolimpact (bijv. verlies van fondsen, ongeautoriseerde state-wijziging of boekhoudkundige fouten).

2.2 De ChiralDetector Pipeline

De auteurs implementeren dit model in ChiralDetector, een vierfasige pipeline die ontworpen is om recall te balanceren met precisie terwijl de kosten van Large Language Models (LLM's) worden beheerd:

1. Pad Extractie & Samenvatting:

   • Bouwt een project-breed call graph vanuit de Solidity broncode.
   • Extraheert "business paths" (single functies, entry-to-leaf chains en fork segmenten).
   • Genereert een semantische feiten-samenvatting ($\Phi(p)$) voor elk pad, die storage reads/writes, waarde-transfers, modifiers en externe calls vastlegt. Deze abstractie is opzettelijk verlieslatend maar relatie-georiënteerd.

2. Candidate Pair Reduction:

   • Vermijdt uitputtende $O(n^2)$ vergelijkingen door een statische ranker te gebruiken.
   • Scoort paren paden op basis van gedeelde storage footprints, overlappende externe calls, naamgevingshints (bijv. "claim" vs. "batchClaim") en actor/waarde-flow gelijkenissen.
   • Prioriteert paren die waarschijnlijk een chirale relatie vormen zonder onzekere signalen met een hoge recall te verwijderen.

3. Semantische Filtering & Detectie (LLM-gebaseerd):

   • Semantische Filter: Bepaalt of een paar plausibel een chirale relatie vormt en wijst een relatietype toe (bijv. inverse, wrapper/core). De filter krijgt de instructie om paren met verschillende padlengtes of tegengestelde economische richtingen te accepteren.
   • Relatie-bewuste Detector: Gegeven een bevestigde relatie, identificeert de LLM specifieke geschonden verplichtingen, levert bronbewijs en formuleert een impact-thesis. Prompts zijn gestructureerd als "contracten" om expliciet redeneren te dwingen in plaats van vage conclusies.

4. Strikte Validatie & Deduplicatie:

   • Een strikte validator probeert bevindingen te falsifiëren door te controleren of de relatie gerechtvaardigd is, of er bewijs bestaat en of alternatieve code-paden de impact ongeldig maken.
   • Root-cause deduplicatie voegt meerdere rapporten samen die dezelfde onderliggende defect en waarschijnlijke fix delen, waarbij onderscheid wordt gemaakt tussen pair-level ruis en root-level issues.

3. Belangrijkste Bijdragen

• Chirale Analyse Model: Een relationeel kwetsbaarheidsframework dat corresponderende bedrijfspaden behandelt als impliciete specificaties, waarmee de analyse verder gaat dan single-function analyse.
• Formalisering: Definitie van chirale relaties als statische metamorfische analogen en de afleiding van zeven specifieke verplichtingsdimensies.
• ChiralDetector Implementatie: Een prototype pipeline die statische analyse, statische pair ranking, LLM-gebaseerde semantische detectie, strikte falsificatie-validatie en root-cause deduplicatie integreert.
• Empirisch Bewijs: Een voorlopige evaluatie op het Phi-protocol die de detectie demonstreert van inconsistenties in de business-logica die moeilijk te vatten zijn in single-function regels.

4. Evaluatieresultaten

De auteurs evalueerden ChiralDetector op het Phi protocol, een Solidity project met diverse relatievormen (claim/batch, adapter/factory, quote/execution).

• Funnel Metrics:

  • Begon met 3.217 statisch gerankte kandidaat-paren.
  • Gereduceerd tot 1.643 paren voor semantische detectie.
  • Produceerde 201 schone bevindingen/verdachte kandidaten.
  • Gecomprimeerd naar 101 lokaal gededupliceerde groepen.
  • 44 groepen overleefden strikte validatie.
  • Finale handmatige root-cause deduplicatie leverde 13 effectieve unieke issues op.

• Representatieve Bevindingen:

  • M10: Cross-art Merkle proof hergebruik (vergelijkbare flow/guard schending).
  • M13: Fee unit mismatch (basis points vs. wei) (Waarde/eenheid schending).
  • M12: Publieke tracking helpers die curator state corrumperen (State/access schending).
  • M05/M02/M04: Gaten in refund propagatie en guard asymmetrieën tussen single en batch paden (Wrapper/core en single/batch waarde-flow schendingen).

• Kostenanalyse:

  • De volledige run kostte ongeveer 212,70 CNY (exclusief menselijke tijd).
  • De dominante kosten waren LLM-inferentie (semantische filtering, detectie en validatie), niet de statische analyse.
  • De strikte validator verminderde de ruis aanzienlijk door 57 van de 101 lokaal gededupliceerde groepen af te wijzen.

5. Betekenis en Claims

Het paper claimt dat chirale analyse een klasse bugs blootlegt — relationele inconsistenties — die van nature moeilijk te vatten zijn in single-function regels, maar cruciaal zijn voor de protocolbeveiliging.

• Inzicht: Veel business-logic bugs bestaan omdat twee gerelateerde paden het oneens zijn over hoe ze een gedeeld business object afhandelen (bijv. een ontvanger van een terugbetaling of een fee berekening), in plaats van dat een enkele functie lokaal onveilig is.
• Gestructureerd LLM Gebruik: Het paper beargumenteert dat het gebruik van LLM's binnen een gestructureerde pipeline (statische reductie $\to$ semantische filtering $\to$ strikte validatie) effectiever en kostenefficiënter is dan "directe agent auditing" (onbeperkt lezen van code). De pipeline externaliseert tussenliggende beslissingen (paren, relaties, verplichtingen), waardoor de analyse inspecteerbaar en debugbaar wordt.
• Bescheidenheid: De auteurs stellen expliciet dat de huidige evaluatie een voorlopige casestudy is op een enkel protocol. Ze beweren niet dat ze al algemene recall of precisie metrieken hebben vastgesteld. Ze erkennen beperkingen, waaronder de benadering van Solidity semantiek in pad-extractie, het potentieel voor LLM hallucinaties, en het gebrek aan geautomatiseerde witness generatie (uitvoerbare proof-of-concept transacties).

Dit werk positioneert zich als een stap naar het expliciet en reproduceerbaar maken van business-logic redeneren in smart contract auditing, en biedt een vocabulaire om te beschrijven waarom specifieke inconsistenties ertoe doen.