diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AbstractPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/AbstractPredicate.java new file mode 100644 index 000000000..47ae33dc8 --- /dev/null +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AbstractPredicate.java @@ -0,0 +1,37 @@ +package crypto.analysis; + +import crypto.extractparameter.CallSiteWithExtractedValue; +import crysl.rule.CrySLPredicate; +import java.util.Collection; +import java.util.Objects; + +public abstract class AbstractPredicate { + + private final CrySLPredicate predicate; + private final Collection parametersToValues; + + public AbstractPredicate( + CrySLPredicate predicate, Collection parametersToValues) { + this.predicate = predicate; + this.parametersToValues = parametersToValues; + } + + public CrySLPredicate getPredicate() { + return predicate; + } + + public Collection getParametersToValues() { + return parametersToValues; + } + + @Override + public int hashCode() { + return Objects.hash(predicate); + } + + @Override + public boolean equals(Object obj) { + return obj instanceof AbstractPredicate other + && Objects.equals(predicate, other.getPredicate()); + } +} diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java index 21ae0df22..4f5f8684d 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java @@ -105,7 +105,7 @@ public void expectPredicate( } } - public void addEnsuredPredicate(EnsuredCrySLPredicate predicate) { + public void addEnsuredPredicate(AbstractPredicate predicate) { for (Statement statement : expectedPredicates.keySet()) { Collection predicateOnSeeds = expectedPredicates.get(statement); diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index 56d4ae1d6..1db361d42 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -14,7 +14,6 @@ import crypto.analysis.errors.AbstractError; import crypto.analysis.errors.ForbiddenMethodError; import crypto.analysis.errors.IncompleteOperationError; -import crypto.analysis.errors.RequiredPredicateError; import crypto.analysis.errors.TypestateError; import crypto.constraints.ConstraintSolver; import crypto.constraints.EvaluableConstraint; @@ -39,6 +38,7 @@ import java.util.Collections; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Map; import java.util.Objects; import java.util.Optional; @@ -62,7 +62,7 @@ public class AnalysisSeedWithSpecification extends IAnalysisSeed { HashMultimap.create(); private final Multimap> hiddenPredicates = HashMultimap.create(); - private final Collection indirectlyEnsuredPredicates = new HashSet<>(); + private final Collection indirectlyEnsuredPredicates = new HashSet<>(); public AnalysisSeedWithSpecification( CryptoScanner scanner, @@ -122,6 +122,7 @@ private void evaluateForbiddenMethods() { ForbiddenMethodError error = new ForbiddenMethodError( this, statement, specification, declaredMethod, alternatives); + this.addError(error); scanner.getAnalysisReporter().reportError(this, error); } } @@ -356,7 +357,8 @@ private void initializeDependantSeedsFromRequiredPredicates(Collection requiredSeeds = computeRequiredSeeds(statement, base, seeds); for (IAnalysisSeed seed : requiredSeeds) { - seed.expectPredicate(statement, predicate, this, paramIndex); + seed.expectPredicate( + statement, predicate.toNormalCrySLPredicate(), this, paramIndex); if (seed instanceof AnalysisSeedWithSpecification) { ((AnalysisSeedWithSpecification) seed).addRequiringSeed(this); @@ -368,7 +370,8 @@ private void initializeDependantSeedsFromRequiredPredicates(Collection requiredSeeds = computeRequiredSeeds(statement, param, seeds); for (IAnalysisSeed seed : requiredSeeds) { - seed.expectPredicate(statement, predicate, this, paramIndex); + seed.expectPredicate( + statement, predicate.toNormalCrySLPredicate(), this, paramIndex); if (seed instanceof AnalysisSeedWithSpecification) { ((AnalysisSeedWithSpecification) seed).addRequiringSeed(this); @@ -439,7 +442,7 @@ private void initializeDependantSeedsFromEnsuringPredicates(Collection methods = @@ -456,7 +459,8 @@ private void initializeDependantSeedsFromEnsuringPredicates(Collection dependentAssignSeeds = computeGeneratedAssignSeeds(statement, allocVal, seeds); for (IAnalysisSeed seed : dependentAssignSeeds) { - this.expectPredicate(statement, predicate, seed, -1); + this.expectPredicate( + statement, predicate.toNormalCrySLPredicate(), seed, -1); } } @@ -469,7 +473,8 @@ private void initializeDependantSeedsFromEnsuringPredicates(Collection dependantParamSeeds = computeGeneratedParameterSeeds(entry.getKey(), paramVal, seeds); for (IAnalysisSeed seed : dependantParamSeeds) { - this.expectPredicate(statement, predicate, seed, i); + this.expectPredicate( + statement, predicate.toNormalCrySLPredicate(), seed, i); } } } @@ -546,86 +551,87 @@ public void ensurePredicates() { Collection expectedPredStatements = expectedPredicates.keySet(); Collection predsToBeEnsured = new HashSet<>(specification.getPredicates()); - for (EnsuredCrySLPredicate predicate : indirectlyEnsuredPredicates) { + for (AbstractPredicate predicate : indirectlyEnsuredPredicates) { predsToBeEnsured.add(predicate.getPredicate().toNormalCrySLPredicate()); } for (CrySLPredicate predToBeEnsured : predsToBeEnsured) { + Collection violations = new HashSet<>(); - for (Statement statement : expectedPredStatements) { - boolean isPredicateGeneratingStateAvailable = false; + if (errorCollection.stream().anyMatch(e -> e instanceof ForbiddenMethodError)) { + violations.add(HiddenPredicate.Violations.CallToForbiddenMethod); + } + + if (!satisfiesConstraintSystem) { + violations.add(HiddenPredicate.Violations.ConstraintsAreNotSatisfied); + } + + if (predToBeEnsured.getConstraint().isPresent() + && isPredConditionViolated(predToBeEnsured)) { + violations.add(HiddenPredicate.Violations.ConditionIsNotSatisfied); + } + for (Statement statement : expectedPredStatements) { if (!expectedPredicatesAtStatement(statement) .contains(predToBeEnsured.toNormalCrySLPredicate())) { continue; } + /* Check for all states whether an accepting state is reached: + * 1) All states are accepting -> Predicate is generated + * 2) No state is accepting -> Predicate is definitely not generated + * 3) There are generating and non-generating states -> At least one + * dataflow path leads to a non-generating state s.t. the predicate + * is not generated (over approximation) + */ Collection states = getStatesAtStatement(statement); - - for (State state : states) { - // Check, whether the predicate should be generated in state - if (!isPredicateGeneratingState(predToBeEnsured, state)) { - continue; - } - - // Check, whether the predicate is not negated in state - if (isPredicateNegatingState(predToBeEnsured, state)) { - continue; - } - - isPredicateGeneratingStateAvailable = true; - EnsuredCrySLPredicate ensPred; - if (!satisfiesConstraintSystem && predToBeEnsured.getConstraint().isEmpty()) { - // predicate has no condition, but the constraint system is not satisfied - ensPred = - new HiddenPredicate( - predToBeEnsured, - constraintSolver.getCollectedValues(), - this, - HiddenPredicate.HiddenPredicateType - .ConstraintsAreNotSatisfied); - } else if (predToBeEnsured.getConstraint().isPresent() - && isPredConditionViolated(predToBeEnsured)) { - // predicate has condition, but condition is not satisfied - ensPred = - new HiddenPredicate( - predToBeEnsured, - constraintSolver.getCollectedValues(), - this, - HiddenPredicate.HiddenPredicateType - .ConditionIsNotSatisfied); - } else { - // constraints are satisfied and predicate has no condition or the condition - // is satisfied - ensPred = - new EnsuredCrySLPredicate( - predToBeEnsured, constraintSolver.getCollectedValues()); - } - - ensurePredicateAtStatement(ensPred, statement); + boolean allStatesNonGenerating = + states.stream() + .noneMatch(s -> doesStateGeneratePredicate(s, predToBeEnsured)); + boolean someStatesNonGenerating = + states.stream() + .anyMatch(s -> !doesStateGeneratePredicate(s, predToBeEnsured)); + + Collection allViolations = new HashSet<>(violations); + if (allStatesNonGenerating) { + allViolations.add(HiddenPredicate.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(HiddenPredicate.Violations.GeneratingStateMayNotBeReached); } - if (!isPredicateGeneratingStateAvailable) { - /* The predicate is not ensured in any state. However, we propagate a hidden predicate - * for all typestate changing statements because the predicate could have been ensured - * if a generating state had been reached - */ - HiddenPredicate hiddenPredicate = + AbstractPredicate generatedPred; + if (!allViolations.isEmpty()) { + generatedPred = new HiddenPredicate( - predToBeEnsured, + predToBeEnsured.toNormalCrySLPredicate(), constraintSolver.getCollectedValues(), this, - HiddenPredicate.HiddenPredicateType - .GeneratingStateIsNeverReached); - ensurePredicateAtStatement(hiddenPredicate, statement); + allViolations); + } else { + generatedPred = + new EnsuredCrySLPredicate( + predToBeEnsured.toNormalCrySLPredicate(), + constraintSolver.getCollectedValues()); } + + ensurePredicateAtStatement(generatedPred, statement); } } scanner.getAnalysisReporter().ensuredPredicates(this, ensuredPredicates); } - private void ensurePredicateAtStatement(EnsuredCrySLPredicate ensPred, Statement statement) { + private boolean doesStateGeneratePredicate(State state, CrySLPredicate predicate) { + return isPredicateGeneratingState(predicate, state) + && !isPredicateNegatingState(predicate, state); + } + + private void ensurePredicateAtStatement(AbstractPredicate ensPred, Statement statement) { if (hasThisParameter(ensPred.getPredicate())) { this.addEnsuredPredicate(ensPred, statement, -1); scanner.getAnalysisReporter().onGeneratedPredicate(this, ensPred, this, statement); @@ -657,7 +663,7 @@ private void ensurePredicateAtStatement(EnsuredCrySLPredicate ensPred, Statement } private void addEnsuredPredicateFromOtherRule( - EnsuredCrySLPredicate pred, Statement statement, int paramIndex) { + AbstractPredicate pred, Statement statement, int paramIndex) { addEnsuredPredicate(pred, statement, paramIndex); indirectlyEnsuredPredicates.add(pred); } @@ -695,14 +701,14 @@ private Collection getStatesAtStatement(Statement statement) { } public void addEnsuredPredicate( - EnsuredCrySLPredicate ensPred, Statement statement, int paramIndex) { + AbstractPredicate ensPred, Statement statement, int paramIndex) { if (ensPred instanceof HiddenPredicate hiddenPredicate) { Map.Entry predAtIndex = new AbstractMap.SimpleEntry<>(hiddenPredicate, paramIndex); hiddenPredicates.put(statement, predAtIndex); - } else { + } else if (ensPred instanceof EnsuredCrySLPredicate ensuredCrySLPredicate) { Map.Entry predAtIndex = - new AbstractMap.SimpleEntry<>(ensPred, paramIndex); + new AbstractMap.SimpleEntry<>(ensuredCrySLPredicate, paramIndex); ensuredPredicates.put(statement, predAtIndex); } } @@ -806,6 +812,7 @@ private void checkInternalConstraints() { Collection violatedConstraints = constraintSolver.evaluateConstraints(); for (AbstractError violatedConstraint : violatedConstraints) { + this.addError(violatedConstraint); scanner.getAnalysisReporter().reportError(this, violatedConstraint); } @@ -982,37 +989,27 @@ private boolean isPredConditionViolated(CrySLPredicate pred) { .orElse(false); } - public Collection retrieveErrorsForPredCondition(CrySLPredicate pred) { - // Check, whether the predicate has a condition - if (pred.getConstraint().isEmpty()) { - return Collections.emptyList(); - } - - // TODO the condition should be reported itself? - ISLConstraint condition = pred.getConstraint().get(); - return Collections.emptyList(); - } - - private boolean doPredsMatch(CrySLPredicate pred, EnsuredCrySLPredicate ensPred) { + private boolean doPredsMatch(CrySLPredicate pred, AbstractPredicate ensPred) { boolean requiredPredicatesExist = true; for (int i = 0; i < pred.getParameters().size(); i++) { String var = pred.getParameters().get(i).getName(); if (isOfNonTrackableType(var)) { continue; - } else if (pred.getInvolvedVarNames().contains(var)) { + } + if (pred.getInvolvedVarNames().contains(var)) { final String parameterI = ensPred.getPredicate().getParameters().get(i).getName(); Collection actVals = Collections.emptySet(); Collection expVals = Collections.emptySet(); - for (CallSiteWithExtractedValue cswpi : ensPred.getParametersToValues()) { - if (cswpi.callSiteWithParam().varName().equals(parameterI)) { - actVals = retrieveValueFromUnit(cswpi); + for (CallSiteWithExtractedValue callSite : ensPred.getParametersToValues()) { + if (callSite.callSiteWithParam().varName().equals(parameterI)) { + actVals = retrieveValueFromUnit(callSite); } } - for (CallSiteWithExtractedValue cswpi : constraintSolver.getCollectedValues()) { - if (cswpi.callSiteWithParam().varName().equals(var)) { - expVals = retrieveValueFromUnit(cswpi); + for (CallSiteWithExtractedValue callSite : constraintSolver.getCollectedValues()) { + if (callSite.callSiteWithParam().varName().equals(var)) { + expVals = retrieveValueFromUnit(callSite); } } @@ -1041,21 +1038,42 @@ private boolean doPredsMatch(CrySLPredicate pred, EnsuredCrySLPredicate ensPred) return requiredPredicatesExist; } - public void addHiddenPredicatesToError(RequiredPredicateError reqPredError) { - for (CrySLPredicate pred : reqPredError.getContradictedPredicates()) { - Collection hiddenPredicatesEnsuringReqPred = new HashSet<>(); + public Collection extractHiddenPredicates(RequiredCrySLPredicate predicate) { + return extractHiddenPredicates( + predicate.getLocation(), List.of(predicate.getPred()), predicate.getParamIndex()); + } + + public Collection extractHiddenPredicates(AlternativeReqPredicate predicate) { + return extractHiddenPredicates( + predicate.getLocation(), predicate.getAlternatives(), predicate.getParamIndex()); + } - for (Map.Entry entry : hiddenPredicates.values()) { + private Collection extractHiddenPredicates( + Statement statement, Collection predicates, int index) { + Collection result = new HashSet<>(); + + if (!hiddenPredicates.containsKey(statement)) { + return result; + } + + Collection> hiddenPreds = + hiddenPredicates.get(statement); + for (Map.Entry entry : hiddenPreds) { + if (entry.getValue() != index) { + continue; + } + + for (CrySLPredicate pred : predicates) { HiddenPredicate hiddenPredicate = entry.getKey(); if (hiddenPredicate.getPredicate().equals(pred) && doPredsMatch(pred, hiddenPredicate)) { - hiddenPredicatesEnsuringReqPred.add(hiddenPredicate); + result.add(hiddenPredicate); } } - - reqPredError.addHiddenPredicates(hiddenPredicatesEnsuringReqPred); } + + return result; } private Collection retrieveValueFromUnit(CallSiteWithExtractedValue callSite) { @@ -1065,23 +1083,17 @@ private Collection retrieveValueFromUnit(CallSiteWithExtractedValue call if (statement.isAssign()) { Val rightSide = statement.getRightOp(); - if (rightSide.isConstant()) { - values.add(retrieveConstantFromValue(rightSide)); + if (rightSide.isIntConstant()) { + values.add(String.valueOf(rightSide.getIntValue())); + } else if (rightSide.isLongConstant()) { + values.add(String.valueOf(rightSide.getLongValue())); + } else if (rightSide.isStringConstant()) { + values.add(rightSide.getStringValue()); } } return values; } - private String retrieveConstantFromValue(Val val) { - if (val.isStringConstant()) { - return val.getStringValue(); - } else if (val.isIntConstant()) { - return String.valueOf(val.getIntValue()); - } else { - return ""; - } - } - private static final Collection trackedTypes = Arrays.asList("java.lang.String", "int", "java.lang.Integer"); diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java index 974a5b501..f47c82367 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java @@ -5,36 +5,25 @@ import java.util.Collection; import java.util.Objects; -public class EnsuredCrySLPredicate { - - private final CrySLPredicate predicate; - private final Collection parametersToValues; +public class EnsuredCrySLPredicate extends AbstractPredicate { public EnsuredCrySLPredicate( CrySLPredicate predicate, Collection parametersToValues) { - this.predicate = predicate; - this.parametersToValues = parametersToValues; - } - - public CrySLPredicate getPredicate() { - return predicate; - } - - public Collection getParametersToValues() { - return parametersToValues; - } - - public String toString() { - return "Proved " + predicate.getPredName(); + super(predicate, parametersToValues); } @Override public int hashCode() { - return Objects.hash(predicate); + return Objects.hash(super.hashCode()); } @Override public boolean equals(Object obj) { - return obj instanceof EnsuredCrySLPredicate other && predicate.equals(other.predicate); + return super.equals(obj) && obj instanceof EnsuredCrySLPredicate; + } + + @Override + public String toString() { + return "Ensured: " + getPredicate().getPredName(); } } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/HiddenPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/HiddenPredicate.java index 6ecc4cb97..8dd0cf2bb 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/HiddenPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/HiddenPredicate.java @@ -1,122 +1,101 @@ package crypto.analysis; -import com.google.common.collect.Lists; +import crypto.analysis.errors.AbstractConstraintsError; import crypto.analysis.errors.AbstractError; -import crypto.analysis.errors.ConstraintError; -import crypto.analysis.errors.HardCodedError; -import crypto.analysis.errors.ImpreciseValueExtractionError; -import crypto.analysis.errors.IncompleteOperationError; -import crypto.analysis.errors.InstanceOfError; -import crypto.analysis.errors.NeverTypeOfError; -import crypto.analysis.errors.RequiredPredicateError; -import crypto.analysis.errors.TypestateError; +import crypto.analysis.errors.AbstractOrderError; +import crypto.analysis.errors.ForbiddenMethodError; +import crypto.analysis.errors.PredicateConstraintError; import crypto.extractparameter.CallSiteWithExtractedValue; import crysl.rule.CrySLPredicate; import java.util.Collection; -import java.util.stream.Collectors; +import java.util.HashSet; +import java.util.Objects; +import java.util.Set; -public class HiddenPredicate extends EnsuredCrySLPredicate { +public class HiddenPredicate extends AbstractPredicate { private final AnalysisSeedWithSpecification generatingSeed; - private final HiddenPredicateType type; + private final Collection violations; + + public enum Violations { + CallToForbiddenMethod, + ConstraintsAreNotSatisfied, + ConditionIsNotSatisfied, + GeneratingStateMayNotBeReached, + GeneratingStateIsNeverReached + } public HiddenPredicate( CrySLPredicate predicate, Collection parametersToValues, AnalysisSeedWithSpecification generatingSeed, - HiddenPredicateType type) { + Collection violations) { super(predicate, parametersToValues); + this.generatingSeed = generatingSeed; - this.type = type; + this.violations = Set.copyOf(violations); } public AnalysisSeedWithSpecification getGeneratingSeed() { return generatingSeed; } - public enum HiddenPredicateType { - GeneratingStateIsNeverReached, - ConstraintsAreNotSatisfied, - ConditionIsNotSatisfied + public Collection getViolations() { + return violations; } - public HiddenPredicateType getType() { - return type; - } - - /** - * Node: Errors are only in complete count at the end of the analysis. - * - * @return errors list of all preceding errors - */ public Collection getPrecedingErrors() { - Collection results = Lists.newArrayList(); - Collection allErrors = generatingSeed.getErrors(); - switch (type) { - case GeneratingStateIsNeverReached: - Collection typestateErrors = - allErrors.stream() - .filter( - e -> - (e instanceof IncompleteOperationError - || e instanceof TypestateError)) - .collect(Collectors.toList()); - if (typestateErrors.isEmpty()) { - // Seed object has no typestate errors that might be responsible for this hidden - // predicate - // TODO: report new info error type to report, - // that the seeds object could potentially ensure the missing predicate which - // might cause further subsequent errors - // but therefore requires a call to the predicate generating statement - } - - // TODO: check whether the generating state is not reached due to a typestate error - return allErrors; - - case ConstraintsAreNotSatisfied: - // Generating state was reached but constraints are not satisfied. - // Thus, return all constraints & required predicate errors. - return allErrors.stream() - .filter( - e -> - (e instanceof RequiredPredicateError - || e instanceof ConstraintError - || e instanceof HardCodedError - || e instanceof ImpreciseValueExtractionError - || e instanceof InstanceOfError - || e instanceof NeverTypeOfError)) - .collect(Collectors.toList()); - case ConditionIsNotSatisfied: - // Generating state was reached but the predicates condition is not satisfied. - // Thus, return all errors that causes the condition to be not satisfied - Collection precedingErrors = - Lists.newArrayList( - generatingSeed.retrieveErrorsForPredCondition(this.getPredicate())); - // This method is called from a RequiredPredicateError that wants to retrieve its - // preceding errors. - // In this case, preceding errors are not reported yet because the predicate - // condition wasn't required to be satisfied. - // Since the hidden predicate is required to be an ensured predicate, we can assume - // the condition required to be satisfied. - // Thus, we report all errors that causes the condition to be not satisfied. - // precedingErrors.forEach(e -> - // this.generatingSeed.scanner.getAnalysisListener().reportError(generatingSeed, - // e)); - precedingErrors.forEach( - e -> - this.generatingSeed - .scanner - .getAnalysisReporter() - .reportError(generatingSeed, e)); - // Further, preceding errors can be of type RequiredPredicateError. - // Thus, we have to recursively map preceding errors for the newly reported errors. - for (AbstractError e : precedingErrors) { - if (e instanceof RequiredPredicateError) { - ((RequiredPredicateError) e).mapPrecedingErrors(); - } - } - return precedingErrors; + Collection result = new HashSet<>(); + + if (violations.contains(Violations.CallToForbiddenMethod)) { + Collection forbiddenMethodErrors = + generatingSeed.getErrors().stream() + .filter(e -> e instanceof ForbiddenMethodError) + .toList(); + result.addAll(forbiddenMethodErrors); } - return results; + + if (violations.contains(Violations.ConstraintsAreNotSatisfied)) { + Collection constraintErrors = + generatingSeed.getErrors().stream() + .filter(e -> e instanceof AbstractConstraintsError) + .toList(); + result.addAll(constraintErrors); + } + + if (violations.contains(Violations.ConditionIsNotSatisfied)) { + PredicateConstraintError error = + new PredicateConstraintError(generatingSeed, getPredicate()); + result.add(error); + } + + if (violations.contains(Violations.GeneratingStateMayNotBeReached) + || violations.contains(Violations.GeneratingStateIsNeverReached)) { + Collection orderError = + generatingSeed.getErrors().stream() + .filter(e -> e instanceof AbstractOrderError) + .toList(); + result.addAll(orderError); + } + + return result; + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), generatingSeed, violations); + } + + @Override + public boolean equals(Object obj) { + return super.equals(obj) + && obj instanceof HiddenPredicate other + && Objects.equals(generatingSeed, other.getGeneratingSeed()) + && Objects.equals(violations, other.getViolations()); + } + + @Override + public String toString() { + return "Hidden: " + getPredicate().getPredName(); } } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java b/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java index e6750e823..bab7222b9 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java @@ -27,7 +27,6 @@ protected record ExpectedPredicateOnSeed( private final Statement origin; private final Val fact; - private boolean secure = true; public IAnalysisSeed( CryptoScanner scanner, @@ -80,11 +79,7 @@ public Type getType() { } public boolean isSecure() { - return secure; - } - - public void setSecure(boolean secure) { - this.secure = secure; + return errorCollection.isEmpty(); } public ForwardBoomerangResults getAnalysisResults() { diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java b/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java index 98068b080..fc4ba696d 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java @@ -1,5 +1,6 @@ package crypto.analysis; +import crypto.analysis.errors.AbstractError; import crypto.analysis.errors.PredicateContradictionError; import crypto.analysis.errors.RequiredPredicateError; import crysl.rule.ISLConstraint; @@ -23,13 +24,15 @@ public PredicateHandler(CryptoScanner cryptoScanner) { public void checkPredicates() { runPredicateMechanism(); - collectMissingRequiredPredicates(); collectContradictingPredicates(); + collectMissingRequiredPredicates(); reportRequiredPredicateErrors(); + + // Connections are only available once all errors have been reported + connectSubsequentErrors(); } private void runPredicateMechanism() { - for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) { seed.computeExpectedPredicates(cryptoScanner.getDiscoveredSeeds()); } @@ -42,58 +45,68 @@ private void runPredicateMechanism() { } } + private void collectContradictingPredicates() { + for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) { + Collection contradictedPredicates = + seed.computeContradictedPredicates(); + + for (RequiredCrySLPredicate pred : contradictedPredicates) { + PredicateContradictionError error = + new PredicateContradictionError( + seed, pred.getLocation(), seed.getSpecification(), pred.getPred()); + seed.addError(error); + cryptoScanner.getAnalysisReporter().reportError(seed, error); + } + } + } + private void collectMissingRequiredPredicates() { for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) { requiredPredicateErrors.put(seed, new ArrayList<>()); Collection missingPredicates = seed.computeMissingPredicates(); for (ISLConstraint pred : missingPredicates) { - if (pred instanceof RequiredCrySLPredicate) { - RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred; + if (pred instanceof RequiredCrySLPredicate reqPred) { + Collection hiddenPreds = seed.extractHiddenPredicates(reqPred); - RequiredPredicateError reqPredError = new RequiredPredicateError(seed, reqPred); - addRequiredPredicateErrorOnSeed(reqPredError, seed); - } else if (pred instanceof AlternativeReqPredicate) { - AlternativeReqPredicate altReqPred = (AlternativeReqPredicate) pred; + RequiredPredicateError reqPredError = + new RequiredPredicateError(seed, reqPred, hiddenPreds); + requiredPredicateErrors.get(seed).add(reqPredError); + } else if (pred instanceof AlternativeReqPredicate altReqPred) { + Collection hiddenPreds = + seed.extractHiddenPredicates(altReqPred); RequiredPredicateError reqPredError = - new RequiredPredicateError(seed, altReqPred); - addRequiredPredicateErrorOnSeed(reqPredError, seed); + new RequiredPredicateError(seed, altReqPred, hiddenPreds); + requiredPredicateErrors.get(seed).add(reqPredError); } } } } - private void addRequiredPredicateErrorOnSeed( - RequiredPredicateError reqPredError, AnalysisSeedWithSpecification seed) { - seed.addHiddenPredicatesToError(reqPredError); - seed.addError(reqPredError); - requiredPredicateErrors.get(seed).add(reqPredError); - } - private void reportRequiredPredicateErrors() { - for (Map.Entry> entry : - requiredPredicateErrors.entrySet()) { - AnalysisSeedWithSpecification seed = entry.getKey(); + for (AnalysisSeedWithSpecification seed : requiredPredicateErrors.keySet()) { + Collection errors = requiredPredicateErrors.get(seed); - for (RequiredPredicateError reqPredError : entry.getValue()) { - reqPredError.mapPrecedingErrors(); + for (RequiredPredicateError reqPredError : errors) { + seed.addError(reqPredError); cryptoScanner.getAnalysisReporter().reportError(seed, reqPredError); } } } - private void collectContradictingPredicates() { - for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) { - Collection contradictedPredicates = - seed.computeContradictedPredicates(); + private void connectSubsequentErrors() { + for (AnalysisSeedWithSpecification seed : requiredPredicateErrors.keySet()) { + Collection errors = requiredPredicateErrors.get(seed); - for (RequiredCrySLPredicate pred : contradictedPredicates) { - PredicateContradictionError error = - new PredicateContradictionError( - seed, pred.getLocation(), seed.getSpecification(), pred.getPred()); - seed.addError(error); - cryptoScanner.getAnalysisReporter().reportError(seed, error); + for (RequiredPredicateError error : errors) { + for (HiddenPredicate hiddenPredicate : error.getHiddenPredicates()) { + Collection precedingErrors = + hiddenPredicate.getPrecedingErrors(); + + precedingErrors.forEach(error::addPrecedingError); + precedingErrors.forEach(e -> e.addSubsequentError(error)); + } } } } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java index d15e2907d..b52f40f7a 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java @@ -4,7 +4,9 @@ import crypto.analysis.IAnalysisSeed; import crysl.rule.CrySLRule; -/** Super class for all errors that violate a constraint from the CONSTRAINTS section */ +/** + * Super class for all errors that violate a constraint from the CONSTRAINTS and REQUIRES section + */ public abstract class AbstractConstraintsError extends AbstractError { public AbstractConstraintsError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) { diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java index c9171f630..f82a7cd92 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java @@ -16,16 +16,16 @@ public abstract class AbstractError { private final Statement errorStmt; private final CrySLRule rule; - private final Collection causedByErrors; // preceding - private final Collection willCauseErrors; // subsequent + private final Collection precedingErrors; // preceding + private final Collection subsequentErrors; // subsequent public AbstractError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) { this.seed = seed; this.errorStmt = errorStmt; this.rule = rule; - this.causedByErrors = new HashSet<>(); - this.willCauseErrors = new HashSet<>(); + this.precedingErrors = new HashSet<>(); + this.subsequentErrors = new HashSet<>(); } public abstract String toErrorMarkerString(); @@ -50,24 +50,28 @@ public int getLineNumber() { return errorStmt.getStartLineNumber(); } - public void addCausingError(AbstractError parent) { - causedByErrors.add(parent); + public void addPrecedingError(AbstractError error) { + precedingErrors.add(error); } public void addCausingError(Collection parents) { - causedByErrors.addAll(parents); + precedingErrors.addAll(parents); } public void addSubsequentError(AbstractError subsequentError) { - willCauseErrors.add(subsequentError); + subsequentErrors.add(subsequentError); + } + + public Collection getPrecedingErrors() { + return precedingErrors; } public Collection getSubsequentErrors() { - return this.willCauseErrors; + return subsequentErrors; } public Collection getRootErrors() { - return this.causedByErrors; + return this.precedingErrors; } public String toString() { diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractRequiresError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractRequiresError.java deleted file mode 100644 index 353bb21bf..000000000 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractRequiresError.java +++ /dev/null @@ -1,23 +0,0 @@ -package crypto.analysis.errors; - -import boomerang.scene.Statement; -import crypto.analysis.IAnalysisSeed; -import crysl.rule.CrySLRule; - -/** Super class for all errors that violate a constraint from the REQUIRES section */ -public abstract class AbstractRequiresError extends AbstractError { - - public AbstractRequiresError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) { - super(seed, errorStmt, rule); - } - - @Override - public int hashCode() { - return super.hashCode(); - } - - @Override - public boolean equals(Object obj) { - return super.equals(obj); - } -} diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateConstraintError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateConstraintError.java new file mode 100644 index 000000000..764464e4b --- /dev/null +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateConstraintError.java @@ -0,0 +1,59 @@ +package crypto.analysis.errors; + +import crypto.analysis.AnalysisSeedWithSpecification; +import crysl.rule.CrySLPredicate; +import java.util.Objects; + +/** + * This class represents an internal error if the constraint of a predicate to be ensured is + * violated and is only used to propagate HiddenPredicates. For example, we have the following + * ENSURES block: + * + * 
{@code
+ * ENSURES
+ *    algorithm in {"AES"} => generatedKey[...]
+ * }
+ * + * If the algorithm is not "AES", the predicate "generatedKey" is not ensured. Instead, the analysis + * propagates a HiddenPredicate with the cause that the constraint is not satisfied to have a valid + * reason. This class then simply indicates that the predicate's constraint is not satisfied. This + * error is/should be not reported. + */ +public class PredicateConstraintError extends AbstractError { + + private final CrySLPredicate predicate; + + public PredicateConstraintError(AnalysisSeedWithSpecification seed, CrySLPredicate predicate) { + super(seed, seed.getOrigin(), seed.getSpecification()); + + this.predicate = predicate; + } + + public CrySLPredicate getPredicate() { + return predicate; + } + + @Override + public String toErrorMarkerString() { + return "Cannot ensure predicate " + + predicate.getPredName() + + " because its constraint is not satisfied"; + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), predicate); + } + + @Override + public boolean equals(Object obj) { + return super.equals(obj) + && obj instanceof PredicateConstraintError other + && Objects.equals(predicate, other.getPredicate()); + } + + @Override + public String toString() { + return "PredicateConstraintError: " + toErrorMarkerString(); + } +} diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java index 712dc2c9b..fa4375904 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java @@ -6,7 +6,7 @@ import crysl.rule.CrySLRule; import java.util.Objects; -public class PredicateContradictionError extends AbstractRequiresError { +public class PredicateContradictionError extends AbstractConstraintsError { private final CrySLPredicate contradictedPredicate; diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java index 941b44d02..84418eeda 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java @@ -5,44 +5,44 @@ import crypto.analysis.HiddenPredicate; import crypto.analysis.RequiredCrySLPredicate; import crysl.rule.CrySLPredicate; -import java.util.Arrays; import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; +import java.util.List; +import java.util.Objects; +import java.util.Set; import java.util.stream.Collectors; /** * Creates {@link RequiredPredicateError} for all Required Predicate error generates * RequiredPredicateError */ -public class RequiredPredicateError extends AbstractRequiresError { +public class RequiredPredicateError extends AbstractConstraintsError { - private final Collection hiddenPredicates; private final Collection contradictedPredicates; + private final Collection hiddenPredicates; private final int paramIndex; public RequiredPredicateError( - AnalysisSeedWithSpecification seed, RequiredCrySLPredicate violatedPred) { + AnalysisSeedWithSpecification seed, + RequiredCrySLPredicate violatedPred, + Collection hiddenPredicates) { super(seed, violatedPred.getLocation(), seed.getSpecification()); - this.hiddenPredicates = new HashSet<>(); - this.contradictedPredicates = Collections.singletonList(violatedPred.getPred()); + this.hiddenPredicates = Set.copyOf(hiddenPredicates); + this.contradictedPredicates = List.of(violatedPred.getPred()); this.paramIndex = violatedPred.getParamIndex(); } public RequiredPredicateError( - AnalysisSeedWithSpecification seed, AlternativeReqPredicate violatedPred) { + AnalysisSeedWithSpecification seed, + AlternativeReqPredicate violatedPred, + Collection hiddenPredicates) { super(seed, violatedPred.getLocation(), seed.getSpecification()); - this.hiddenPredicates = new HashSet<>(); - this.contradictedPredicates = violatedPred.getAlternatives(); + this.hiddenPredicates = Set.copyOf(hiddenPredicates); + this.contradictedPredicates = List.copyOf(violatedPred.getAlternatives()); this.paramIndex = violatedPred.getParamIndex(); } - public void addHiddenPredicates(Collection hiddenPredicates) { - this.hiddenPredicates.addAll(hiddenPredicates); - } - public void mapPrecedingErrors() { for (HiddenPredicate hiddenPredicate : hiddenPredicates) { Collection precedingErrors = hiddenPredicate.getPrecedingErrors(); @@ -51,11 +51,6 @@ public void mapPrecedingErrors() { } } - /** - * This method returns a list of contradicting predicates - * - * @return list of contradicting predicates - */ public Collection getContradictedPredicates() { return contradictedPredicates; } @@ -85,64 +80,30 @@ public String toErrorMarkerString() { } private String getParamIndexAsText() { - String res; - switch (paramIndex) { - case -1: - return "Return value"; - case 0: - res = "First "; - break; - case 1: - res = "Second "; - break; - case 2: - res = "Third "; - break; - case 3: - res = "Fourth "; - break; - case 4: - res = "Fifth "; - break; - case 5: - res = "Sixth "; - break; - default: - res = (paramIndex + 1) + "th "; - break; - } - res += "parameter"; - return res; + return switch (paramIndex) { + case -1 -> "Return value"; + case 0 -> "First parameter"; + case 1 -> "Second parameter"; + case 2 -> "Third parameter"; + case 3 -> "Fourth parameter"; + case 4 -> "Fifth parameter"; + case 5 -> "Sixth parameter"; + default -> (paramIndex + 1) + "th parameter"; + }; } @Override public int hashCode() { - return Arrays.hashCode( - new Object[] { - super.hashCode(), hiddenPredicates, contradictedPredicates, paramIndex - }); + return Objects.hash(super.hashCode(), hiddenPredicates, contradictedPredicates, paramIndex); } @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (!super.equals(obj)) return false; - if (getClass() != obj.getClass()) return false; - - RequiredPredicateError other = (RequiredPredicateError) obj; - if (hiddenPredicates == null) { - if (other.getHiddenPredicates() != null) return false; - } else if (!hiddenPredicates.equals(other.hiddenPredicates)) { - return false; - } - - if (contradictedPredicates == null) { - if (other.getContradictedPredicates() != null) return false; - } else if (!contradictedPredicates.equals(other.getContradictedPredicates())) { - return false; - } - - return paramIndex == other.getParamIndex(); + return super.equals(obj) + && obj instanceof RequiredPredicateError other + && Objects.equals(contradictedPredicates, other.getContradictedPredicates()) + && Objects.equals(hiddenPredicates, other.getHiddenPredicates()) + && paramIndex == other.getParamIndex(); } @Override diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java b/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java index cac54f0de..7e10c8ed4 100644 --- a/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java +++ b/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java @@ -10,7 +10,6 @@ import java.util.ArrayList; import java.util.List; import java.util.Map; -import java.util.stream.Collectors; public class ValueConstraint extends EvaluableConstraint { @@ -28,9 +27,7 @@ public void evaluate() { } List lowerCaseValues = - valCons.getValueRange().parallelStream() - .map(String::toLowerCase) - .collect(Collectors.toList()); + valCons.getValueRange().parallelStream().map(String::toLowerCase).toList(); for (Map.Entry val : values) { if (!lowerCaseValues.contains(val.getKey().toLowerCase())) { ConstraintError error = diff --git a/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java b/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java index 049f8ffd5..24f0476bc 100644 --- a/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java +++ b/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java @@ -6,6 +6,7 @@ import boomerang.scene.Statement; import boomerang.scene.Val; import com.google.common.collect.Multimap; +import crypto.analysis.AbstractPredicate; import crypto.analysis.EnsuredCrySLPredicate; import crypto.analysis.IAnalysisSeed; import crypto.analysis.errors.AbstractError; @@ -183,7 +184,7 @@ public void afterPredicateCheck() { public void onGeneratedPredicate( IAnalysisSeed fromSeed, - EnsuredCrySLPredicate predicate, + AbstractPredicate predicate, IAnalysisSeed toPred, Statement statement) { for (IResultsListener listener : resultsListeners) { @@ -229,53 +230,36 @@ public void ensuredPredicates( } public void reportError(IAnalysisSeed seed, AbstractError error) { - seed.setSecure(false); - for (IAnalysisListener analysisListener : analysisListeners) { analysisListener.onReportedError(seed, error); } for (IErrorListener errorListener : errorListeners) { - if (error instanceof CallToError) { - CallToError callToError = (CallToError) error; + if (error instanceof CallToError callToError) { errorListener.reportError(callToError); - } else if (error instanceof ConstraintError) { - ConstraintError constraintError = (ConstraintError) error; + } else if (error instanceof ConstraintError constraintError) { errorListener.reportError(constraintError); - } else if (error instanceof ForbiddenMethodError) { - ForbiddenMethodError forbiddenMethodError = (ForbiddenMethodError) error; + } else if (error instanceof ForbiddenMethodError forbiddenMethodError) { errorListener.reportError(forbiddenMethodError); - } else if (error instanceof HardCodedError) { - HardCodedError hardCodedError = (HardCodedError) error; + } else if (error instanceof HardCodedError hardCodedError) { errorListener.reportError(hardCodedError); - } else if (error instanceof ImpreciseValueExtractionError) { - ImpreciseValueExtractionError impreciseError = - (ImpreciseValueExtractionError) error; + } else if (error instanceof ImpreciseValueExtractionError impreciseError) { errorListener.reportError(impreciseError); - } else if (error instanceof IncompleteOperationError) { - IncompleteOperationError incompleteError = (IncompleteOperationError) error; + } else if (error instanceof IncompleteOperationError incompleteError) { errorListener.reportError(incompleteError); - } else if (error instanceof InstanceOfError) { - InstanceOfError instanceOfError = (InstanceOfError) error; + } else if (error instanceof InstanceOfError instanceOfError) { errorListener.reportError(instanceOfError); - } else if (error instanceof NeverTypeOfError) { - NeverTypeOfError neverTypeOfError = (NeverTypeOfError) error; + } else if (error instanceof NeverTypeOfError neverTypeOfError) { errorListener.reportError(neverTypeOfError); - } else if (error instanceof NoCallToError) { - NoCallToError noCallToError = (NoCallToError) error; + } else if (error instanceof NoCallToError noCallToError) { errorListener.reportError(noCallToError); - } else if (error instanceof PredicateContradictionError) { - PredicateContradictionError contradictionError = - (PredicateContradictionError) error; + } else if (error instanceof PredicateContradictionError contradictionError) { errorListener.reportError(contradictionError); - } else if (error instanceof RequiredPredicateError) { - RequiredPredicateError predicateError = (RequiredPredicateError) error; + } else if (error instanceof RequiredPredicateError predicateError) { errorListener.reportError(predicateError); - } else if (error instanceof TypestateError) { - TypestateError typestateError = (TypestateError) error; + } else if (error instanceof TypestateError typestateError) { errorListener.reportError(typestateError); - } else if (error instanceof UncaughtExceptionError) { - UncaughtExceptionError exceptionError = (UncaughtExceptionError) error; + } else if (error instanceof UncaughtExceptionError exceptionError) { errorListener.reportError(exceptionError); } else { errorListener.reportError(error); diff --git a/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java b/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java index aaef32b58..e49ee7fd8 100644 --- a/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java +++ b/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java @@ -5,6 +5,7 @@ import boomerang.scene.CallGraph; import boomerang.scene.Statement; import com.google.common.collect.Multimap; +import crypto.analysis.AbstractPredicate; import crypto.analysis.EnsuredCrySLPredicate; import crypto.analysis.IAnalysisSeed; import crypto.analysis.errors.AbstractError; @@ -36,7 +37,7 @@ void checkedConstraints( void generatedPredicate( IAnalysisSeed fromSeed, - EnsuredCrySLPredicate predicate, + AbstractPredicate predicate, IAnalysisSeed toSeed, Statement statement); diff --git a/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java b/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java index dbaa88eaa..f46171d4a 100644 --- a/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java +++ b/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java @@ -9,6 +9,7 @@ import com.google.common.collect.HashMultimap; import com.google.common.collect.Multimap; import com.google.common.collect.Table; +import crypto.analysis.AbstractPredicate; import crypto.analysis.EnsuredCrySLPredicate; import crypto.analysis.IAnalysisSeed; import crypto.analysis.errors.AbstractError; @@ -102,7 +103,7 @@ public void checkedConstraints( @Override public void generatedPredicate( IAnalysisSeed fromSeed, - EnsuredCrySLPredicate predicate, + AbstractPredicate predicate, IAnalysisSeed toSeed, Statement statement) { for (Assertion a : assertions) { diff --git a/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java index e274a512e..1487a1073 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java @@ -2,7 +2,7 @@ import boomerang.scene.Statement; import boomerang.scene.Val; -import crypto.analysis.EnsuredCrySLPredicate; +import crypto.analysis.AbstractPredicate; import crypto.analysis.HiddenPredicate; import java.util.Collection; import test.Assertion; @@ -38,7 +38,7 @@ public Statement getStmt() { return stmt; } - public void reported(Collection seed, EnsuredCrySLPredicate pred) { + public void reported(Collection seed, AbstractPredicate pred) { if (!seed.contains(val) || pred instanceof HiddenPredicate) { return; } diff --git a/CryptoAnalysis/src/test/java/test/assertions/HasGeneratedPredicateAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/HasGeneratedPredicateAssertion.java index f07a3ca5c..824b90e05 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/HasGeneratedPredicateAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/HasGeneratedPredicateAssertion.java @@ -2,7 +2,7 @@ import boomerang.scene.Statement; import boomerang.scene.Val; -import crypto.analysis.EnsuredCrySLPredicate; +import crypto.analysis.AbstractPredicate; import crypto.analysis.HiddenPredicate; import java.util.Collection; import test.Assertion; @@ -28,7 +28,7 @@ public boolean isImprecise() { return false; } - public void reported(Collection seed, EnsuredCrySLPredicate predicate) { + public void reported(Collection seed, AbstractPredicate predicate) { if (seed.contains(val) && !(predicate instanceof HiddenPredicate)) { satisfied = true; } diff --git a/CryptoAnalysis/src/test/java/test/assertions/HasNotGeneratedPredicateAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/HasNotGeneratedPredicateAssertion.java index d4e309f83..5ee66eed2 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/HasNotGeneratedPredicateAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/HasNotGeneratedPredicateAssertion.java @@ -2,7 +2,7 @@ import boomerang.scene.Statement; import boomerang.scene.Val; -import crypto.analysis.EnsuredCrySLPredicate; +import crypto.analysis.AbstractPredicate; import crypto.analysis.HiddenPredicate; import java.util.Collection; import test.Assertion; @@ -32,7 +32,7 @@ public Statement getStatement() { return statement; } - public void reported(Collection seed, EnsuredCrySLPredicate predicate) { + public void reported(Collection seed, AbstractPredicate predicate) { if (seed.contains(val) && !(predicate instanceof HiddenPredicate)) { imprecise = true; } diff --git a/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java index 55db56df8..6bce7e224 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java @@ -2,7 +2,7 @@ import boomerang.scene.Statement; import boomerang.scene.Val; -import crypto.analysis.EnsuredCrySLPredicate; +import crypto.analysis.AbstractPredicate; import crypto.analysis.HiddenPredicate; import java.util.Collection; import test.Assertion; @@ -38,7 +38,7 @@ public Statement getStmt() { return stmt; } - public void reported(Collection seed, EnsuredCrySLPredicate pred) { + public void reported(Collection seed, AbstractPredicate pred) { if (!seed.contains(val) || pred instanceof HiddenPredicate) { return; } diff --git a/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java b/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java index 658a3a687..7903d79b4 100644 --- a/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java +++ b/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java @@ -112,7 +112,7 @@ protected final void assertErrors( int difference = expected - actual; if (difference < 0) { report.add( - "\n\tFound " + "Found " + Math.abs(difference) + " too many errors of type " + errorType.getSimpleName() @@ -120,7 +120,7 @@ protected final void assertErrors( + methodWrapper); } else if (difference > 0) { report.add( - "\n\tFound " + "Found " + difference + " too few errors of type " + errorType.getSimpleName() @@ -148,7 +148,7 @@ protected final void assertErrors( int unexpectedErrors = getErrorsOfType(errorType, errors); report.add( - "\n\tFound " + "Found " + unexpectedErrors + " too many errors of type " + errorType.getSimpleName() diff --git a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java index f01d1da5f..1f6f07e42 100644 --- a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java +++ b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java @@ -88,7 +88,7 @@ public void avoidCodingErrorsExamples() { new ErrorSpecification.Builder("example.PBEwLargeCountAndRandomSalt", "main", 1) .withTPs(ConstraintError.class, 1) .withTPs(TypestateError.class, 1) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(ForbiddenMethodError.class, 1) .withTPs(IncompleteOperationError.class, 1) .build()); @@ -123,7 +123,7 @@ public void avoidConstantPwdPBEExamples() { new ErrorSpecification.Builder("example.PBEwParameterPassword", "main", 1) .withTPs(ConstraintError.class, 1) .withTPs(TypestateError.class, 1) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(ForbiddenMethodError.class, 1) .withTPs(IncompleteOperationError.class, 1) .build()); @@ -391,7 +391,7 @@ public void avoidInsecureDefaultsExamples() { addErrorSpecification( new ErrorSpecification.Builder("example.UseQualifiedNameForPBE1", "main", 1) .withTPs(ConstraintError.class, 1) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(ForbiddenMethodError.class, 1) .withTPs(TypestateError.class, 1) .withTPs(IncompleteOperationError.class, 1) diff --git a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java index ebae70404..279d60f0d 100644 --- a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java +++ b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java @@ -275,7 +275,7 @@ public void constPwd4PBEExamples() { addErrorSpecification( new ErrorSpecification.Builder("pkm.constPwd4PBE.ConstPassword4PBE1", "main", 1) .withTPs(ConstraintError.class, 2) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(TypestateError.class, 1) .withTPs(ForbiddenMethodError.class, 1) .withTPs(IncompleteOperationError.class, 1) @@ -284,7 +284,7 @@ public void constPwd4PBEExamples() { addErrorSpecification( new ErrorSpecification.Builder("pkm.constPwd4PBE.ConstPassword4PBE2", "main", 1) .withTPs(ConstraintError.class, 2) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(TypestateError.class, 1) .withTPs(ForbiddenMethodError.class, 1) .withTPs(IncompleteOperationError.class, 1) @@ -700,6 +700,7 @@ public void insecureDefaultExamples() { .withTPs(ConstraintError.class, 1) .withTPs(ForbiddenMethodError.class, 1) .withTPs(IncompleteOperationError.class, 1) + .withTPs(RequiredPredicateError.class, 1) .build()); addErrorSpecification( new ErrorSpecification.Builder("pdf.insecureDefault.InsecureDefault3DES", "main", 1) @@ -1184,7 +1185,7 @@ public void paramsPBEExamples() { addErrorSpecification( new ErrorSpecification.Builder("cib.paramsPBE.PBEwConstSalt1", "main", 1) .withTPs(ConstraintError.class, 1) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(ForbiddenMethodError.class, 1) .withTPs(TypestateError.class, 1) .withTPs(IncompleteOperationError.class, 1) @@ -1193,7 +1194,7 @@ public void paramsPBEExamples() { addErrorSpecification( new ErrorSpecification.Builder("cib.paramsPBE.PBEwSmallCount1", "main", 1) .withTPs(ConstraintError.class, 1) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(ForbiddenMethodError.class, 1) .withTPs(TypestateError.class, 1) .withTPs(IncompleteOperationError.class, 1) @@ -1202,7 +1203,7 @@ public void paramsPBEExamples() { addErrorSpecification( new ErrorSpecification.Builder("cib.paramsPBE.PBEwSmallSalt", "main", 1) .withTPs(ConstraintError.class, 1) - .withTPs(RequiredPredicateError.class, 3) + .withTPs(RequiredPredicateError.class, 4) .withTPs(ForbiddenMethodError.class, 1) .withTPs(TypestateError.class, 1) .withTPs(IncompleteOperationError.class, 1) @@ -1349,6 +1350,7 @@ public void riskyInsecureCryptoExamples() { .withTPs(ConstraintError.class, 2) .withTPs(ForbiddenMethodError.class, 1) .withTPs(IncompleteOperationError.class, 1) + .withTPs(RequiredPredicateError.class, 2) .build()); addErrorSpecification(