Added javadoc

Author: merendamattia

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

@@ -24,16 +24,6 @@
  * <li>Helps in detecting vulnerabilities where external inputs modify contract
  * state without verification.</li>
  * </ul>
- * <p>
- * <b>Implementation Details:</b>
- * </p>
- * <ul>
- * <li>Maintains an abstract stack where tainted values are tracked.</li>
- * <li>Defines tainted operators corresponding to EVM opcodes that introduce
- * untrusted values.</li>
- * <li>Provides methods to create TOP (fully tainted) and BOTTOM (untainted)
- * states.</li>
- * </ul>
  *
  * @see TaintAbstractDomain
  * @see UncheckedExternalInfluenceChecker

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

@@ -1,12 +1,29 @@
 package it.unipr.analysis.taint;
 
 import it.unipr.analysis.operator.*;
+import it.unipr.checker.UncheckedStateUpdateChecker;
 import it.unive.lisa.symbolic.value.Operator;
 import java.util.ArrayList;
 import java.util.Collections;
 import java.util.HashSet;
 import java.util.Set;
 
+/**
+ * This abstract domain represents the taint analysis for detecting unchecked
+ * state updates in smart contracts. It extends TaintAbstractDomain to track whether
+ * values derived from external calls (CALL, DELEGATECALL, STATICCALL) influence
+ * the contract's state without validation.
+ *
+ * <p><b>Purpose:</b></p>
+ * <ul>
+ *   <li>Identifies operations that introduce tainted values from external contract calls.</li>
+ *   <li>Tracks symbolic execution to determine if tainted values propagate to SSTORE.</li>
+ *   <li>Detects vulnerabilities where external calls modify the contract state without verification.</li>
+ * </ul>
+ *
+ * @see TaintAbstractDomain
+ * @see UncheckedStateUpdateChecker
+ */
 public class UncheckedStateUpdateAbstractDomain extends TaintAbstractDomain {
 
 	private static final UncheckedStateUpdateAbstractDomain TOP = new UncheckedStateUpdateAbstractDomain(

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

@@ -2,6 +2,7 @@
 
 import it.unipr.analysis.taint.TaintAbstractDomain;
 import it.unipr.analysis.taint.TaintElement;
+import it.unipr.analysis.taint.UncheckedStateUpdateAbstractDomain;
 import it.unipr.cfg.EVMCFG;
 import it.unipr.cfg.ProgramCounterLocation;
 import it.unipr.cfg.Sstore;
@@ -21,6 +22,27 @@
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
+/**
+ * This checker detects cases where a contract updates its state using values 
+ * returned from external calls (CALL, DELEGATECALL, STATICCALL) without proper validation.
+ *
+ * <p><b>Purpose:</b></p>
+ * <ul>
+ *   <li>Identifies operations where state updates (SSTORE) are influenced by external contract calls.</li>
+ *   <li>Ensures that state updates do not depend on unverified external data.</li>
+ *   <li>Prevents potential security vulnerabilities due to unchecked state modifications.</li>
+ * </ul>
+ *
+ * <p><b>Analysis Process:</b></p>
+ * <ul>
+ *   <li>Uses taint analysis to track the propagation of values from external calls.</li>
+ *   <li>Marks CALL, DELEGATECALL, and STATICCALL as taint sources.</li>
+ *   <li>Marks SSTORE as a sink where state is modified.</li>
+ *   <li>If a tainted value reaches SSTORE without encountering a validation step (JUMPI), the contract is vulnerable.</li>
+ * </ul>
+ *
+ * @see UncheckedStateUpdateAbstractDomain
+ */
 public class UncheckedStateUpdateChecker implements
 		SemanticCheck<SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> {
 

src/main/java/it/unipr/crossChainAnalysis/CrossChainAnalysis.java

@@ -106,6 +106,7 @@ public void runCheckers() {
 			futures.add(_executor.submit(() -> runEventOrderChecker(contract)));
 			futures.add(_executor.submit(() -> runUncheckedStateUpdateChecker(contract)));
 			futures.add(_executor.submit(() -> runUncheckedExternalInfluenceChecker(contract)));
+			// TODO add tx.origin and timestamp dependency checker
 		}
 
 		try {