Skip to content

Commit

Permalink
Fixes the failing tests mentioned in issue #97
Browse files Browse the repository at this point in the history 
Signed-off-by: Rakshit Krishnappa Ravi <rakshitkrishnapparavi@gmail.com>

- generates seed for assignment statements with static field from CrySL ruleclass
- fixed ensuresPred method to handle seeds with static field assignment
  • Loading branch information
@rakshitkr
rakshitkr committed Aug 10, 2020
1 parent c013f5f commit b1cee5b
Show file tree
Hide file tree
Showing 3 changed files with 124 additions and 5 deletions.
75 changes: 74 additions & 1 deletion CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,22 @@
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.stream.Collectors;

import com.google.common.collect.HashMultimap;
import com.google.common.collect.Lists;
import com.google.common.collect.Maps;
import com.google.common.collect.Multimap;
import com.google.common.collect.Sets;
import com.google.common.collect.Table;
import com.google.common.collect.Table.Cell;

import boomerang.WeightedForwardQuery;
import boomerang.callgraph.ObservableICFG;
import boomerang.debugger.Debugger;
import boomerang.jimple.AllocVal;
Expand Down Expand Up @@ -46,7 +50,10 @@
import ideal.IDEALSeedSolver;
import soot.IntType;
import soot.Local;
import soot.MethodOrMethodContext;
import soot.RefType;
import soot.Scene;
import soot.SootClass;
import soot.SootMethod;
import soot.Type;
import soot.Unit;
Expand All @@ -56,9 +63,14 @@
import soot.jimple.Constant;
import soot.jimple.IntConstant;
import soot.jimple.InvokeExpr;
import soot.jimple.StaticFieldRef;
import soot.jimple.Stmt;
import soot.jimple.StringConstant;
import soot.jimple.ThrowStmt;
import soot.jimple.internal.JAssignStmt;
import soot.jimple.internal.JStaticInvokeExpr;
import soot.jimple.toolkits.callgraph.ReachableMethods;
import soot.util.queue.QueueReader;
import sync.pds.solver.nodes.Node;
import typestate.TransitionFunction;
import typestate.finiteautomata.ITransition;
Expand Down Expand Up @@ -255,6 +267,51 @@ private void ensuresPred(CrySLPredicate predToBeEnsured, Statement currStmt, Sta
expectPredicateWhenThisObjectIsInState(stateNode, currStmt, predToBeEnsured, satisfiesConstraintSytem);
}
}

Stmt stmt1 = currStmt.getUnit().get();
if(stmt1 instanceof AssignStmt && ((AssignStmt) stmt1).getRightOp() instanceof StaticFieldRef) {
AssignStmt stmt = (AssignStmt) stmt1;
StaticFieldRef value = (StaticFieldRef) stmt.getRightOp();
SootClass dClass = value.getFieldRef().declaringClass();
ReachableMethods rm = Scene.v().getReachableMethods();
QueueReader<MethodOrMethodContext> listener = rm.listener();
while (listener.hasNext()) {
MethodOrMethodContext next = listener.next();
SootMethod m = next.method();
if(m.getDeclaringClass().equals(dClass) && m.getName().equals("<clinit>")) {
Collection<WeightedForwardQuery<TransitionFunction>> nestedSeeds = new HashSet<>();
if (!m.hasActiveBody())
return;
SootMethod method;
if((method = findSeedSource(m, value)) != null) {
Collection<CrySLMethod> convert = CrySLMethodToSootMethod.v().convert(method);

for (CrySLMethod crySLMethod : convert) {
Entry<String, String> retObject = crySLMethod.getRetObject();
if (!retObject.getKey().equals("_") && currStmt.getUnit().get() instanceof AssignStmt && predicateParameterEquals(predToBeEnsured.getParameters(), retObject.getKey())) {
Value leftOp = stmt.getLeftOp();
AllocVal val = new AllocVal(leftOp, currStmt.getMethod(), stmt.getRightOp(), new Statement(stmt, currStmt.getMethod()));
expectPredicateOnOtherObject(predToBeEnsured, currStmt, val, satisfiesConstraintSytem);
}
// This is useless because of absence of invoke expression in currStmt
// int i = 0;
// for (Entry<String, String> p : crySLMethod.getParameters()) {
// if (predicateParameterEquals(predToBeEnsured.getParameters(), p.getKey())) {
//// Value param = ie.getArg(i);
//// if (param instanceof Local) {
//// Val val = new Val(param, currStmt.getMethod());
//// expectPredicateOnOtherObject(predToBeEnsured, currStmt, val, satisfiesConstraintSytem);
//// }
// }
// i++;
// }

}
}
}
}
}

if (currStmt.isCallsite()) {
InvokeExpr ie = ((Stmt) currStmt.getUnit().get()).getInvokeExpr();
SootMethod invokedMethod = ie.getMethod();
Expand All @@ -281,9 +338,25 @@ private void ensuresPred(CrySLPredicate predToBeEnsured, Statement currStmt, Sta
}

}

}
}

