Skip to content

Commit 4c4056a

Browse files
Second Adjustment
2 parents 9a85fac + 9481a69 commit 4c4056a

File tree

9 files changed

+280
-61
lines changed

9 files changed

+280
-61
lines changed

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

Lines changed: 18 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@
2020
import it.unive.lisa.util.representation.StructuredRepresentation;
2121
import java.util.ArrayList;
2222
import java.util.Collections;
23-
import java.util.HashSet;
2423
import java.util.Iterator;
2524
import java.util.List;
2625
import java.util.Set;
@@ -32,10 +31,9 @@ public abstract class TaintAbstractDomain implements ValueDomain<TaintAbstractDo
3231

3332

3433
private final ArrayList<TaintElement> stack;
35-
3634

3735
/**
38-
* Builds a taint abstract stack starting from a given stack and a list of elements that push taint.
36+
* Builds a taint abstract stack starting from a given stack.
3937
*
4038
* @param stack the stack of values
4139
*/
@@ -66,8 +64,12 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
6664

6765
if (op != null) {
6866
switch (op.getClass().getSimpleName()) {
67+
case "OriginOperator": {
68+
TaintAbstractDomain resultStack = clone();
69+
resultStack.push(TaintElement.TAINT);
70+
return resultStack;
71+
}
6972
case "TimestampOperator":
70-
case "OriginOperator":
7173
case "CodesizeOperator":
7274
case "GaspriceOperator":
7375
case "ReturndatasizeOperator":
@@ -92,6 +94,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
9294
resultStack.push(TaintElement.TAINT);
9395
else resultStack.push(TaintElement.CLEAN);
9496
resultStack.toString();
97+
9598
return resultStack;
9699
}
97100

@@ -106,20 +109,20 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
106109
if (hasBottomUntil(1))
107110
return bottom();
108111

112+
109113
TaintAbstractDomain resultStack = clone();
110-
TaintElement opnd1 = resultStack.pop();
111-
114+
resultStack.pop();
115+
112116
return resultStack;
113117
}
114118
case "JumpiOperator": { // JUMPI
115-
116119
if (hasBottomUntil(2))
117120
return bottom();
118121

119122
TaintAbstractDomain resultStack = clone();
120-
TaintElement opnd1 = resultStack.pop();
121-
TaintElement opnd2 = resultStack.pop();
122-
123+
resultStack.pop();
124+
resultStack.pop();
125+
123126
return resultStack;
124127
}
125128

@@ -699,6 +702,7 @@ private TaintAbstractDomain swapX(int x, TaintAbstractDomain stack) {
699702
for (int i = 0; i < clone.size(); i++)
700703
result.add((TaintElement) obj[i]);
701704

705+
702706
return mk(result);
703707
}
704708

@@ -890,9 +894,9 @@ public TaintElement pop() {
890894
* Checks whether between 0 and x-positions of the stack an element is
891895
* bottom. /** Checks whether between 0 and x-positions of the stack an
892896
* element is bottom.
893-
*
897+
*
894898
* @param x the position
895-
*
899+
*
896900
* @return {@code true} if between 0 and x-positions of the stack an element
897901
* is bottom, {@code false} otherwise.
898902
*/
@@ -907,6 +911,7 @@ public boolean hasBottomUntil(int x) {
907911
public TaintAbstractDomain clone() {
908912
if (isBottom())
909913
return this;
914+
910915
return mk(new ArrayList<>(stack));
911916
}
912917

@@ -948,3 +953,4 @@ else if (isTop())
948953
public abstract TaintAbstractDomain mk(ArrayList<TaintElement> list);
949954

950955
}
956+

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
}

src/test/java/it/unipr/analysis/cron/EVMBytecodeGroundTruth.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,8 @@ public void testGroundTruth() throws Exception {
6868

6969
List<String> smartContracts = EVMLiSA.readSmartContractsFromFile(SMARTCONTRACTS_FULLPATH);
7070

71-
ExecutorService executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors());
71+
int cores = Runtime.getRuntime().availableProcessors() / 3 * 2;
72+
ExecutorService executor = Executors.newFixedThreadPool(cores > 0 ? cores : 1);
7273

