Skip to content

Commit 9481a69

Browse files
merendamattiamerendamattia
committed
fix: deleted pushTaintList and spotlessApply
1 parent b50513d commit 9481a69

File tree

7 files changed

+61
-116
lines changed

7 files changed

+61
-116
lines changed

‎evm-testcases/taint/example08/report.json‎

Lines changed: 0 additions & 38 deletions
This file was deleted.

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -498,9 +498,7 @@ void checkers(LiSAConfiguration conf, LiSA lisa, Program program, JumpSolver che
498498
// Clear existing checks and add the TxOriginChecker
499499
conf.semanticChecks.clear();
500500
conf.semanticChecks.add(new TxOriginChecker());
501-
HashSet<String> list = new HashSet<String>();
502-
list.add("OriginOperator");
503-
conf.abstractState = new SimpleAbstractState<>(new MonolithicHeap(), new TaintAbstractDomain(list),
501+
conf.abstractState = new SimpleAbstractState<>(new MonolithicHeap(), new TaintAbstractDomain(),
504502
new TypeEnvironment<>(new InferredTypes()));
505503
lisa.run(program);
506504

‎src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java‎

Lines changed: 24 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@
1818
import it.unive.lisa.util.representation.StructuredRepresentation;
1919
import java.util.ArrayList;
2020
import java.util.Collections;
21-
import java.util.HashSet;
2221
import java.util.Iterator;
2322
import java.util.List;
2423
import java.util.function.Predicate;
@@ -27,37 +26,25 @@ public class TaintAbstractDomain implements ValueDomain<TaintAbstractDomain>, Ba
2726

2827
private static int STACK_LIMIT = 32;
2928
private static final TaintAbstractDomain TOP = new TaintAbstractDomain(
30-
new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)), new HashSet<String>());
31-
private static final TaintAbstractDomain BOTTOM = new TaintAbstractDomain(null, new HashSet<String>());
29+
new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)));
30+
private static final TaintAbstractDomain BOTTOM = new TaintAbstractDomain(null);
3231

3332
private final ArrayList<TaintElement> stack;
34-
35-
private final HashSet<String> pushTaintList;
3633

3734
/**
3835
* Builds an initial symbolic stack.
3936
*/
4037
public TaintAbstractDomain() {
4138
this.stack = new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM));
42-
this.pushTaintList = new HashSet<String>();
43-
}
44-
45-
/**
46-
* Builds a taint abstract stack starting from a given list of elements that push taint .
47-
*/
48-
public TaintAbstractDomain(HashSet<String> pushTaintList) {
49-
this.stack = new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM));
50-
this.pushTaintList = pushTaintList;
5139
}
5240