private SootMethod findSeedSource(SootMethod m, Value value) {
for (Unit u : m.getActiveBody().getUnits()) {
if(u instanceof JAssignStmt) {
Value val = ((AssignStmt) u).getLeftOp();
if(val.toString().equals(value.toString())) {
Value rval = ((AssignStmt) u).getRightOp();
if(rval instanceof JStaticInvokeExpr) {
SootMethod calledMethod = ((JStaticInvokeExpr) rval).getMethod();
return calledMethod;
}
return findSeedSource(m, rval);
}
}
}
return null;
}

private boolean predicateParameterEquals(List<ICrySLPredicateParameter> parameters, String key) {
for (ICrySLPredicateParameter predicateParam : parameters) {
Expand Down
51 changes: 50 additions & 1 deletion ...oAnalysis/src/main/java/crypto/typestate/FiniteStateMachineToTypestateChangeFunction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,22 @@
import boomerang.WeightedForwardQuery;
import boomerang.jimple.AllocVal;
import boomerang.jimple.Statement;
import soot.MethodOrMethodContext;
import soot.RefType;
import soot.Scene;
import soot.SootClass;
import soot.SootMethod;
import soot.Unit;
import soot.Value;
import soot.jimple.AssignStmt;
import soot.jimple.InstanceInvokeExpr;
import soot.jimple.InvokeExpr;
import soot.jimple.StaticFieldRef;
import soot.jimple.Stmt;
import soot.jimple.internal.JAssignStmt;
import soot.jimple.internal.JStaticInvokeExpr;
import soot.jimple.toolkits.callgraph.ReachableMethods;
import soot.util.queue.QueueReader;
import typestate.TransitionFunction;
import typestate.finiteautomata.MatcherTransition;
import typestate.finiteautomata.State;
Expand Down Expand Up @@ -49,10 +58,30 @@ public FiniteStateMachineToTypestateChangeFunction(SootBasedStateMachineGraph fs
this.fsm = fsm;
}


@Override
public Collection<WeightedForwardQuery<TransitionFunction>> generateSeed(SootMethod method, Unit unit) {
Set<WeightedForwardQuery<TransitionFunction>> out = new HashSet<>();

if(unit instanceof AssignStmt && ((AssignStmt) unit).getRightOp() instanceof StaticFieldRef) {
AssignStmt stmt = (AssignStmt) unit;
StaticFieldRef value = (StaticFieldRef) stmt.getRightOp();
SootClass dClass = value.getFieldRef().declaringClass();
ReachableMethods rm = Scene.v().getReachableMethods();
QueueReader<MethodOrMethodContext> listener = rm.listener();
while (listener.hasNext()) {
MethodOrMethodContext next = listener.next();
SootMethod m = next.method();
if(m.getDeclaringClass().equals(dClass) && m.getName().equals("<clinit>")) {
Collection<WeightedForwardQuery<TransitionFunction>> nestedSeeds = new HashSet<>();
if (!m.hasActiveBody())
return out;

if(findSeedSource(m, value))
out.add(createQuery(stmt,method,new AllocVal(stmt.getLeftOp(), method, stmt.getRightOp(), new Statement(stmt,method))));
}
}
}

if (!(unit instanceof Stmt) || !((Stmt) unit).containsInvokeExpr())
return out;
InvokeExpr invokeExpr = ((Stmt) unit).getInvokeExpr();
Expand All @@ -71,6 +100,26 @@ public Collection<WeightedForwardQuery<TransitionFunction>> generateSeed(SootMet
return out;
}

private boolean findSeedSource(SootMethod m, Value value) {
for (Unit u : m.getActiveBody().getUnits()) {
if(u instanceof JAssignStmt) {
Value val = ((AssignStmt) u).getLeftOp();
if(val.toString().equals(value.toString())) {
Value rval = ((AssignStmt) u).getRightOp();
if(rval instanceof JStaticInvokeExpr) {
SootMethod calledMethod = ((JStaticInvokeExpr) rval).getMethod();
if (fsm.initialTransitonLabel().contains(calledMethod))
return true;
else
return false;
}
return findSeedSource(m, rval);
}
}
}
return false;
}

private WeightedForwardQuery<TransitionFunction> createQuery(Unit unit, SootMethod method, AllocVal allocVal) {
return new WeightedForwardQuery<TransitionFunction>(new Statement((Stmt)unit,method), allocVal, fsm.getInitialWeight(new Statement((Stmt)unit,method)));
}
Expand Down
3 changes: 0 additions & 3 deletions CryptoAnalysis/src/test/java/test/UsagePatternTestingFramework.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -367,9 +367,6 @@ private List<CrySLRule> getRules() {
@Override
public List<String> excludedPackages() {
List<String> excludedPackages = super.excludedPackages();
for(CrySLRule r : getRules()) {
excludedPackages.add(r.getClassName());
}
return excludedPackages;
}

Expand Down

0 comments on commit b1cee5b

Please sign in to comment.