Skip to content

Commit

Permalink
Merge pull request #495 from CROSSINGTUD/issue_322
Browse files Browse the repository at this point in the history
Change getInitialTransitions() to return all initial transitions
  • Loading branch information
schlichtig authored Dec 5, 2023
2 parents 386f925 + 7888dab commit 46ea8c1
Show file tree
Hide file tree
Showing 5 changed files with 412 additions and 24 deletions.
15 changes: 12 additions & 3 deletions CryptoAnalysis/src/main/java/crypto/rules/StateMachineGraph.java
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,17 @@
import crypto.interfaces.FiniteStateMachine;

public final class StateMachineGraph implements FiniteStateMachine<StateNode>, java.io.Serializable {
/**
*
*/

private static final long serialVersionUID = 1L;
private final Set<StateNode> nodes;
private final List<TransitionEdge> edges;
private final List<TransitionEdge> initialEdges;
private int nodeNameCounter = 0;

public StateMachineGraph() {
nodes = new HashSet<StateNode>();
edges = new ArrayList<TransitionEdge>();
initialEdges = new ArrayList<TransitionEdge>();
}

public StateNode createNewNode() {
Expand All @@ -45,6 +45,11 @@ private Boolean addEdge(TransitionEdge edge) {
return false;
}
edges.add(edge);

if (left.isInitialState()) {
initialEdges.add(edge);
}

return true;
}

Expand Down Expand Up @@ -133,6 +138,10 @@ public List<TransitionEdge> getEdges() {
public TransitionEdge getInitialTransition() {
return edges.get(0);
}

public Collection<TransitionEdge> getInitialTransitions() {
return initialEdges;
}

public Collection<StateNode> getAcceptingStates() {
return nodes.parallelStream().filter(node -> node.getAccepting()).collect(Collectors.toList());
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,10 @@ private boolean parametersMatch(List<Entry<String, String>> parameters, List<Typ
for (Type t : parameterTypes) {
if (parameters.get(i).getValue().equals("AnyType"))
continue;
if (!t.toString().equals(parameters.get(i).getValue())) {

// Soot does not track generic types, so we are required to remove <...> from the parameter
String adaptedParameter = parameters.get(i).getValue().replaceAll("[<].*?[>]", "");
if (!t.toString().equals(adaptedParameter)) {
return false;
}
i++;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -54,26 +54,32 @@ public FiniteStateMachineToTypestateChangeFunction(SootBasedStateMachineGraph fs
@Override
public Collection<WeightedForwardQuery<TransitionFunction>> generateSeed(SootMethod method, Unit unit) {
Set<WeightedForwardQuery<TransitionFunction>> out = new HashSet<>();
if (!(unit instanceof Stmt) || !((Stmt) unit).containsInvokeExpr())

if (!(unit instanceof Stmt) || !((Stmt) unit).containsInvokeExpr()) {
return out;
}

InvokeExpr invokeExpr = ((Stmt) unit).getInvokeExpr();
SootMethod calledMethod = invokeExpr.getMethod();
if (!fsm.initialTransitonLabel().contains(calledMethod))

if (!fsm.initialTransitonLabel().contains(calledMethod)) {
return out;
}

if (calledMethod.isStatic()) {
if(unit instanceof AssignStmt){
if (unit instanceof AssignStmt) {
AssignStmt stmt = (AssignStmt) unit;
out.add(createQuery(stmt,method,new AllocVal(stmt.getLeftOp(), method, stmt.getRightOp(), new Statement(stmt,method))));
out.add(createQuery(stmt, method, new AllocVal(stmt.getLeftOp(), method, stmt.getRightOp(), new Statement(stmt, method))));
}
} else if (invokeExpr instanceof InstanceInvokeExpr && !(invokeExpr instanceof InterfaceInvokeExpr)){
InstanceInvokeExpr iie = (InstanceInvokeExpr) invokeExpr;
out.add(createQuery(unit,method,new AllocVal(iie.getBase(), method,iie, new Statement((Stmt) unit,method))));
out.add(createQuery(unit, method, new AllocVal(iie.getBase(), method, iie, new Statement((Stmt) unit, method))));
}
return out;
}

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)));
return new WeightedForwardQuery<TransitionFunction>(new Statement((Stmt) unit, method), allocVal, fsm.getInitialWeight(new Statement((Stmt) unit, method)));
}


Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package crypto.typestate;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
Expand All @@ -17,6 +18,9 @@
import crypto.rules.StateNode;
import crypto.rules.TransitionEdge;
import soot.SootMethod;
import soot.jimple.AssignStmt;
import soot.jimple.InvokeExpr;
import soot.jimple.InvokeStmt;
import typestate.TransitionFunction;
import typestate.finiteautomata.MatcherTransition;
import typestate.finiteautomata.MatcherTransition.Parameter;
Expand All @@ -30,28 +34,36 @@ public class SootBasedStateMachineGraph {

private final StateMachineGraph stateMachineGraph;
private Multimap<State, SootMethod> outTransitions = HashMultimap.create();
private Collection<SootMethod> initialTransitonLabel;
private List<CrySLMethod> crySLinitialTransitionLabel;
private LabeledMatcherTransition initialTransiton;

private Collection<SootMethod> initialTransitionLabels;
private Collection<CrySLMethod> crySLinitialTransitionLabels;
private Collection<LabeledMatcherTransition> initialMatcherTransitions;

public SootBasedStateMachineGraph(StateMachineGraph fsm) {
this.stateMachineGraph = fsm;
// TODO #15 we must start the analysis in state
// stateMachineGraph.getInitialTransition().from();
this.initialTransitionLabels = new ArrayList<>();
this.crySLinitialTransitionLabels = new ArrayList<>();
this.initialMatcherTransitions = new ArrayList<>();

Collection<TransitionEdge> initialTransitions = stateMachineGraph.getInitialTransitions();

for (final TransitionEdge t : stateMachineGraph.getAllTransitions()) {
WrappedState from = wrappedState(t.from());
WrappedState to = wrappedState(t.to());
LabeledMatcherTransition trans = LabeledMatcherTransition.getTransition(from, t.getLabel(),
Parameter.This, to, Type.OnCallOrOnCallToReturn);
this.addTransition(trans);
outTransitions.putAll(from, convert(t.getLabel()));
if (stateMachineGraph.getInitialTransition().equals(t))
this.initialTransiton = trans;

if (initialTransitions.contains(t)) {
initialMatcherTransitions.add(trans);
}
}
crySLinitialTransitionLabel = stateMachineGraph.getInitialTransition().getLabel();

initialTransitonLabel = convert(stateMachineGraph.getInitialTransition().getLabel());
for (TransitionEdge edge : initialTransitions) {
crySLinitialTransitionLabels.addAll(edge.getLabel());
initialTransitionLabels.addAll(convert(edge.getLabel()));
}

// All transitions that are not in the state machine
for (StateNode t : this.stateMachineGraph.getNodes()) {
State wrapped = wrappedState(t);
Expand Down Expand Up @@ -93,18 +105,39 @@ public Collection<SootMethod> getInvolvedMethods() {
}

public TransitionFunction getInitialWeight(Statement stmt) {
return new TransitionFunction(initialTransiton, Collections.singleton(stmt));
TransitionFunction defaultTransition = new TransitionFunction(((ArrayList<LabeledMatcherTransition>) initialMatcherTransitions).get(0), Collections.singleton(stmt));

if (!(stmt.getUnit().get() instanceof InvokeStmt) && !(stmt.getUnit().get() instanceof AssignStmt)) {
return defaultTransition;
}

for (LabeledMatcherTransition trans : initialMatcherTransitions) {
if (stmt.getUnit().get() instanceof InvokeStmt) {
InvokeExpr invokeExpr = stmt.getUnit().get().getInvokeExpr();

if (trans.getMatching(invokeExpr.getMethod()).isPresent()) {
return new TransitionFunction(trans, Collections.singleton(stmt));
}
} else if (stmt.getUnit().get() instanceof AssignStmt) {
InvokeExpr invokeExpr = stmt.getUnit().get().getInvokeExpr();

if (trans.getMatching(invokeExpr.getMethod()).isPresent()) {
return new TransitionFunction(trans, Collections.singleton(stmt));
}
}
}
return defaultTransition;
}

public List<MatcherTransition> getAllTransitions() {
return Lists.newArrayList(transition);
}

public Collection<SootMethod> initialTransitonLabel() {
return Lists.newArrayList(initialTransitonLabel);
return initialTransitionLabels;
}

public List<CrySLMethod> getInitialTransition() {
return crySLinitialTransitionLabel;
public Collection<CrySLMethod> getInitialTransition() {
return crySLinitialTransitionLabels;
}
}
Loading

0 comments on commit 46ea8c1

Please sign in to comment.