First draft of TxOriginChecker with Taint check

Author: denisguareschi

evm-testcases/taint/example12/report.json

@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_program.evm-testcases_taint_example12_example12.sol().json" ],
   "info" : {
     "cfgs" : "1",
-    "duration" : "409ms",
-    "end" : "2024-12-17T12:27:08.913+01:00",
+    "duration" : "247ms",
+    "end" : "2024-12-19T11:23:35.330+01:00",
     "expressions" : "2",
     "files" : "1",
     "globals" : "0",
     "members" : "1",
     "programs" : "1",
-    "start" : "2024-12-17T12:27:08.504+01:00",
+    "start" : "2024-12-19T11:23:35.083+01:00",
     "statements" : "9",
     "units" : "0",
     "version" : "0.1",

src/main/java/it/unipr/analysis/taint/TaintAbstractStack.java

@@ -1,5 +1,6 @@
 package it.unipr.analysis.taint;
 
+import it.unipr.analysis.StackElement;
 import it.unive.lisa.analysis.BaseLattice;
 import it.unive.lisa.analysis.Lattice;
 import it.unive.lisa.analysis.ScopeToken;
@@ -1152,4 +1153,20 @@ public boolean equals(Object obj) {
 	public int hashCode() {
 		return java.util.Objects.hash(stack);
 	}
+
+	public TaintElement getSecondElement() {
+		if (isBottom())
+			return TaintElement.BOTTOM;
+		else if (isTop())
+			return TaintElement.TOP;
+		return this.stack.get(STACK_LIMIT - 2);
+	}
+
+	public TaintElement getFirstElement() {
+		if (isBottom())
+			return TaintElement.BOTTOM;
+		else if (isTop())
+			return TaintElement.TOP;
+		return this.stack.get(STACK_LIMIT - 1);
+	}
 }

src/main/java/it/unipr/analysis/taint/TaintElement.java

@@ -57,7 +57,7 @@ else if (isClean())
 	 * 
 	 * @return {@code true} if this value is taint, {@code false} otherwise
 	 */
-	private boolean isTaint() {
+	public boolean isTaint() {
 		return this == TAINT;
 	}
 

src/main/java/it/unipr/cfg/EVMCFG.java

@@ -127,6 +127,27 @@ public Set<Statement> getAllJumps() {
 
 		return jumpNodes;
 	}
+	
+	/**
+	 * Returns a set of all the JUMPI statements in the CFG.
+	 * 
+	 * @return a set of all the JUMPI statements in the CFG
+	 */
+	public Set<Statement> getAllJumpI() {
+		if (jumpNodes == null) {
+			NodeList<CFG, Statement, Edge> cfgNodeList = this.getNodeList();
+			Set<Statement> jumpStatements = new HashSet<>();
+
+			for (Statement statement : cfgNodeList.getNodes()) {
+				if (statement instanceof Jumpi) {
+					jumpStatements.add(statement);
+				}
+			}
+			return jumpNodes = jumpStatements;
+		}
+
+		return jumpNodes;
+	}
 
 	public int getOpcodeCount() {
 		// -1 for the return statement

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

@@ -1,10 +1,17 @@
 package it.unipr.checker;
 
+import it.unipr.analysis.AbstractStack;
 import it.unipr.analysis.EVMAbstractState;
 import it.unipr.analysis.MyCache;
+import it.unipr.analysis.StackElement;
+import it.unipr.analysis.taint.TaintAbstractStack;
+import it.unipr.analysis.taint.TaintElement;
 import it.unipr.cfg.EVMCFG;
 import it.unipr.cfg.Origin;
 import it.unipr.cfg.ProgramCounterLocation;
+import it.unive.lisa.analysis.AnalysisState;
+import it.unive.lisa.analysis.AnalyzedCFG;
+import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SimpleAbstractState;
 import it.unive.lisa.analysis.heap.MonolithicHeap;
 import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
@@ -18,22 +25,63 @@
 import org.apache.logging.log4j.Logger;
 
 public class TxOriginChecker implements
-		SemanticCheck<SimpleAbstractState<MonolithicHeap, EVMAbstractState, TypeEnvironment<InferredTypes>>> {
+		SemanticCheck<SimpleAbstractState<MonolithicHeap, TaintAbstractStack, TypeEnvironment<InferredTypes>>> {
 
 	private static final Logger log = LogManager.getLogger(TxOriginChecker.class);
 
 	@Override
 	public boolean visit(
 			CheckToolWithAnalysisResults<
-					SimpleAbstractState<MonolithicHeap, EVMAbstractState, TypeEnvironment<InferredTypes>>> tool,
+					SimpleAbstractState<MonolithicHeap, TaintAbstractStack, TypeEnvironment<InferredTypes>>> tool,
 			CFG graph, Statement node) {
 
 		if (node instanceof Origin) {
 			EVMCFG cfg = ((EVMCFG) graph);
-			Set<Statement> jumps = cfg.getAllJumps();
+			Set<Statement> jumps = cfg.getAllJumpI();
 			Statement origin = node;
 
-			for (Statement jump : jumps) {
+			for (AnalyzedCFG<SimpleAbstractState<MonolithicHeap, TaintAbstractStack,
+					TypeEnvironment<InferredTypes>>> result : tool.getResultOf(cfg)) {
+				AnalysisState<SimpleAbstractState<MonolithicHeap, TaintAbstractStack,
+						TypeEnvironment<InferredTypes>>> analysisResult = null;
+
+				for(Statement jump: jumps) {
+					try {
+						analysisResult = result.getAnalysisStateBefore(jump);
+					} catch (SemanticException e1) {
+						log.error("(TxOriginChecker): {}", e1.getMessage());
+					}
+					
+					// Retrieve the symbolic stack from the analysis result
+					TaintAbstractStack taintedStack = analysisResult.getState().getValueState();
+					
+					// If the stack is bottom, the jump is definitely
+					// unreachable
+					if (taintedStack.isBottom())
+						// Nothing to do
+						continue;
+					else {
+						TaintElement firstStackElement = taintedStack.getFirstElement();
+						TaintElement secondStackElement = taintedStack.getSecondElement();
+						if(secondStackElement.isBottom())
+							// Nothing to do
+							continue;
+						else {
+							// Checks if either first or second element in the stack is tainted
+							if(firstStackElement.isTaint() || secondStackElement.isTaint()) {
+								checkForTxOrigin(origin, jump, tool, cfg);
+							}
+						}
+					}
+				}
+				
+				
+
+				
+
+				
+			}
+			/*for (Statement jump : jumps) {
 				if (cfg.reachableFrom(origin, jump)) {
 					ProgramCounterLocation jumploc = (ProgramCounterLocation) jump.getLocation();
 
@@ -54,10 +102,26 @@ public boolean visit(
 					// contaminated value from the stack by origin opcode
 					// (GENERICS)
 				}
-			}
+			}*/
 
 		}
 
 		return true;
 	}
+	
+	private void checkForTxOrigin(Statement origin, Statement jump, CheckToolWithAnalysisResults<
+			SimpleAbstractState<MonolithicHeap, TaintAbstractStack, TypeEnvironment<InferredTypes>>> tool, EVMCFG cfg) {
+			if (cfg.reachableFrom(origin, jump)) {
+				ProgramCounterLocation jumploc = (ProgramCounterLocation) jump.getLocation();
+
+				log.debug("Tx. Origin attack at {} at line no. {} coming from line {}", jumploc.getPc(),
+						jumploc.getSourceCodeLine(),
+						((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine());
+
+				String warn = "TxOrigin attack at " + jumploc.getPc();
+				tool.warn(warn);
+				MyCache.getInstance().addTxOriginWarning(cfg.hashCode(), warn);
+
+			}
+	}
 }