Reentrancy checker & plot evmlisa results

script-python/journal/compile-all.py

@@ -79,6 +79,36 @@ def extract_and_save_longest_bytecode():
                         bytecode_file.write("0x" + longest_bytecode)
                     # print(f"Extracted longest bytecode from {longest_contract_name} to {bytecode_filename}")
 
+def extract_and_save_bytecode():
+    """
+    Extracts all bytecode from each .json file and saves it in the specified output directory.
+    """
+    # Clear and create bytecode directory
+    clear_directory(bytecode_dir)
+    os.makedirs(bytecode_dir, exist_ok=True)
+
+    for json_filename in os.listdir(json_dir):
+        if json_filename.endswith(".json"):
+            json_filepath = os.path.join(json_dir, json_filename)
+            with open(json_filepath, 'r') as json_file:
+
+                data = json.load(json_file)
+                contracts = data.get("contracts", {})
+                count = 1  # Sequential counter for each bytecode in the same JSON
+
+                for contract_name, contract_data in contracts.items():
+                    bytecode = contract_data.get("bin")
+                    if bytecode:
+                        # Add a sequential number to the filename
+                        bytecode_filename = os.path.join(
+                            bytecode_dir, f"{os.path.splitext(json_filename)[0]}_{count}.bytecode"
+                        )
+                        with open(bytecode_filename, 'w') as bytecode_file:
+                            bytecode_file.write("0x" + bytecode)
+                        print(f"Extracted bytecode to {bytecode_filename}")
+                        count += 1  # Increment counter for next bytecode
+
 if __name__ == "__main__":
     compile_solidity_sources()
+    # extract_and_save_bytecode()
     extract_and_save_longest_bytecode()

script-python/journal/run-benchmark.py

@@ -15,7 +15,7 @@
 results_dir = './reentrancy/results'
 result_evmlisa_dir = results_dir + '/evmlisa'
 result_ethersolve_dir = results_dir + '/ethersolve'
-max_threads = os.cpu_count() / 2  # Core avaiable
+max_threads = int(os.cpu_count() / 3)  # Core avaiable
 
 #################################### Utility
 def delete_tmp_files(directory):
@@ -53,26 +53,30 @@ def clean_files(directory_path):
             # else:
                 # print(f"No changes made to {filename}")
 
-def plot_results(data_ethersolve, data_solidifi):
+def plot_results(data_evmlisa, data_ethersolve, data_solidifi):
     keys1 = sorted(data_ethersolve.keys())
     values1 = [data_ethersolve[key] for key in keys1]
 
     keys2 = sorted(data_solidifi.keys())
     values2 = [data_solidifi[key] for key in keys2]
 
+    keys3 = sorted(data_evmlisa.keys())
+    values3 = [data_evmlisa[key] for key in keys3]
+
     plt.figure(figsize=(12, 6))
 
     plt.plot(keys1, values1, marker='o', label='Ethersolve', color='purple')
     plt.plot(keys2, values2, marker='o', label='SolidiFI', color='red')
+    plt.plot(keys3, values3, marker='o', label='EVMLiSA', color='green')
 
     plt.xlabel('Problem ID')
     plt.ylabel('Value')
     plt.title('Comparison of results (re-entrancy)')
-    plt.xticks(sorted(set(keys1).union(set(keys2))))  # Show all problem IDs on x-axis
+    plt.xticks(sorted(set(keys1).union(set(keys2).union(keys3))))  # Show all problem IDs on x-axis
     plt.legend()
     plt.grid()
 
-    # plt.show()
+    plt.show()
 
 #################################### EVMLiSA
 
@@ -153,7 +157,7 @@ def evmlisa():
     clean_files(result_evmlisa_dir)
     print(f"[EVMLISA] File cleaned.")
 
-def analyze_results_evmlisa(directory_path):
+def check_sound_analysis_evmlisa(directory_path):
     sound = True
 
     for filename in os.listdir(directory_path):
@@ -175,6 +179,39 @@ def analyze_results_evmlisa(directory_path):
     if sound:
         print("[EVMLiSA] All analysis are SOUND")
 
+def results_evmlisa(directory_path):
+    re_entrancy_warning_counts = {}
+
+    for filename in os.listdir(directory_path):
+        if filename.endswith(".json"):
+            file_path = os.path.join(directory_path, filename)
+            try:
+                with open(file_path, 'r') as file:
+                    data = json.load(file)
+
+                    if "re-entrancy-warning" in data:
+                        re_entrancy_warning_counts[filename] = data['re-entrancy-warning']
+                    else:
+                        print(f"[EVMLiSA] Warning: 're-entrancy-warning' not found in {filename}")
+            except Exception as e:
+                print(f"[EVMLiSA] ERROR: {filename}: {e}")            
+
+    results = defaultdict(int)
+    for file, result in re_entrancy_warning_counts.items():
+        match = re.match(r'buggy_(\d+)-\w+\.json', file)
+        if match:
+            id = int(match.group(1))
+            results[id] += result
+
+        match = re.match(r'buggy_(\d+)_(\d+)-\w+\.json', file)
+        if match:
+            id = int(match.group(1))
+            results[id] += result
+
+    sorted_data = dict(sorted(results.items()))
+    print(sorted_data)
+    return sorted_data
+
 
 #################################### EtherSolve
 
@@ -311,9 +348,10 @@ def results_solidifi(folder_path):
     evmlisa_thread.join()
     ethersolve_thread.join()
 
-    analyze_results_evmlisa(result_evmlisa_dir)
+    check_sound_analysis_evmlisa(result_evmlisa_dir)
 
     plot_results(
+        results_evmlisa(result_evmlisa_dir),
         results_ethersolve(result_ethersolve_dir),
         results_solidifi("./SolidiFI-benchmark/buggy_contracts/Re-entrancy")
     )

