Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change getInitialTransitions() to return all initial transitions #495

Merged
merged 1 commit into from
Dec 5, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading