Skip to content

Commit

Permalink
Merge pull request #808 from CROSSINGTUD/ideal-clean-up
Browse files Browse the repository at this point in the history 
Include changes and bugfixes from IDEAL
  • Loading branch information
@swissiety
swissiety authored Feb 7, 2025
2 parents cb6dc0e + 1f68393 commit d4b7e63
Show file tree
Hide file tree
Showing 59 changed files with 985 additions and 1,325 deletions.
2 changes: 1 addition & 1 deletion CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ public void registerExpectedPredicate(ExpectedPredicate expectedPredicate) {
}

for (AnalysisSeedWithSpecification seed : scanner.getAnalysisSeedsWithSpec()) {
Collection<Statement> invokedMethods = seed.getInvokedMethods();
Collection<Statement> invokedMethods = seed.getInvokedMethodStatements();

if (invokedMethods.contains(statement)) {
seed.registerExpectedPredicate(predicate);
Expand Down
121 changes: 29 additions & 92 deletions CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
import boomerang.scene.Val;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.Multimap;
import com.google.common.collect.Sets;
import com.google.common.collect.Table;
import crypto.analysis.errors.AbstractConstraintsError;
import crypto.analysis.errors.ForbiddenMethodError;
Expand Down Expand Up @@ -50,9 +49,7 @@ public class AnalysisSeedWithSpecification extends IAnalysisSeed {
private final ConstraintsAnalysis constraintsAnalysis;
private boolean internalConstraintsSatisfied;

private final Multimap<Statement, State> typeStateChange = HashMultimap.create();
private final Map<ControlFlowGraph.Edge, DeclaredMethod> allCallsOnObject;

private final Collection<Statement> allCallsOnObject;
private final Multimap<Statement, Integer> relevantStatements = HashMultimap.create();
private final Collection<AbstractPredicate> indirectlyEnsuredPredicates = new HashSet<>();

Expand All @@ -65,7 +62,7 @@ public AnalysisSeedWithSpecification(
super(scanner, statement, fact, results);

this.specification = specification;
this.allCallsOnObject = results.getInvokedMethodOnInstance();
this.allCallsOnObject = results.getInvokeStatementsOnInstance();

Definitions.ConstraintsDefinition definition =
new Definitions.ConstraintsDefinition(
Expand Down Expand Up @@ -109,15 +106,16 @@ public void execute() {

/** Check the FORBIDDEN section and report corresponding errors */
private void evaluateForbiddenMethods() {
for (Map.Entry<ControlFlowGraph.Edge, DeclaredMethod> calledMethod :
allCallsOnObject.entrySet()) {
Optional<CrySLForbiddenMethod> forbiddenMethod =
isForbiddenMethod(calledMethod.getValue());
for (Statement statement : allCallsOnObject) {
if (!statement.containsInvokeExpr()) {
continue;
}

DeclaredMethod declaredMethod = statement.getInvokeExpr().getMethod();
Optional<CrySLForbiddenMethod> forbiddenMethod = isForbiddenMethod(declaredMethod);

if (forbiddenMethod.isPresent()) {
Collection<CrySLMethod> alternatives = forbiddenMethod.get().getAlternatives();
Statement statement = calledMethod.getKey().getStart();
DeclaredMethod declaredMethod = calledMethod.getValue();

ForbiddenMethodError error =
new ForbiddenMethodError(
Expand All @@ -140,50 +138,29 @@ private Optional<CrySLForbiddenMethod> isForbiddenMethod(DeclaredMethod declared
return Optional.empty();
}

/**
* Check the ORDER section and report a corresponding {@link TypestateError} for each sequence
* of statements that visits a {@link ReportingErrorStateNode}
*/
private void evaluateTypestateOrder() {
Collection<ControlFlowGraph.Edge> allTypestateChangeStatements = new HashSet<>();
for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> cell :
analysisResults.asEdgeValWeightTable().cellSet()) {
Collection<ControlFlowGraph.Edge> edges =
cell.getValue().getLastStateChangeStatements();
allTypestateChangeStatements.addAll(edges);
}

for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> c :
analysisResults.asEdgeValWeightTable().cellSet()) {
ControlFlowGraph.Edge curr = c.getRowKey();

// The initial statement is always the start of the CFG edge, all other statements are
// targets
Statement typestateChangeStatement;
if (curr.getStart().equals(getOrigin())) {
typestateChangeStatement = curr.getStart();
} else {
typestateChangeStatement = curr.getTarget();
}

if (allTypestateChangeStatements.contains(curr)) {
Collection<? extends State> targetStates = getTargetStates(c.getValue());

for (State newStateAtCurr : targetStates) {
typeStateChangeAtStatement(typestateChangeStatement, newStateAtCurr);
for (Statement statement : allCallsOnObject) {
Collection<State> statesAtStatement = getStatesAtStatement(statement);
for (State state : statesAtStatement) {
if (state instanceof ReportingErrorStateNode errorStateNode) {
TypestateError typestateError =
new TypestateError(
this, statement, specification, errorStateNode.expectedCalls());
this.addError(typestateError);
scanner.getAnalysisReporter().reportError(this, typestateError);
}
}
}
}

private void typeStateChangeAtStatement(Statement statement, State stateNode) {
if (typeStateChange.put(statement, stateNode)) {
if (stateNode instanceof ReportingErrorStateNode errorStateNode) {
TypestateError typestateError =
new TypestateError(
this, statement, specification, errorStateNode.expectedCalls());
this.addError(typestateError);
scanner.getAnalysisReporter().reportError(this, typestateError);
}
}
}

/**
* Check the ORDER section and report a corresponding {@link IncompleteOperationError} for each
* sequence of statements that do not end in an accepting state
*/
private void evaluateIncompleteOperations() {
Table<ControlFlowGraph.Edge, Val, TransitionFunction> endPathOfPropagation =
analysisResults.getObjectDestructingStatements();
Expand Down Expand Up @@ -301,7 +278,7 @@ private boolean isMethodToAcceptingState(DeclaredMethod method) {

@Override
public void beforePredicateChecks(Collection<IAnalysisSeed> seeds) {
for (Statement statement : getInvokedMethods()) {
for (Statement statement : getInvokedMethodStatements()) {
relevantStatements.put(statement, -1);
}

Expand Down Expand Up @@ -444,12 +421,7 @@ private void propagatePredicate(
if (allStatesNonGenerating) {
allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateIsNeverReached);
} else if (someStatesNonGenerating) {
/* TODO
* Due to a bug, IDEal returns the states [0,1] whenever there is a
* single call to a method, e.g. Object o = new Object(); o.m();. After
* the call to m1(), o is always in state 0 and 1, although it should only be 1
*/
// allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateMayNotBeReached);
allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateMayNotBeReached);
}

if (isIndirectlyEnsured) {
Expand Down Expand Up @@ -669,31 +641,6 @@ private boolean doesStateGeneratePredicate(State state, CrySLPredicate predicate
&& !isPredicateNegatingState(predicate, state);
}

private Collection<State> getStatesAtStatement(Statement statement) {
Collection<State> states = new HashSet<>();

if (statement.containsInvokeExpr()) {
Collection<TransitionFunction> functions =
statementValWeightTable.row(statement).values();

for (TransitionFunction function : functions) {
Collection<State> targets = getTargetStates(function);

states.addAll(targets);
}
}

return states;
}

private Collection<State> getTargetStates(TransitionFunction value) {
Collection<State> res = Sets.newHashSet();
for (ITransition t : value.values()) {
if (t.to() != null) res.add(t.to());
}
return res;
}

private boolean isPredicateGeneratingState(CrySLPredicate ensPred, State stateNode) {
// Predicate has a condition, i.e. "after" is specified -> Active predicate for
// corresponding states
Expand Down Expand Up @@ -817,20 +764,10 @@ public CrySLRule getSpecification() {
return specification;
}

public Map<ControlFlowGraph.Edge, DeclaredMethod> getAllCallsOnObject() {
public Collection<Statement> getInvokedMethodStatements() {
return allCallsOnObject;
}

public Collection<Statement> getInvokedMethods() {
Collection<Statement> statements = new HashSet<>();

for (ControlFlowGraph.Edge edge : allCallsOnObject.keySet()) {
statements.add(edge.getStart());
}

return statements;
}

public Collection<EnsuredPredicate> getEnsuredPredicatesAtStatement(Statement statement) {
return ensuredPredicates.get(statement);
}
Expand Down
39 changes: 28 additions & 11 deletions CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
package crypto.analysis;

import boomerang.results.ForwardBoomerangResults;
import boomerang.scene.ControlFlowGraph;
import boomerang.scene.Method;
import boomerang.scene.Statement;
import boomerang.scene.Type;
import boomerang.scene.Val;
import com.google.common.collect.HashBasedTable;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.Multimap;
import com.google.common.collect.Table;
Expand All @@ -22,6 +20,8 @@
import java.util.Objects;
import java.util.Optional;
import typestate.TransitionFunction;
import typestate.finiteautomata.ITransition;
import typestate.finiteautomata.State;

public abstract class IAnalysisSeed implements IPredicateCheckListener {

Expand Down Expand Up @@ -49,18 +49,11 @@ public IAnalysisSeed(
this.fact = fact;
this.analysisResults = results;

this.errorCollection = new HashSet<>();

this.statementValWeightTable = HashBasedTable.create();
for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> cell :
results.asEdgeValWeightTable().cellSet()) {
statementValWeightTable.put(
cell.getRowKey().getStart(), cell.getColumnKey(), cell.getValue());
}
this.statementValWeightTable = results.asStatementValWeightTable();

this.errorCollection = new HashSet<>();
this.expectedPredicates = HashMultimap.create();
this.predicateStateChangeListeners = new HashSet<>();

this.ensuredPredicates = HashMultimap.create();
this.unEnsuredPredicates = HashMultimap.create();
}
Expand All @@ -71,6 +64,30 @@ public Collection<Val> getAliasesAtStatement(Statement statement) {
return statementValWeightTable.row(statement).keySet();
}

public Collection<State> getStatesAtStatement(Statement statement) {
Collection<State> states = new HashSet<>();

Collection<TransitionFunction> transitions =
statementValWeightTable.row(statement).values();
for (TransitionFunction transition : transitions) {
Collection<State> targetStates = getTargetStates(transition);

states.addAll(targetStates);
}

return states;
}

private Collection<State> getTargetStates(TransitionFunction transitionFunction) {
Collection<State> states = new HashSet<>();

for (ITransition transition : transitionFunction.values()) {
states.add(transition.to());
}

return states;
}

public void addPredicateStateChangeListener(IPredicateStateChangeListener listener) {
predicateStateChangeListeners.add(listener);
}
Expand Down
33 changes: 7 additions & 26 deletions CryptoAnalysis/src/main/java/crypto/analysis/SeedGenerator.java
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
package crypto.analysis;

import boomerang.results.ForwardBoomerangResults;
import boomerang.scene.CallGraph;
import boomerang.scene.DataFlowScope;
import boomerang.scene.Statement;
import boomerang.scene.Val;
import crypto.definition.Definitions;
import crypto.typestate.ForwardSeedQuery;
import crypto.typestate.TypestateAnalysis;
import crypto.typestate.TypestateDefinition;
import crysl.rule.CrySLRule;
import java.util.Collection;
import java.util.Collections;
Expand All @@ -23,29 +21,12 @@ public class SeedGenerator {
public SeedGenerator(CryptoScanner scanner, Collection<CrySLRule> rules) {
this.scanner = scanner;

TypestateDefinition definition =
new TypestateDefinition() {
@Override
public Collection<CrySLRule> getRuleset() {
return rules;
}

@Override
public CallGraph getCallGraph() {
return scanner.getCallGraph();
}

@Override
public DataFlowScope getDataFlowScope() {
return scanner.getDataFlowScope();
}

@Override
public int getTimeout() {
return scanner.getTimeout();
}
};

Definitions.TypestateDefinition definition =
new Definitions.TypestateDefinition(
rules,
scanner.getCallGraph(),
scanner.getDataFlowScope(),
scanner.getTimeout());
typestateAnalysis = new TypestateAnalysis(definition);
}

Expand Down
7 changes: 1 addition & 6 deletions CryptoAnalysis/src/main/java/crypto/constraints/ConstraintsAnalysis.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package crypto.constraints;

import boomerang.scene.ControlFlowGraph;
import boomerang.scene.Statement;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.Multimap;
Expand Down Expand Up @@ -53,11 +52,7 @@ public void initialize() {

private void initializeCollectedCalls() {
collectedCalls.clear();

Collection<ControlFlowGraph.Edge> edges = seed.getAllCallsOnObject().keySet();
for (ControlFlowGraph.Edge edge : edges) {
collectedCalls.add(edge.getStart());
}
collectedCalls.addAll(seed.getInvokedMethodStatements());
}

private void initializeExtractedValues() {
Expand Down
8 changes: 8 additions & 0 deletions CryptoAnalysis/src/main/java/crypto/definition/Definitions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@
import boomerang.scene.DataFlowScope;
import boomerang.scene.sparse.SparseCFGCache;
import crypto.listener.AnalysisReporter;
import crysl.rule.CrySLRule;
import java.util.Collection;

public interface Definitions {

Expand All @@ -14,6 +16,12 @@ record SeedDefinition(
SparseCFGCache.SparsificationStrategy strategy,
AnalysisReporter reporter) {}

record TypestateDefinition(
Collection<CrySLRule> rules,
CallGraph callGraph,
DataFlowScope dataFlowScope,
int timeout) {}

record ConstraintsDefinition(
CallGraph callGraph,
DataFlowScope dataFlowScope,
Expand Down
Loading

0 comments on commit d4b7e63

Please sign in to comment.