src/main/java/it/unipr/EVMLiSA.java

@@ -1,15 +1,9 @@
 package it.unipr;
 
-import it.unipr.analysis.AbstractStack;
-import it.unipr.analysis.AbstractStackSet;
-import it.unipr.analysis.EVMAbstractState;
-import it.unipr.analysis.MyCache;
-import it.unipr.analysis.MyLogger;
-import it.unipr.analysis.StackElement;
-import it.unipr.cfg.EVMCFG;
-import it.unipr.cfg.Jump;
-import it.unipr.cfg.Jumpi;
+import it.unipr.analysis.*;
+import it.unipr.cfg.*;
 import it.unipr.checker.JumpSolver;
+import it.unipr.checker.ReentrancyChecker;
 import it.unipr.frontend.EVMFrontend;
 import it.unive.lisa.LiSA;
 import it.unive.lisa.analysis.SimpleAbstractState;
@@ -230,6 +224,7 @@ else if (bytecode != null)
 		conf.interproceduralAnalysis = new ModularWorstCaseAnalysis<>();
 		JumpSolver checker = new JumpSolver();
 		conf.semanticChecks.add(checker);
+		conf.semanticChecks.add(new ReentrancyChecker());
 		conf.callGraph = new RTACallGraph();
 		conf.serializeResults = false;
 		conf.optimize = false;
@@ -246,6 +241,8 @@ else if (dumpDot)
 			// Print the results
 			finish = System.currentTimeMillis();
 
+			jsonOptions.put("re-entrancy-warning", UniquePairCollector.getInstance().size());
+
 			MyLogger result = EVMLiSA.dumpStatistics(checker)
 					.address(addressSC)
 					.time(finish - start)

src/main/java/it/unipr/analysis/UniquePairCollector.java

@@ -0,0 +1,73 @@
+package it.unipr.analysis;
+
+import java.util.HashSet;
+import java.util.Set;
+import org.apache.commons.lang3.tuple.Pair;
+
+/**
+ * Singleton class that collects unique Pair<?, ?> elements.
+ */
+public class UniquePairCollector {
+	private static UniquePairCollector _instance = null;
+	private Set<Pair<?, ?>> pairSet;
+
+	/**
+	 * Retrieves the singleton instance of the collector.
+	 *
+	 * @return the singleton instance of {@link UniquePairCollector}.
+	 */
+	public static UniquePairCollector getInstance() {
+		if (_instance == null) {
+			synchronized (UniquePairCollector.class) {
+				if (_instance == null)
+					_instance = new UniquePairCollector();
+			}
+		}
+		return _instance;
+	}
+
+	/**
+	 * Private constructor to prevent instantiation. Initializes the set for
+	 * storing unique pairs.
+	 */
+	private UniquePairCollector() {
+		this.pairSet = new HashSet<>();
+	}
+
+	/**
+	 * Adds a pair to the collection if it is unique.
+	 *
+	 * @param pair the pair to add.
+	 * 
+	 * @return true if the pair was added, false if it was a duplicate.
+	 */
+	public boolean add(Pair<?, ?> pair) {
+		synchronized (UniquePairCollector.class) {
+			return pairSet.add(pair);
+		}
+	}
+
+	/**
+	 * Returns the number of unique pairs in the collection.
+	 *
+	 * @return the size of the collection.
+	 */
+	public int size() {
+		synchronized (UniquePairCollector.class) {
+			return pairSet.size();
+		}
+	}
+
+	/**
+	 * Checks if a given pair is present in the collection.
+	 *
+	 * @param pair the pair to check.
+	 * 
+	 * @return true if the pair is present, false otherwise.
+	 */
+	public boolean contains(Pair<?, ?> pair) {
+		synchronized (UniquePairCollector.class) {
+			return pairSet.contains(pair);
+		}
+	}
+}

src/main/java/it/unipr/checker/ReentrancyChecker.java

@@ -1,8 +1,10 @@
 package it.unipr.checker;
 
 import it.unipr.analysis.EVMAbstractState;
+import it.unipr.analysis.UniquePairCollector;
 import it.unipr.cfg.Call;
 import it.unipr.cfg.EVMCFG;
+import it.unipr.cfg.Sstore;
 import it.unive.lisa.analysis.SimpleAbstractState;
 import it.unive.lisa.analysis.heap.MonolithicHeap;
 import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
@@ -11,10 +13,12 @@
 import it.unive.lisa.checks.semantic.SemanticCheck;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.statement.Statement;
+import java.util.Set;
+import java.util.stream.Collectors;
+import org.apache.commons.lang3.tuple.ImmutablePair;
 
 public class ReentrancyChecker implements
 		SemanticCheck<SimpleAbstractState<MonolithicHeap, EVMAbstractState, TypeEnvironment<InferredTypes>>> {
-
 	@Override
 	public boolean visit(
 			CheckToolWithAnalysisResults<
@@ -23,9 +27,19 @@ public boolean visit(
 
 		if (node instanceof Call) {
 			EVMCFG cfg = ((EVMCFG) graph);
-			// found paths to SSTORE
-		}
 
+			Set<Statement> ns = cfg.getNodes().stream()
+					.filter(n -> n instanceof Sstore)
+					.collect(Collectors.toSet());
+
+			for (Statement stmt : ns)
+				if (cfg.reachableFrom(node, stmt)) {
+
+					tool.warn("Reentrancy attack from " + node.getLocation() + " to " + stmt.getLocation());
+					UniquePairCollector.getInstance().add(new ImmutablePair<>(node.getLocation(), stmt.getLocation()));
+				}
+
+		}
 		return true;
 	}
-}
+}