evm lisa Download - evm lisa Quellcode Download

evm lisa

Andere Kategorien

1.0.0

Herunterladen

EVMLISA: Ein abstrakter interpretationsbasierter statischer Analysator für EVM-Bytecode

EVMLISA ist ein statischer Analysator, der auf einer abstrakten Interpretation für EVM -Bytecode von intelligenten Verträgen basiert, die auf Ethereum Blockchain eingesetzt und auf Lisa basieren. Bei einem EVM-Bytecode-Smart-Vertrag erstellt EVMLISA ein solides und präzises Kontroll-Flow-Diagramm des Smart Contract.

EVMLISA basiert auf der Peer-Review-Veröffentlichung

Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. "Auf dem Weg zu einer soliden Konstruktion von EVM-Bytecode-Kontroll-Fluss-Diagrammen" . In Proceedings des 26. ACM International Workshop zu formellen Techniken für Java-ähnliche Programme (FTFJP 2024), die mit ECOOP 2024 geleitet wurden.

? Bau EVMLISA

Das Kompilieren von EVMLISA erfordert:

JDK> = 11
Gradle> = 6,6
Ethercan API -Schlüssel

Sie müssen:

Klonen Sie das Repository:

git clone https://github.com/lisa-analyzer/evm-lisa.git
cd evm-lisa

Importieren Sie das Projekt in den Arbeitsbereich Eclipse/Intellij als Gradle -Projekt (optional).

EVMLISA laufen

Stellen Sie vor dem Ausführen von EVMLISA sicher, dass Sie eine Umgebungsvariable mit Ihrem Ethercan -API -Schlüssel eingerichtet haben. Befolgen Sie die folgenden Schritte, um die Umgebungsvariable einzurichten:

Erstellen Sie zunächst eine Datei namens .env im EVMLISA -Projekt.
Fügen Sie in der .env -Datei die folgende Zeile hinzu:

 ETHERSCAN_API_KEY=<your_etherscan_api_key>

Ersetzen Sie <your_etherscan_api_key> durch Ihren Ethercan -API -Schlüssel.

Hier finden Sie, wie Sie einen Ethercan -API -Schlüssel generieren.

Sobald Sie die Umgebungsvariable eingerichtet haben, können Sie EVMLISA über Docker oder Bash ausführen.

Über Docker

Bauen Sie den Container:

 mkdir -p execution/docker &&
docker build -t evm-lisa:latest .

Dann können Sie EVMLISA mit:

 docker run --rm -it 
-v $(pwd)/.env:/app/.env 
-v $(pwd)/execution/docker:/app/execution/results 
evm-lisa:latest 
-a <smart_contract_address> [options]

-v $(pwd)/.env:/app/.env : montieren Sie die .env -Datei.
-v $(pwd)/execution/docker:/app/execution/results : Teilen Sie den Ordner der Ergebnisse.

Ersetzen Sie <smart_contract_address> durch die Adresse des Smart -Vertrags von Ethereum, den Sie analysieren möchten.

Über Bash

Bauen Sie das Projekt auf:

./gradlew build

Verteilungszip erstellen:

./gradlew distZip

Die Verteilung entpacken:

unzip build/distributions/evm-lisa.zip -d execution

Dann können Sie EVMLISA mit:

./execution/evm-lisa/bin/evm-lisa 
-a < smart_contract_address > [options]

Ersetzen Sie <smart_contract_address> durch die Adresse des Smart -Vertrags von Ethereum, den Sie analysieren möchten.

In diesem Befehl wird der Analyseprozess für den angegebenen Smart -Vertrag eingeleitet, der Erkenntnisse und Ergebnisse liefert, die auf der EVM -Bytecode des Vertrags basieren.

 Options:
 -a,--address <arg>          address of an Ethereum smart contract
 -b,--benchmark <arg>        filepath of the benchmark suite (i.e., a list of smart contract addresses)
 -C,--cores <arg>            number of cores to use
 -c,--dump-cfg               dump the CFG
 -d,--dump-analysis <arg>    dump the analysis (html, dot)
 -D,--download-bytecode      download the bytecode, without analyzing it
 -f,--filepath <arg>         filepath of an EVM bytecode smart contract
 -o,--output <arg>           output directory path
 -q,--stack-size <arg>       maximal height of stack
 -s,--dump-stats             dump statistics
 -S,--use-live-storage       use the live storage in SLOAD
 -w,--stack-set-size <arg>   maximal size of stack sets

? Abstrakte Stack -Set -Domäne

Bei der Analyse von EVM -Bytecode -Programmen verwendet EVMLISA eine Domäne mit abstrakten Stapeln, um die Genauigkeit zu verbessern, insbesondere wenn Schleifen im Quellcode auftreten.

EVMLISA führt die abstrakte Stack Powerset -Domäne ein $ texttt {setst} _ {k, h, l} $ das besteht aus Sätzen abstrakter Stapel mit höchstens $ l $ Elemente und eine Höhe von höchstens $ H $ . Mit dieser Domäne kann der Analysator Sammlungen abstrakter Stapel aufrechterhalten, die Notwendigkeit vermeiden, die Lub zu berechnen und jedes Element eines abstrakten Stacks zu ermöglichen $ k $ Ganzzahlset.

? Auslaufbeispiel

Hier ist ein Beispiel dafür, wie man EVMLISA betreibt. In diesem Beispiel werden wir einen intelligenten Vertrag unter der Adresse 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B mit spezifischen Optionen für Stapelgröße, Stapelgröße, Live-Speichergebrauch und Dump des CFG analysieren:

Bash:

./execution/evm-lisa/bin/evm-lisa 
-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
--stack-size 64 
--stack-set-size 10 
--dump-stats 
--use-live-storage

Docker:

docker run --rm -it 
-v $( pwd ) /.env:/app/.env 
-v $( pwd ) /execution/docker:/app/execution/results 
evm-lisa:latest 
-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
--stack-size 64 
--stack-set-size 10 
--dump-stats 
--use-live-storage

Verwenden Sie docker run -a stderr , um nur den JSON -Bericht als Standardausgabe zu entsorgen.

Die erwartete Ausgabe ist wie folgt:

 # #############
Total opcodes : 344
Total jumps : 45
Resolved jumps : 44
Definitely unreachable jumps : 1
Maybe unreachable jumps : 0
Unsound jumps : 0
Maybe unsound jumps : 0
# #############

Sprungklassifizierung

Gelöst : Alle Ziele des Sprungknotens wurden gelöst;
Auf jeden Fall unerreichbar : Der Sprungknoten ist nicht erreichbar (dh er wird mit dem unteren abstrakten Zustand erreicht);
Vielleicht nicht erreichbar : Der Sprungknoten ist in der CFG nicht erreichbar, beginnend von seinem Einstiegspunkt, aber er kann über einen (vielleicht) unauftroffenen Sprungknoten (falls vorhanden) erreichbar sein.
Unsicher : Der Sprungknoten wird zumindest mit einem Stapel mit einem unbekannten numerischen Wert erreicht, der einem gültigen Sprungziel als Top -Element entsprechen kann.
Vielleicht unangemessen : Der Stack -Set hat die maximale Stapelgröße überschritten.