7374
for (String address : smartContracts) {
7475
executor.submit(() -> {

src/test/java/it/unipr/analysis/cron/EVMBytecodeSmartBugsReentrancyTruth.java

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@
1414
import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
1515
import it.unive.lisa.program.Program;
1616
import java.io.File;
17+
import java.nio.file.Files;
18+
import java.nio.file.Path;
1719
import java.nio.file.Paths;
1820
import java.util.ArrayList;
1921
import java.util.List;
@@ -29,21 +31,26 @@ public class EVMBytecodeSmartBugsReentrancyTruth {
2931

3032
@Ignore
3133
public void testSmartBugsReentrancyTruth() throws Exception {
32-
String SMARTBUGS_BYTECODES_DIR = Paths
33-
.get("evm-testcases", "ground-truth", "test-reentrancy-smartbugs-truth", "bytecode")
34-
.toString();
34+
Path smartbugsBytecodesDirPath = Paths
35+
.get("evm-testcases", "ground-truth", "test-reentrancy-smartbugs-truth", "bytecode");
36+
String SMARTBUGS_BYTECODES_DIR = smartbugsBytecodesDirPath.toString();
3537

3638
EVMFrontend.setUseCreationCode();
3739

3840
List<String> bytecodes = getFileNamesInDirectory(SMARTBUGS_BYTECODES_DIR);
3941

40-
ExecutorService executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors() / 2);
42+
int cores = Runtime.getRuntime().availableProcessors() / 3 * 2;
43+
ExecutorService executor = Executors.newFixedThreadPool(cores > 0 ? cores : 1);
4144

4245
// Run the benchmark in parallel
4346
for (String bytecodeFileName : bytecodes) {
4447
executor.submit(() -> {
4548
try {
46-
String bytecodeFullPath = SMARTBUGS_BYTECODES_DIR + bytecodeFileName;
49+
String bytecodeFullPath = smartbugsBytecodesDirPath.resolve(bytecodeFileName).toString();
50+
51+
String bytecode = new String(Files.readAllBytes(Paths.get(bytecodeFullPath)));
52+
if (bytecode.startsWith("0x"))
53+
EVMFrontend.opcodesFromBytecode(bytecode, bytecodeFullPath);
4754

4855
Program program = EVMFrontend.generateCfgFromFile(bytecodeFullPath);
4956

src/test/java/it/unipr/analysis/cron/EVMBytecodeSolidiFIReentrancyTruth.java

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@
1515
import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
1616
import it.unive.lisa.program.Program;
1717
import java.io.File;
18+
import java.nio.file.Files;
19+
import java.nio.file.Path;
1820
import java.nio.file.Paths;
1921
import java.util.ArrayList;
2022
import java.util.List;
@@ -32,19 +34,26 @@ public class EVMBytecodeSolidiFIReentrancyTruth {
3234
@Test
3335
public void testSolidiFIReentrancyTruth() throws Exception {
3436
setSolidifiMap();
35-
String SOLIDIFI_BYTECODES_DIR = Paths
36-
.get("evm-testcases", "ground-truth", "test-reentrancy-solidifi-truth", "bytecode")
37-
.toString();
3837
EVMFrontend.setUseCreationCode();
38+
39+
Path solidifiBytecodesDirPath = Paths
40+
.get("evm-testcases", "ground-truth", "test-reentrancy-solidifi-truth", "bytecode");
41+
String SOLIDIFI_BYTECODES_DIR = solidifiBytecodesDirPath.toString();
42+
3943
List<String> bytecodes = getFileNamesInDirectory(SOLIDIFI_BYTECODES_DIR);
4044

41-
ExecutorService executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors());
45+
int cores = Runtime.getRuntime().availableProcessors() / 3 * 2;
46+
ExecutorService executor = Executors.newFixedThreadPool(cores > 0 ? cores : 1);
4247

4348
// Run the benchmark
4449
for (String bytecodeFileName : bytecodes) {
4550
executor.submit(() -> {
4651
try {
47-
String bytecodeFullPath = SOLIDIFI_BYTECODES_DIR + bytecodeFileName;
52+
String bytecodeFullPath = solidifiBytecodesDirPath.resolve(bytecodeFileName).toString();
53+
54+
String bytecode = new String(Files.readAllBytes(Paths.get(bytecodeFullPath)));
55+
if (bytecode.startsWith("0x"))
56+
EVMFrontend.opcodesFromBytecode(bytecode, bytecodeFullPath);
4857

4958
Program program = EVMFrontend.generateCfgFromFile(bytecodeFullPath);
5059

0 commit comments

Comments
 (0)