Merge pull request #23 from lisa-analyzer/truth-ground

Ground Truth and Dockerfile

Author: VincenzoArceri

.gitignore

@@ -9,6 +9,9 @@
 
 # Ignore output directories that contain generated results
 evm-outputs/
+test-ground-truth-stats/
+evm-testcases/ground-truth/test/logs.txt
+evm-testcases/ground-truth/test/statistics.csv
 
 # Ignore downloaded bytecode
 evm-testcases/benchmark/

Dockerfile

@@ -0,0 +1,36 @@
+# Use a base image with JDK 11
+FROM openjdk:11-jdk-slim
+
+# Specify the version of Gradle to install
+ARG GRADLE_VERSION=6.6
+
+# Install Gradle
+RUN apt-get update && apt-get install -y wget unzip git && \
+    wget https://services.gradle.org/distributions/gradle-${GRADLE_VERSION}-bin.zip && \
+    mkdir /opt/gradle && \
+    unzip -d /opt/gradle gradle-${GRADLE_VERSION}-bin.zip && \
+    rm gradle-${GRADLE_VERSION}-bin.zip && \
+    ln -s /opt/gradle/gradle-${GRADLE_VERSION}/bin/gradle /usr/bin/gradle && \
+    apt-get clean && rm -rf /var/lib/apt/lists/*
+
+# Set working directory
+WORKDIR /app
+
+# Clone the EVMLiSA repository (latest stable version)
+# RUN git clone https://github.com/lisa-analyzer/evm-lisa.git .
+
+# Copy the entire EVMLiSA project into the container (latest version)
+COPY . .
+
+# Build the project with Gradle
+RUN gradle build
+
+# Extract the project ZIP file for distribution
+RUN gradle distZip && \
+    unzip -o build/distributions/evm-lisa.zip -d /app/execution
+
+# Create results directory
+RUN mkdir -p /app/execution/results
+
+# Set the entry point of the container
+ENTRYPOINT ["/app/execution/evm-lisa/bin/evm-lisa"]

README.md

@@ -9,30 +9,22 @@
 
 EVMLiSA is a static analyzer based on abstract interpretation for [EVM bytecode](https://www.ethervm.io/) of smart contracts deployed on Ethereum blockchain and built upon [LiSA](https://unive-ssv.github.io/lisa/). Given a EVM bytecode smart contract, EVMLiSA builds a sound and precise control-flow graph of the smart contract.
 
-
 EVMLiSA is based on the peer-reviewed publication
 > Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. _**"Towards a Sound Construction of EVM Bytecode Control-Flow Graphs"**_. In Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2024), co-located with ECOOP 2024.
 
-
 # 🛠 Building EVMLiSA
 Compiling EVMLiSA requires:
 - JDK >= 11
 - [Gradle](https://gradle.org/releases/) >= 6.6
 - [Etherscan API key](https://etherscan.io/myapikey)
 
-Development is done in [Eclipse](https://www.eclipse.org/downloads/).
 You need to:
 - Clone the repository:
   ```bash
   git clone https://github.com/lisa-analyzer/evm-lisa.git
   cd evm-lisa
   ```
-- Install the Gradle IDE Pack plugin through the Eclipse Marketplace; from the eclipse menu bar:
-  - *Help*
-  - *Eclipse Marketplace...*
-  - *Search* for *Gradle IDE Pack 3.8*
-  - *Install Gradle IDE Pack 3.8*
-- Import the project into the eclipse workspace as a Gradle project.
+- Import the project into the Eclipse/IntelliJ workspace as a Gradle project (optional).
 
 # ⚙️ Running EVMLiSA
 Before running EVMLiSA, ensure you have set up an Environment Variable with your Etherscan API Key. Follow the steps below to set up the environment variable:
@@ -46,8 +38,30 @@ ETHERSCAN_API_KEY=<your_etherscan_api_key>
 
 > Here you can find how to generate an [Etherscan API key](https://etherscan.io/myapikey).
 
-Once you have set up the environment variable, follow these steps to run EVMLiSA:
+Once you have set up the environment variable, you can run EVMLiSA via Docker or via Bash.
+
+## Via Docker
+Build the container:
+```
+mkdir -p execution/docker &&
+docker build -t evm-lisa:latest .
+```
+
+Then you can run EVMLiSA with:
+```
+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`: mount the `.env` file.
+- `-v $(pwd)/execution/docker:/app/execution/results`: share the results' folder.
 
+> Replace `<smart_contract_address>` with the address of the Ethereum smart contract you want to analyze.
+
+## Via Bash
 Build the Project:
 ```bash
 ./gradlew build
@@ -63,11 +77,12 @@ Unzip the Distribution:
 unzip build/distributions/evm-lisa.zip -d execution
 ```
 
-Run EVMLiSA:
+Then you can run EVMLiSA with:
 ```bash
-./execution/evm-lisa/bin/evm-lisa -a <smart_contract_address> [options]
+./execution/evm-lisa/bin/evm-lisa \
+-a <smart_contract_address> [options]
 ```
-Replace `<smart_contract_address>` with the address of the Ethereum smart contract you want to analyze.
+> Replace `<smart_contract_address>` with the address of the Ethereum smart contract you want to analyze.
 
 This command will initiate the analysis process for the specified smart contract, providing insights and results based on the EVM bytecode of the contract.
 
@@ -94,15 +109,32 @@ EVMLiSA introduces the abstract stack powerset domain $\texttt{SetSt}_{k,h,l}$ w
 
 # 📋 Running example
 Here is an example of how to run EVMLiSA. In this example, we will analyze a smart contract at the address `0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B` with specific options for stack size, stack-set size, live storage usage and the dump of the CFG:
+
+- Bash:
+```bash
+./execution/evm-lisa/bin/evm-lisa \
+-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B \
+--stack-size 64 \
+--stack-set-size 10 \
+--dump-stats \
+--use-live-storage
 ```
-./execution/evm-lisa/bin/evm-lisa 
--a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
---stack-size 64 
---stack-set-size 10 
+
+- Docker:
+```bash
+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
---dump-analysis dot
 ```
 
+> Use `docker run -a stderr` to dump only the json report as standard output.
+
 The expected output is as follows:
 ```yaml
 ##############
@@ -123,3 +155,10 @@ Maybe unsound jumps: 0
 - _Unsound_: the jump node is reached at least with a stack with an unknown numerical value that may correspond to a
 valid jump destination as the top element;
 - _Maybe unsound_: the stack set exceeded the maximal stack size.
+
+---
+
+## Contributors
+<a href="https://github.com/lisa-analyzer/evm-lisa/graphs/contributors">
+  <img src="https://contrib.rocks/image?repo=lisa-analyzer/evm-lisa" />
+</a>

benchmark/50-ground-truth.txt

@@ -0,0 +1,50 @@
+0xDcfCcaf54CB8c7c30bb7959929AbA24bF136FF57
+0x5b348ec54c290683697f6a812ca1bfbb0e74c70d
+0x9a1ba1687c2759fe96bfacbfb5300458b7d726f0
+0x4582b79844e753ed53928d8b8761e9f27eb22735
+0x60f19fd1f15fc08a1ea27d407dae25c4e7937547
+0x1370e65e0228b27566a5cb7328160794001f8651
+0x0dcd1b77ef4459c37551b3a3fa4a8e1f2485ad08
+0x16eA5Db6A7C2A72749a7f7600CAA64c97468D50E
+0x5a67e970cc210d6b5fb6512d8142e3eb648c1d32
+0xb04862d030a38c351e8ecae09508cd30f80d88e3
+0x6ea4f5bcd17185c5958677569340e39ac6364e9f
+0xced519a9e7555dee0399f8da3019d8d557a88f81
+0x2fa57c80249b0683c443043aB01b894125876AfC
+0x0c6b8078d27c9729fad5db98c331291bf57ec879
+0x2cfC31b4e1E838453c22675F46bB248AC9DDD439
+0x33f9704b980a21b776eac1d9d4111db33ab6dfda
+0x9960012D71d2085516646B411925AD1d115ED01F
+0x7Afa3d0E44046C7ce8094dC429305A7ff3706D10
+0xcbe2cb2511e4fc2ca3552a65cf95324a5786c64f
+0xc4772Be15F0483672CD5f16CA06456c46908B61c
+0xfdf37696ba7b6f96efda6109fab72a1351c2e33a
+0x37c1f2469d510449a847e4e5c48607a2fc9aa223
+0xce85d05d57c4b16a09de0133c2abedf1bfeea57c
+0xd5a14d1846de1ad342853b79d1b5ef344c4973ef
+0xcc0eab15b35cf04b57db2bb1f9237cd782115bdc
+0x7699B9ACb26b9d05bd9091e14B28Ba57C1F0F5E8
+0x3f121b9a6bc33b6c9f711ccbcaac67459c875641
+0xb663945fc96656ad9f5b7ad1561182aca7071592
+0x9248679610d7a502a069948278160c88239f123b
+0x7f212c237699f3244da5ac025e12bcbf00d09357
+0x5b7279055048d435d70e86be71764de0a09e5b7f
+0x13b385a0cbc3296f14b342bad0e4fdf91ee08100
+0x0a442ac10830f98e6f0485c6193490c5260e94b8
+0xfa0460097248642d69bfb223bab5999507a8c23d
+0xc053308c25597ac6447ccfbf25bb08bfdf03b596
+0x3b7c618156f8cef53e123a66166aaf915b30ba3e
+0x75b884711094aa9f407251892d28653d049fafbd
+0xb0990e799314c516060b67a030fa5f5318baab69
+0xe536920e8256d58Ca9356899bcc36C4F14E76a2c
+0x306c0b64c39fb8924b026f6b9418d38278fc3c3f
+0x7c6ECf809bc86518458fcC87CdC73B9a4289Cc40
+0xcaa7f414906138a05051ecb759163dcc20514510
+0xf7783e451fcbf7ccc2e15b7fee4f534b41ecd6e4
+0x75272b96b7685834ef49b406e6a333ea28b10860
+0x3932f366886d2b981485503a182173da80d15c97
+0xa25150b69733D6834628613E712934C279BEadF7
+0xb30aef19a72d235090100795dacfaf529813f1f3
+0x78791ee453093a33486a7a5c5e425f998f63a785
+0x62fb2cdaf98b4851920548e991e14445721ad952
+0xa151e7a30b805d399106bef9ee6b4a463232b643

evm-testcases/cfs/add/report.json

@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_program.evm-testcases_cfs_add_add_eth.sol().json" ],
   "info" : {
     "cfgs" : "1",
-    "duration" : "121ms",
-    "end" : "2024-07-02T10:39:01.518+02:00",
+    "duration" : "142ms",
+    "end" : "2024-10-03T17:31:51.377+02:00",
     "expressions" : "6",
     "files" : "1",
     "globals" : "0",
     "members" : "1",
     "programs" : "1",
-    "start" : "2024-07-02T10:39:01.397+02:00",
+    "start" : "2024-10-03T17:31:51.235+02:00",
     "statements" : "11",
     "units" : "0",
     "version" : "0.1b8",