Skip to content

Commit 9852eed

Browse files
committed
Adding support for checker about error handling issues in blockchain software
1 parent 30f81ad commit 9852eed

30 files changed

+1373
-142
lines changed

go-lisa/go-testcases/unhandled-errors/cosmos-gravity-bridge-abci.go

Lines changed: 390 additions & 0 deletions
Large diffs are not rendered by default.
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package distribution
2+
3+
import (
4+
"time"
5+
6+
"github.com/cosmos/cosmos-sdk/telemetry"
7+
sdk "github.com/cosmos/cosmos-sdk/types"
8+
"github.com/cosmos/cosmos-sdk/x/distribution/keeper"
9+
"github.com/cosmos/cosmos-sdk/x/distribution/types"
10+
)
11+
12+
13+
func BeginBlocker(ctx sdk.Context, k keeper.Keeper) error {
14+
15+
panic("PANIC AT THE DISCO!")
16+
17+
return nil
18+
}
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
package distribution
2+
3+
import (
4+
"time"
5+
6+
"github.com/cosmos/cosmos-sdk/telemetry"
7+
sdk "github.com/cosmos/cosmos-sdk/types"
8+
"github.com/cosmos/cosmos-sdk/x/distribution/keeper"
9+
"github.com/cosmos/cosmos-sdk/x/distribution/types"
10+
)
11+
12+
13+
func BeginBlocker(ctx sdk.Context, k keeper.Keeper) error {
14+
15+
defer func() {
16+
if r := recover(); r != nil {
17+
fmt.Println("Handle panic")
18+
}
19+
}()
20+
21+
panic("PANIC AT THE DISCO!")
22+
23+
return nil
24+
}