5341
/**
54-
* Builds a taint abstract stack starting from a given stack and a list of elements that push taint.
42+
* Builds a taint abstract stack starting from a given stack.
5543
*
5644
* @param stack the stack of values
5745
*/
58-
private TaintAbstractDomain(ArrayList<TaintElement> stack, HashSet<String> pushTaintList) {
46+
private TaintAbstractDomain(ArrayList<TaintElement> stack) {
5947
this.stack = stack;
60-
this.pushTaintList = pushTaintList;
6148
}
6249

6350
@Override
@@ -83,8 +70,12 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
8370

8471
if (op != null) {
8572
switch (op.getClass().getSimpleName()) {
73+
case "OriginOperator": {
74+
TaintAbstractDomain resultStack = clone();
75+
resultStack.push(TaintElement.TAINT);
76+
return resultStack;
77+
}
8678
case "TimestampOperator":
87-
case "OriginOperator":
8879
case "CodesizeOperator":
8980
case "GaspriceOperator":
9081
case "ReturndatasizeOperator":
@@ -105,10 +96,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
10596
case "PushOperator":
10697
case "Push0Operator": {
10798
TaintAbstractDomain resultStack = clone();
108-
if(this.pushTaintList.contains(op.getClass().getSimpleName()))
109-
resultStack.push(TaintElement.TAINT);
110-
else resultStack.push(TaintElement.CLEAN);
111-
resultStack.toString();
99+
resultStack.push(TaintElement.CLEAN);
112100
return resultStack;
113101
}
114102

@@ -121,22 +109,21 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
121109

122110
case "JumpOperator": { // JUMP
123111
if (hasBottomUntil(1))
124-
return BOTTOM;
112+
return BOTTOM;
125113

126114
TaintAbstractDomain resultStack = clone();
127-
TaintElement opnd1 = resultStack.pop();
128-
115+
resultStack.pop();
116+
129117
return resultStack;
130118
}
131119
case "JumpiOperator": { // JUMPI
132-
133120
if (hasBottomUntil(2))
134121
return BOTTOM;
135122

136123
TaintAbstractDomain resultStack = clone();
137-
TaintElement opnd1 = resultStack.pop();
138-
TaintElement opnd2 = resultStack.pop();
139-
124+
resultStack.pop();
125+
resultStack.pop();
126+
140127
return resultStack;
141128
}
142129

@@ -716,7 +703,7 @@ private TaintAbstractDomain swapX(int x, TaintAbstractDomain stack) {
716703
for (int i = 0; i < clone.size(); i++)
717704
result.add((TaintElement) obj[i]);
718705

719-
return new TaintAbstractDomain(result, this.pushTaintList);
706+
return new TaintAbstractDomain(result);
720707
}
721708

722709
private TaintAbstractDomain dupX(int x, TaintAbstractDomain stack) {
@@ -743,7 +730,7 @@ private TaintAbstractDomain dupX(int x, TaintAbstractDomain stack) {
743730
result.add(tmp);
744731
result.remove(0);
745732

746-
return new TaintAbstractDomain(result, this.pushTaintList);
733+
return new TaintAbstractDomain(result);
747734
}
748735

749736
private ArrayList<TaintElement> getStack() {
@@ -854,7 +841,7 @@ public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticExce
854841
result.add(thisElement.glb(otherElement));
855842
}
856843

857-
return new TaintAbstractDomain(result, this.pushTaintList);
844+
return new TaintAbstractDomain(result);
858845
}
859846

860847
@Override
@@ -870,7 +857,7 @@ public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticExce
870857
result.add(thisElement.lub(otherElement));
871858
}
872859

873-
return new TaintAbstractDomain(result, this.pushTaintList);
860+
return new TaintAbstractDomain(result);
874861
}
875862

876863
@Override
@@ -916,9 +903,9 @@ public TaintElement pop() {
916903
* Checks whether between 0 and x-positions of the stack an element is
917904
* bottom. /** Checks whether between 0 and x-positions of the stack an
918905
* element is bottom.
919-
*
906+
*
920907
* @param x the position
921-
*
908+
*
922909
* @return {@code true} if between 0 and x-positions of the stack an element
923910
* is bottom, {@code false} otherwise.
924911
*/
@@ -933,7 +920,7 @@ public boolean hasBottomUntil(int x) {
933920
public TaintAbstractDomain clone() {
934921
if (isBottom())
935922
return this;
936-
return new TaintAbstractDomain(new ArrayList<>(stack), new HashSet<String>(pushTaintList));
923+
return new TaintAbstractDomain(new ArrayList<>(stack));
937924
}
938925

939926
@Override
@@ -968,4 +955,4 @@ else if (isTop())
968955
return TaintElement.TOP;
969956
return this.stack.get(STACK_LIMIT - 1);
970957
}
971-
}
958+
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ public Set<Statement> getAllSstore() {
7373

7474
return sstores;
7575
}
76-
76+
7777
/**
7878
* Returns a set of all the SHA3 statements in the CFG. SHA3
7979
*
@@ -150,7 +150,7 @@ public Set<Statement> getAllJumps() {
150150

151151
return jumpNodes;
152152
}
153-
153+
154154
/**
155155
* Returns a set of all the JUMPI statements in the CFG.
156156
*

‎src/main/java/it/unipr/cfg/Jumpi.java‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -50,9 +50,10 @@ public <A extends AbstractState<A>> AnalysisState<A> forwardSemantics(AnalysisSt
5050
InterproceduralAnalysis<A> interprocedural, StatementStore<A> expressions) throws SemanticException {
5151

5252
EVMAbstractState valueState = entryState.getState().getDomainInstance(EVMAbstractState.class);
53-
54-
if(valueState == null) return entryState;
55-
53+
54+
if (valueState == null)
55+
return entryState;
56+
5657
// Split here
5758
Set<AbstractStack> trueStacks = new HashSet<>();
5859
Set<AbstractStack> falseStacks = new HashSet<>();

‎src/main/java/it/unipr/checker/TimestampDependencyChecker.java‎

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
package it.unipr.checker;
22

3-
import java.util.Set;
4-
53
import it.unipr.analysis.taint.TaintAbstractDomain;
64
import it.unipr.cfg.Balance;
75
import it.unipr.cfg.Blockhash;
@@ -16,6 +14,7 @@
1614
import it.unive.lisa.checks.semantic.SemanticCheck;
1715
import it.unive.lisa.program.cfg.CFG;
1816
import it.unive.lisa.program.cfg.statement.Statement;
17+
import java.util.Set;
1918

2019
public class TimestampDependencyChecker implements
2120
SemanticCheck<SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> {
@@ -33,21 +32,20 @@ public boolean visit(
3332
CheckToolWithAnalysisResults<
3433
SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool,
3534
CFG graph, Statement node) {
36-
37-
if (node instanceof Timestamp || node instanceof Blockhash || node instanceof Difficulty || node instanceof Balance) {
35+
36+
if (node instanceof Timestamp || node instanceof Blockhash || node instanceof Difficulty
37+
|| node instanceof Balance) {
3838
EVMCFG cfg = ((EVMCFG) graph);
3939
Set<Statement> nsh = cfg.getAllSha3();
4040
Set<Statement> ns = cfg.getAllSstore();
41-
// The function cfg.getAllJumps() returns all jumps, whether being jump or jumpi
42-
// if you want to separete the jumps, a different function need to be done
41+
// The function cfg.getAllJumps() returns all jumps, whether being
42+
// jump or jumpi
43+
// if you want to separete the jumps, a different function need to
44+
// be done
4345
Set<Statement> nj = cfg.getAllJumps();
44-
45-
46+
4647
}
47-
48-
49-
50-
48+
5149
return SemanticCheck.super.visit(tool, graph, node);
5250
}
5351

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

Lines changed: 20 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
package it.unipr.checker;
22

3-
import it.unipr.analysis.AbstractStack;
4-
import it.unipr.analysis.EVMAbstractState;
53
import it.unipr.analysis.MyCache;
6-
import it.unipr.analysis.StackElement;
74
import it.unipr.analysis.taint.TaintAbstractDomain;
85
import it.unipr.analysis.taint.TaintElement;
96
import it.unipr.cfg.EVMCFG;
@@ -45,16 +42,16 @@ public boolean visit(
4542
AnalysisState<SimpleAbstractState<MonolithicHeap, TaintAbstractDomain,
4643
TypeEnvironment<InferredTypes>>> analysisResult = null;
4744

48-
for(Statement jump: jumps) {
45+
for (Statement jump : jumps) {
4946
try {
5047
analysisResult = result.getAnalysisStateBefore(jump);
5148
} catch (SemanticException e1) {
5249
log.error("(TxOriginChecker): {}", e1.getMessage());
5350
}
54-
51+
5552
// Retrieve the symbolic stack from the analysis result
5653
TaintAbstractDomain taintedStack = analysisResult.getState().getValueState();
57-
54+
5855
// If the stack is bottom, the jump is definitely
5956
// unreachable
6057
if (taintedStack.isBottom())
@@ -63,36 +60,38 @@ public boolean visit(
6360
else {
6461
TaintElement firstStackElement = taintedStack.getFirstElement();
6562
TaintElement secondStackElement = taintedStack.getSecondElement();
66-
if(secondStackElement.isBottom())
63+
if (secondStackElement.isBottom())
6764
// Nothing to do
6865
continue;
6966
else {
70-
// Checks if either first or second element in the stack is tainted
71-
if(firstStackElement.isTaint() || secondStackElement.isTaint()) {
67+
// Checks if either first or second element in the
68+
// stack is tainted
69+
if (firstStackElement.isTaint() || secondStackElement.isTaint()) {
7270
checkForTxOrigin(origin, jump, tool, cfg);
7371
}
7472
}
7573
}
76-
}
74+
}
7775
}
7876

7977
}
8078

8179
return true;
8280
}
83-
81+
8482
private void checkForTxOrigin(Statement origin, Statement jump, CheckToolWithAnalysisResults<
85-
SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool, EVMCFG cfg) {
86-
if (cfg.reachableFrom(origin, jump)) {
87-
ProgramCounterLocation jumploc = (ProgramCounterLocation) jump.getLocation();
83+
SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool,
84+
EVMCFG cfg) {
85+
if (cfg.reachableFrom(origin, jump)) {
86+
ProgramCounterLocation jumploc = (ProgramCounterLocation) jump.getLocation();
8887

89-
log.debug("Tx. Origin attack at {} at line no. {} coming from line {}", jumploc.getPc(),
90-
jumploc.getSourceCodeLine(),
91-
((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine());
88+
log.debug("Tx. Origin attack at {} at line no. {} coming from line {}", jumploc.getPc(),
89+
jumploc.getSourceCodeLine(),
90+
((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine());
9291

93-
String warn = "TxOrigin attack at " + ((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine();
94-
tool.warn(warn);
95-
MyCache.getInstance().addTxOriginWarning(cfg.hashCode(), warn);
96-
}
92+
String warn = "TxOrigin attack at " + ((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine();
93+
tool.warn(warn);
94+
MyCache.getInstance().addTxOriginWarning(cfg.hashCode(), warn);
95+
}
9796
}
9897
}

0 commit comments

Comments
 (0)