go-lisa/go-testcases/unhandled-errors/unhandled-errors.go renamed to go-lisa/go-testcases/unhandled-errors/hf-unhandled-errors.go

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ func (t *SimpleAsset) Invoke(stub shim.ChaincodeStubInterface) peer.Response {
1616

1717
value1, _ := stub.GetState(args[0]) // KO: error is discarded
1818

19+
stub.PutState(args[0], []byte("ASD")) // KO: error is discarded
20+
1921
value2, err := stub.GetState(args[1]) // KO: error is not handled
2022

2123
return shim.Success([]byte("Hello!"))

go-lisa/src/main/java/it/unive/golisa/GoLiSA.java

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package it.unive.golisa;
22

33
import it.unive.golisa.analysis.GoIntervalDomain;
4+
import it.unive.golisa.analysis.DummyDomain;
45
import it.unive.golisa.analysis.entrypoints.EntryPointsFactory;
56
import it.unive.golisa.analysis.entrypoints.EntryPointsUtils;
67
import it.unive.golisa.analysis.ni.IntegrityNIDomain;
@@ -11,6 +12,7 @@
1112
import it.unive.golisa.checker.IntegrityNIChecker;
1213
import it.unive.golisa.checker.NumericalOverflowOfVariablesChecker;
1314
import it.unive.golisa.checker.TaintChecker;
15+
import it.unive.golisa.checker.cosmos.panic.ABCIPanicChecker;
1416
import it.unive.golisa.checker.hf.CrossChannelInvocationsIssuesChecker;
1517
import it.unive.golisa.checker.hf.UnhandledErrorsChecker;
1618
import it.unive.golisa.checker.hf.readwrite.ReadWritePairChecker;
@@ -201,6 +203,9 @@ public static void main(String[] args) throws AnalysisSetupException {
201203
break;
202204
case "unhandled-errors":
203205
conf.syntacticChecks.add(new UnhandledErrorsChecker());
206+
conf.abstractState = new SimpleAbstractState<>(new PointBasedHeap(), new ValueEnvironment<>(new DummyDomain()),
207+
new TypeEnvironment<>(new InferredTypes()));
208+
conf.semanticChecks.add(new ABCIPanicChecker());
204209
break;
205210
case "numerical-issues":
206211
conf.openCallPolicy = RelaxedOpenCallPolicy.INSTANCE;
@@ -287,6 +292,12 @@ private static void lisaExecution(String filePath, AnnotationSet[] annotationSet
287292
if(analysis.equals("numerical-issues") || analysis.equals("div-by-zero"))
288293
for (CFG c : program.getAllCFGs())
289294
program.addEntryPoint(c);
295+
296+
if(analysis.equals("unhandled-errors") && framework.equalsIgnoreCase("COSMOS-SDK"))
297+
for (CFG c : program.getAllCFGs())
298+
if(c.getDescriptor().getSignature().contains("BeginBlocker")
299+
|| c.getDescriptor().getSignature().contains("EndBlocker"))
300+
program.addEntryPoint(c);
290301

291302
if (!program.getEntryPoints().isEmpty()) {
292303
conf.interproceduralAnalysis = new ContextBasedAnalysis<>(FullStackToken.getSingleton());
Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
package it.unive.golisa.analysis;
2+
3+
import it.unive.lisa.analysis.SemanticException;
4+
import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
5+
import it.unive.lisa.util.representation.StringRepresentation;
6+
import it.unive.lisa.util.representation.StructuredRepresentation;
7+
8+
public class DummyDomain implements BaseNonRelationalValueDomain<DummyDomain>, Comparable<DummyDomain>{
9+
10+
private static final DummyDomain dummy = new DummyDomain();
11+
private final byte id;
12+
13+
14+
public DummyDomain() {
15+
id = 0;
16+
}
17+
18+
@Override
19+
public DummyDomain lubAux(DummyDomain other) throws SemanticException {
20+
return dummy;
21+
}
22+
23+
@Override
24+
public boolean lessOrEqualAux(DummyDomain other) throws SemanticException {
25+
return false;
26+
}
27+
28+
@Override
29+
public DummyDomain top() {
30+
return dummy;
31+
}
32+
33+
@Override
34+
public DummyDomain bottom() {
35+
return dummy;
36+
}
37+
38+
@Override
39+
public StructuredRepresentation representation() {
40+
return new StringRepresentation("dummy");
41+
}
42+
43+
@Override
44+
public int compareTo(DummyDomain o) {
45+
return 0;
46+
}
47+
48+
}
Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
package it.unive.golisa.cfg.expression;
2+
3+
import it.unive.lisa.analysis.AbstractState;
4+
import it.unive.lisa.analysis.AnalysisState;
5+
import it.unive.lisa.analysis.SemanticException;
6+
import it.unive.lisa.analysis.StatementStore;
7+
import it.unive.lisa.analysis.lattices.ExpressionSet;
8+
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
9+
import it.unive.lisa.program.cfg.CFG;
10+
import it.unive.lisa.program.cfg.CodeLocation;
11+
import it.unive.lisa.program.cfg.statement.Expression;
12+
import it.unive.lisa.program.cfg.statement.NaryExpression;
13+
import it.unive.lisa.program.cfg.statement.Statement;
14+
import it.unive.lisa.symbolic.SymbolicExpression;
15+
16+
/**
17+
* A Go panic expression (e.g., panic("Error!")).
18+
*
19+
* @author <a href="mailto:[email protected]">Luca Olivieri</a>
20+
*/
21+
public class GoPanic extends NaryExpression {
22+
23+
24+
/**
25+
* Builds the make expression.
26+
*
27+
* @param cfg the {@link CFG} where this expression lies
28+
* @param location the location where this expression is defined
29+
* @param type the type to allocate
30+
* @param parameters the parameters
31+
*/
32+
public GoPanic(CFG cfg, CodeLocation location, Expression[] parameters) {
33+
super(cfg, location, "panic", parameters);
34+
}
35+
36+
@Override
37+
public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
38+
InterproceduralAnalysis<A> interprocedural, AnalysisState<A> state,
39+
ExpressionSet[] params, StatementStore<A> expressions)
40+
throws SemanticException {
41+
42+
AnalysisState<A> result = state;
43+
for(ExpressionSet set : params) {
44+
for(SymbolicExpression exp : set)
45+
result =result.lub(result.smallStepSemantics(exp, this));
46+
}
47+
48+
return result;
49+
}
50+
51+
@Override
52+
protected int compareSameClassAndParams(Statement o) {
53+
return 0; // nothing else to compare
54+
}
55+
}
Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
package it.unive.golisa.cfg.expression;
2+
3+
import it.unive.lisa.analysis.AbstractState;
4+
import it.unive.lisa.analysis.AnalysisState;
5+
import it.unive.lisa.analysis.SemanticException;
6+
import it.unive.lisa.analysis.StatementStore;
7+
import it.unive.lisa.analysis.lattices.ExpressionSet;
8+
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
9+
import it.unive.lisa.program.cfg.CFG;
10+
import it.unive.lisa.program.cfg.CodeLocation;
11+
import it.unive.lisa.program.cfg.statement.Expression;
12+
import it.unive.lisa.program.cfg.statement.NaryExpression;
13+
import it.unive.lisa.program.cfg.statement.Statement;
14+
import it.unive.lisa.symbolic.SymbolicExpression;
15+
16+
/**
17+
* A Go recover expression (e.g., recover()).
18+
*
19+
* @author <a href="mailto:[email protected]">Luca Olivieri</a>
20+
*/
21+
public class GoRecover extends NaryExpression {
22+
23+
24+
/**
25+
* Builds the make expression.
26+
*
27+
* @param cfg the {@link CFG} where this expression lies
28+
* @param location the location where this expression is defined
29+
* @param type the type to allocate
30+
* @param parameters the parameters
31+
*/
32+
public GoRecover(CFG cfg, CodeLocation location) {
33+
super(cfg, location, "recover");
34+
}
35+
36+
@Override
37+
public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
38+
InterproceduralAnalysis<A> interprocedural, AnalysisState<A> state,
39+
ExpressionSet[] params, StatementStore<A> expressions)
40+
throws SemanticException {
41+
42+
AnalysisState<A> result = state;
43+
for(ExpressionSet set : params) {
44+
for(SymbolicExpression exp : set)
45+
result =result.lub(result.smallStepSemantics(exp, this));
46+
}
47+
48+
return result;
49+
}
50+
51+
@Override
52+
protected int compareSameClassAndParams(Statement o) {
53+
return 0; // nothing else to compare
54+
}
55+
}
Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
package it.unive.golisa.cfg.runtime.io.type.copy;
2+
3+
import it.unive.golisa.cfg.type.composite.GoStructType;
4+
import it.unive.golisa.golang.util.GoLangUtils;
5+
import it.unive.lisa.program.ClassUnit;
6+
import it.unive.lisa.program.CompilationUnit;
7+
import it.unive.lisa.program.Program;
8+
9+
/**
10+
* A PipeReader type.
11+
*
12+
* @link https://pkg.go.dev/io#PipeReader
13+
*
14+
* @author <a href="mailto:[email protected]">Luca Olivieri</a>
15+
*/
16+
public class PipeReader extends GoStructType {
17+
18+
/**
19+
* Unique instance of PipeReader.
20+
*/
21+
private static PipeReader INSTANCE;
22+
23+
private PipeReader(CompilationUnit unit) {
24+
super("PipeReader", unit);
25+
}
26+
27+
@Override
28+
public String toString() {
29+
return "io.PipeReader";
30+
}
31+
32+
@Override
33+
public boolean equals(Object other) {
34+
return this == other;
35+
}
36+
37+
@Override
38+
public int hashCode() {
39+
return System.identityHashCode(this);
40+
}
41+
42+
/**
43+
* Yields the {@link PipeReader} type.
44+
*
45+
* @param program the program to which this type belongs
46+
*
47+
* @return the {@link PipeReader} type
48+
*/
49+
public static PipeReader getPipeReaderType(Program program) {
50+
if (INSTANCE == null) {
51+
ClassUnit pipeReaderUnit = new ClassUnit(GoLangUtils.GO_RUNTIME_SOURCECODE_LOCATION, program, "PipeReader",
52+
false);
53+
INSTANCE = new PipeReader(pipeReaderUnit);
54+
}
55+
56+
return INSTANCE;
57+
}
58+
}
Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
package it.unive.golisa.cfg.runtime.io.type.copy;
2+
3+
import it.unive.golisa.cfg.type.composite.GoStructType;
4+
import it.unive.golisa.golang.util.GoLangUtils;
5+
import it.unive.lisa.program.ClassUnit;
6+
import it.unive.lisa.program.CompilationUnit;
7+
import it.unive.lisa.program.Program;
8+
9+
/**
10+
* A PipeWriter type.
11+
*
12+
* @link https://pkg.go.dev/io#PipeWriter
13+
*
14+
* @author <a href="mailto:[email protected]">Luca Olivieri</a>
15+
*/
16+
public class PipeWriter extends GoStructType {
17+
18+
/**
19+
* Unique instance of {@link PipeWriter} type.
20+
*/
21+
private static PipeWriter INSTANCE;
22+
23+
private PipeWriter(String name, CompilationUnit unit) {
24+
super(name, unit);
25+
}
26+
27+
@Override
28+
public String toString() {
29+
return "io.PipeWriter";
30+
}
31+
32+
@Override
33+
public boolean equals(Object other) {
34+
return this == other;
35+
}
36+
37+
@Override
38+
public int hashCode() {
39+
return System.identityHashCode(this);
40+
}
41+
42+
/**
43+
* Yields the {@link PipeWriter} type.
44+
*
45+
* @param program the program to which this type belongs
46+
*
47+
* @return the {@link PipeWriter} type
48+
*/
49+
public static PipeWriter getPipeWriterType(Program program) {
50+
if (INSTANCE == null) {
51+
ClassUnit pipeWriterUnit = new ClassUnit(GoLangUtils.GO_RUNTIME_SOURCECODE_LOCATION, program, "PipeWriter",
52+
false);
53+
INSTANCE = new PipeWriter("PipeWriter", pipeWriterUnit);
54+
}
55+
56+
return INSTANCE;
57+
}
58+
}

0 commit comments

Comments
 (0)