From 0b205b182a77202875fba60a0f12f1c58e13a14b Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Thu, 4 Jul 2024 16:29:57 +0200 Subject: [PATCH 01/16] Add test case from #69 --- .../tests/headless/ReportedIssueTest.java | 3 +++ CryptoAnalysisTargets/ReportedIssues/pom.xml | 8 ++++++ .../src/main/java/issue69/Issue69.java | 25 +++++++++++++++++++ 3 files changed, 36 insertions(+) create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue69/Issue69.java diff --git a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java index 7465e2abe..e90c5bc9e 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java @@ -43,6 +43,9 @@ public void reportedIssues() { setErrorsCount("", ConstraintError.class, 1); setErrorsCount("", RequiredPredicateError.class, 3); + setErrorsCount("", IncompleteOperationError.class, 1); + setErrorsCount("", RequiredPredicateError.class, 4); + // TODO toCharArray() is not currently not considered when evaluating NeverTypeOfErrors setErrorsCount("", NeverTypeOfError.class, 0); setErrorsCount("", RequiredPredicateError.class, 3); diff --git a/CryptoAnalysisTargets/ReportedIssues/pom.xml b/CryptoAnalysisTargets/ReportedIssues/pom.xml index 280f473a2..5f6776100 100644 --- a/CryptoAnalysisTargets/ReportedIssues/pom.xml +++ b/CryptoAnalysisTargets/ReportedIssues/pom.xml @@ -15,4 +15,12 @@ + + + + commons-codec + commons-codec + 1.10 + + \ No newline at end of file diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue69/Issue69.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue69/Issue69.java new file mode 100644 index 000000000..773f4619e --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue69/Issue69.java @@ -0,0 +1,25 @@ +package issue69; + +import org.apache.commons.codec.binary.Base64; + +import javax.crypto.Cipher; +import java.security.Key; +import java.security.KeyFactory; +import java.security.spec.X509EncodedKeySpec; + +public class Issue69 { + + private static final String KEY_ALGORITHM = "RSA"; + + public void encryptByPublicKey(String publicKey) throws Exception { + byte[] keyBytes = new Base64().decode(publicKey.getBytes()); + X509EncodedKeySpec x509KeySpec = new X509EncodedKeySpec(keyBytes); + KeyFactory keyFactory = KeyFactory.getInstance(KEY_ALGORITHM); + Key publicK = keyFactory.generatePublic(x509KeySpec); + + Cipher cipher = Cipher.getInstance(keyFactory.getAlgorithm()); + + // RequiredPredicateError because no predicate is ensured on 'keyBytes' + cipher.init(Cipher.ENCRYPT_MODE, publicK); + } +} From abca07bfcf4172a42379a797855ed15a3bcb876e Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Thu, 4 Jul 2024 17:20:51 +0200 Subject: [PATCH 02/16] Add test case from #208 --- .../tests/headless/ReportedIssueTest.java | 3 +++ .../Issue208WithMultipleEntryPoints.java | 19 ++++++++++++++ .../Issue208WithSingleEntryPoint.java | 25 +++++++++++++++++++ 3 files changed, 47 insertions(+) create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithMultipleEntryPoints.java create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithSingleEntryPoint.java diff --git a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java index e90c5bc9e..720dfbdc3 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java @@ -20,6 +20,9 @@ public void reportedIssues() { HeadlessCryptoScanner scanner = createScanner(mavenProject); setErrorsCount("", RequiredPredicateError.class, 1); + + setErrorsCount("", RequiredPredicateError.class, 0); + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", ConstraintError.class, 1); setErrorsCount("", RequiredPredicateError.class, 1); diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithMultipleEntryPoints.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithMultipleEntryPoints.java new file mode 100644 index 000000000..f851d8e84 --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithMultipleEntryPoints.java @@ -0,0 +1,19 @@ +package issue208; + +import javax.crypto.spec.IvParameterSpec; +import java.security.SecureRandom; + +public class Issue208WithMultipleEntryPoints { + + private final SecureRandom secureRandom = new SecureRandom(); + + private static final int IV_LENGTH = 32; + + private void encryptImpl() { + byte[] iv = new byte[IV_LENGTH]; + secureRandom.nextBytes(iv); + + // iv has to ensure 'randomized' + IvParameterSpec ivParameterSpec = new IvParameterSpec(iv); + } +} diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithSingleEntryPoint.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithSingleEntryPoint.java new file mode 100644 index 000000000..290a28121 --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue208/Issue208WithSingleEntryPoint.java @@ -0,0 +1,25 @@ +package issue208; + +import javax.crypto.spec.IvParameterSpec; +import java.security.SecureRandom; + +public class Issue208WithSingleEntryPoint { + + private final SecureRandom secureRandom = new SecureRandom(); + + private static final int IV_LENGTH = 32; + + private void encryptImpl() { + byte[] iv = new byte[IV_LENGTH]; + secureRandom.nextBytes(iv); + + IvParameterSpec ivParameterSpec = new IvParameterSpec(iv); + } + + public static void main(String[] args) { + // Method 'main' is the single entry point -> Instantiate SecureRandom seed and + // use it in 'encryptImpl' + Issue208WithSingleEntryPoint issue208 = new Issue208WithSingleEntryPoint(); + issue208.encryptImpl(); + } +} From 66f0e2c9410ed624986c5f654146f154e03e8be4 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Sat, 6 Jul 2024 12:26:35 +0200 Subject: [PATCH 03/16] Add parameter indices to compare predicates more precisely --- .../analysis/AlternativeReqPredicate.java | 30 ++-- .../AnalysisSeedWithSpecification.java | 73 +++++---- .../analysis/EnsuredCrySLPredicate.java | 4 +- .../crypto/analysis/PredicateHandler.java | 150 ++++++------------ .../analysis/RequiredCrySLPredicate.java | 20 ++- .../errors/RequiredPredicateError.java | 101 +++++++----- .../crypto/constraints/ConstraintSolver.java | 26 ++- .../StateMachineGraphBuilder.java | 1 + .../ConstraintErrorCountAssertion.java | 7 +- .../HasEnsuredPredicateAssertion.java | 7 +- .../NotHasEnsuredPredicateAssertion.java | 8 +- .../RequiredPredicatesTest.java | 7 +- .../RequiredPredicateWithThisTest.java | 62 ++++++-- .../requiredpredicateswiththis/Source.java | 8 + .../TargetAlternative1.java | 4 + .../TargetAlternative2.java | 4 + .../TargetWithAlternatives.java | 2 +- .../headless/BragaCryptoGoodUsesTest.java | 39 +++-- .../headless/BragaCryptoMisusesTest.java | 20 +-- .../requiredPredicateWithThis/Source.crysl | 10 +- .../TargetAlternative1.crysl | 4 + .../TargetAlternative2.crysl | 4 + ...ves.crysl => TargetWithAlternatives.crysl} | 7 +- .../UsingTarget.crysl | 2 +- .../requiredPredicates/Requires.crysl | 6 +- 25 files changed, 359 insertions(+), 247 deletions(-) create mode 100644 CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative1.java create mode 100644 CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative2.java create mode 100644 CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative1.crysl create mode 100644 CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative2.crysl rename CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/{TargetWithDifferentAlternatives.crysl => TargetWithAlternatives.crysl} (54%) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AlternativeReqPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/AlternativeReqPredicate.java index 1f4a7e7b6..dd0ea3c9d 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AlternativeReqPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AlternativeReqPredicate.java @@ -10,20 +10,15 @@ public class AlternativeReqPredicate implements ISLConstraint { - private final Statement stmt; private final List alternatives; + private final Statement stmt; + private final int paramIndex; - public AlternativeReqPredicate(CrySLPredicate alternativeOne, Statement stmt) { - this.alternatives = new ArrayList<>(); - this.alternatives.add(alternativeOne); - this.stmt = stmt; - } - - public AlternativeReqPredicate(CrySLPredicate alternativeOne, CrySLPredicate alternativeTwo, Statement stmt) { + public AlternativeReqPredicate(CrySLPredicate alternativeOne, Statement stmt, int paramIndex) { this.alternatives = new ArrayList<>(); this.alternatives.add(alternativeOne); - this.alternatives.add(alternativeTwo); this.stmt = stmt; + this.paramIndex = paramIndex; } @Override @@ -32,6 +27,7 @@ public int hashCode() { int result = 1; result = prime * result + ((alternatives == null) ? 0 : alternatives.hashCode()); result = prime * result + ((stmt == null) ? 0 : stmt.hashCode()); + result = prime * result + paramIndex; return result; } @@ -51,16 +47,24 @@ public boolean equals(Object obj) { return false; if (stmt == null) { return other.stmt == null; - } else return stmt.equals(other.stmt); + } else if (!stmt.equals(other.stmt)) { + return false; + } + + return paramIndex == other.paramIndex; } public Statement getLocation() { return stmt; } + public int getParamIndex() { + return paramIndex; + } + @Override public String toString() { - return "misses " + alternatives.stream().map(CrySLPredicate::toString).collect(Collectors.joining(" OR ")) + ((stmt != null) ? " @ " + stmt : ""); + return alternatives.stream().map(CrySLPredicate::toString).collect(Collectors.joining(" OR ")) + " @ " + stmt + " @ index " + paramIndex; } @Override @@ -81,8 +85,8 @@ public List getAlternatives() { return alternatives; } - public boolean addAlternative(CrySLPredicate newAlt) { - return alternatives.add(newAlt); + public void addAlternative(CrySLPredicate newAlt) { + alternatives.add(newAlt); } } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index e22ddd20f..b92354b29 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -39,6 +39,7 @@ import typestate.finiteautomata.ITransition; import typestate.finiteautomata.State; +import java.util.AbstractMap; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -48,6 +49,7 @@ import java.util.List; import java.util.Map; import java.util.Optional; +import java.util.Set; import java.util.stream.Collectors; public class AnalysisSeedWithSpecification extends IAnalysisSeed { @@ -61,7 +63,7 @@ public class AnalysisSeedWithSpecification extends IAnalysisSeed { private final Multimap typeStateChange = HashMultimap.create(); private Map allCallsOnObject; - private final Collection ensuredPredicates = Sets.newHashSet(); + private final Map>> ensuredPredicates = new HashMap<>(); private final Collection indirectlyEnsuredPredicates = Sets.newHashSet(); private final Collection hiddenPredicates = Sets.newHashSet(); @@ -323,17 +325,18 @@ private boolean isMethodToAcceptingState(DeclaredMethod method) { * predicate checks * * @param ensPred the ensured predicate + * @param statement the statement where the predicate should be ensured + * @param paramIndex the parameter index where the predicate is ensured (-1 for predicates on this seed) */ - public void addEnsuredPredicate(EnsuredCrySLPredicate ensPred) { - // Hidden predicates do not satisfy any constraints + public void addEnsuredPredicate(EnsuredCrySLPredicate ensPred, Statement statement, int paramIndex) { if (ensPred instanceof HiddenPredicate) { HiddenPredicate hiddenPredicate = (HiddenPredicate) ensPred; hiddenPredicates.add(hiddenPredicate); return; } - // If the predicate was not ensured before, ensure it and check the constraints - if (ensuredPredicates.add(ensPred)) { + Map.Entry predAtIndex = new AbstractMap.SimpleEntry<>(ensPred, paramIndex); + if (ensuredPredicates.computeIfAbsent(statement, k -> new HashSet<>()).add(predAtIndex)) { checkConstraintsAndEnsurePredicates(); } } @@ -359,7 +362,7 @@ private void checkConstraintsAndEnsurePredicates() { isPredicateGeneratingStateAvailable = true; EnsuredCrySLPredicate ensPred; - if (!satisfiesConstraintSystem && !predToBeEnsured.getConstraint().isPresent()) { + if (!satisfiesConstraintSystem && predToBeEnsured.getConstraint().isEmpty()) { // predicate has no condition, but the constraint system is not satisfied ensPred = new HiddenPredicate(predToBeEnsured, parameterAnalysis.getCollectedValues(), this, HiddenPredicate.HiddenPredicateType.ConstraintsAreNotSatisfied); } else if (predToBeEnsured.getConstraint().isPresent() && !isPredConditionSatisfied(predToBeEnsured)) { @@ -502,7 +505,7 @@ private void expectPredicateOnOtherObject(EnsuredCrySLPredicate ensPred, Stateme if (baseType.getWrappedClass().getName().equals(rule.getClassName())) { Optional seed = scanner.getSeedWithSpec(AnalysisSeedWithSpecification.makeSeedForComparison(scanner, statement, fact, rule)); - if (!seed.isPresent()) { + if (seed.isEmpty()) { LOGGER.debug("{} has not been discovered in the Typestate Analysis", seed); continue; } @@ -516,7 +519,7 @@ private void expectPredicateOnOtherObject(EnsuredCrySLPredicate ensPred, Stateme if (!specificationExists) { Optional seed = scanner.getSeedWithoutSpec(AnalysisSeedWithEnsuredPredicate.makeSeedForComparison(scanner, statement, fact)); - if (!seed.isPresent()) { + if (seed.isEmpty()) { LOGGER.debug("{} has not been discovered in the Typestate Analysis", seed); return; } @@ -569,7 +572,6 @@ private void activateIndirectlyEnsuredPredicates() { /* Add the predicate with 'this' to the ensured predicates, check the required predicate constraints * and ensure it in all accepting states that do not negate it */ - addEnsuredPredicate(predWithThis); for (Table.Cell c : analysisResults.asStatementValWeightTable().cellSet()) { Collection states = getTargetStates(c.getValue()); @@ -694,7 +696,7 @@ private boolean checkInternalConstraints() { */ private boolean isConstraintSystemSatisfied() { if (internalConstraintsSatisfied) { - return checkPredicates().isEmpty(); + return computeMissingPredicates().isEmpty(); } return false; } @@ -705,25 +707,24 @@ private boolean isConstraintSystemSatisfied() { * * @return remainingPredicates predicates that are not satisfied */ - public Collection checkPredicates() { - Collection requiredPredicates = Lists.newArrayList(); - for (ISLConstraint con : constraintSolver.getRequiredPredicates()) { - if (!ConstraintSolver.predefinedPreds.contains((con instanceof RequiredCrySLPredicate) ? ((RequiredCrySLPredicate) con).getPred().getPredName() - : ((AlternativeReqPredicate) con).getAlternatives().get(0).getPredName())) { - requiredPredicates.add(con); - } - } - Collection remainingPredicates = Sets.newHashSet(requiredPredicates); + public Collection computeMissingPredicates() { + Collection requiredPredicates = constraintSolver.getRequiredPredicates(); + Collection remainingPredicates = new HashSet<>(requiredPredicates); for (ISLConstraint pred : requiredPredicates) { + Set> predsAtStatement = ensuredPredicates.getOrDefault(pred.getLocation(), new HashSet<>()); + if (pred instanceof RequiredCrySLPredicate) { RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred; + int reqParamIndex = reqPred.getParamIndex(); if (reqPred.getPred().isNegated()) { + // Check for negated predicates, e.g. !randomized boolean violated = false; - for (EnsuredCrySLPredicate ensPred : ensuredPredicates) { - if (reqPred.getPred().equals(ensPred.getPredicate()) && doPredsMatch(reqPred.getPred(), ensPred)) { + // Negated predicates are violated if the corresponding predicate is ensured + for (Map.Entry ensPredAtIndex : predsAtStatement) { + if (doReqPredAndEnsPredMatch(reqPred.getPred(), reqParamIndex, ensPredAtIndex)) { violated = true; } } @@ -732,29 +733,31 @@ public Collection checkPredicates() { remainingPredicates.remove(pred); } } else { - for (EnsuredCrySLPredicate ensPred : ensuredPredicates) { - if (reqPred.getPred().equals(ensPred.getPredicate()) && doPredsMatch(reqPred.getPred(), ensPred)) { + // Check for basic required predicates, e.g. randomized + for (Map.Entry ensPredAtIndex : predsAtStatement) { + if (doReqPredAndEnsPredMatch(reqPred.getPred(), reqParamIndex, ensPredAtIndex)) { remainingPredicates.remove(pred); } } } } else if (pred instanceof AlternativeReqPredicate) { - AlternativeReqPredicate alt = (AlternativeReqPredicate) pred; - Collection alternatives = alt.getAlternatives(); + AlternativeReqPredicate altPred = (AlternativeReqPredicate) pred; + Collection alternatives = altPred.getAlternatives(); Collection positives = alternatives.stream().filter(e -> !e.isNegated()).collect(Collectors.toList()); Collection negatives = alternatives.stream().filter(CrySLPredicate::isNegated).collect(Collectors.toList()); + int altParamIndex = altPred.getParamIndex(); boolean satisfied = false; Collection ensuredNegatives = alternatives.stream().filter(CrySLPredicate::isNegated).collect(Collectors.toList()); - for (EnsuredCrySLPredicate ensPred : ensuredPredicates) { - // Check if any positive alternative is satisfied by the ensured predicate - if (positives.stream().anyMatch(e -> e.equals(ensPred.getPredicate()) && doPredsMatch(e, ensPred))) { + for (Map.Entry ensPredAtIndex : predsAtStatement) { + // If any positive alternative is satisfied, the whole predicate is satisfied + if (positives.stream().anyMatch(e -> doReqPredAndEnsPredMatch(e, altParamIndex, ensPredAtIndex))) { satisfied = true; } - // Negated alternatives that are ensured are not satisfied - Collection violatedNegAlternatives = negatives.stream().filter(e -> e.equals(ensPred.getPredicate()) && doPredsMatch(e, ensPred)).collect(Collectors.toList()); + // Remove all negated alternatives that are ensured + Collection violatedNegAlternatives = negatives.stream().filter(e -> doReqPredAndEnsPredMatch(e, altParamIndex, ensPredAtIndex)).collect(Collectors.toList()); ensuredNegatives.removeAll(violatedNegAlternatives); } @@ -764,22 +767,30 @@ public Collection checkPredicates() { } } - for (ISLConstraint rem : Lists.newArrayList(remainingPredicates)) { + // Check conditional required predicates + for (ISLConstraint rem : new HashSet<>(remainingPredicates)) { if (rem instanceof RequiredCrySLPredicate) { RequiredCrySLPredicate singlePred = (RequiredCrySLPredicate) rem; + if (isPredConditionSatisfied(singlePred.getPred())) { remainingPredicates.remove(singlePred); } } else if (rem instanceof AlternativeReqPredicate) { Collection altPred = ((AlternativeReqPredicate) rem).getAlternatives(); + if (altPred.parallelStream().anyMatch(this::isPredConditionSatisfied)) { remainingPredicates.remove(rem); } } } + return remainingPredicates; } + private boolean doReqPredAndEnsPredMatch(CrySLPredicate reqPred, int reqPredIndex, Map.Entry ensPred) { + return reqPred.equals(ensPred.getKey().getPredicate()) && doPredsMatch(reqPred, ensPred.getKey()) && reqPredIndex == ensPred.getValue(); + } + /** * Check for a predicate A => B, whether the condition A of B is satisfied * diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java index 04169ef09..4c67e7980 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java @@ -11,9 +11,9 @@ public class EnsuredCrySLPredicate { private final CrySLPredicate predicate; private final Multimap parametersToValues; - public EnsuredCrySLPredicate(CrySLPredicate predicate, Multimap parametersToValues2) { + public EnsuredCrySLPredicate(CrySLPredicate predicate, Multimap parametersToValues) { this.predicate = predicate; - parametersToValues = parametersToValues2; + this.parametersToValues = parametersToValues; } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java b/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java index 29d2f3065..4ffa208b7 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java @@ -3,26 +3,19 @@ import boomerang.results.ForwardBoomerangResults; import boomerang.scene.ControlFlowGraph; import boomerang.scene.InvokeExpr; -import boomerang.scene.Method; import boomerang.scene.Statement; import boomerang.scene.Val; import com.google.common.collect.HashBasedTable; import com.google.common.collect.Sets; import com.google.common.collect.Table; -import com.google.common.collect.Table.Cell; import crypto.analysis.errors.RequiredPredicateError; -import crypto.extractparameter.CallSiteWithExtractedValue; -import crypto.extractparameter.CallSiteWithParamIndex; -import crypto.rules.CrySLObject; import crypto.rules.CrySLPredicate; import crypto.rules.CrySLRule; import crypto.rules.ISLConstraint; import typestate.TransitionFunction; -import java.util.AbstractMap.SimpleEntry; import java.util.ArrayList; import java.util.Collection; -import java.util.Collections; import java.util.HashMap; import java.util.HashSet; import java.util.List; @@ -34,16 +27,16 @@ public class PredicateHandler { private final class AddPredicateToOtherSeed implements ResultsHandler { private final Statement statement; private final Val base; - private final Method callerMethod; private final EnsuredCrySLPredicate ensPred; - private final AnalysisSeedWithSpecification secondSeed; + private final AnalysisSeedWithSpecification otherSeed; + private final int paramIndex; - private AddPredicateToOtherSeed(Statement statement, Val base, Method callerMethod, EnsuredCrySLPredicate ensPred, AnalysisSeedWithSpecification secondSeed) { + private AddPredicateToOtherSeed(Statement statement, Val base, EnsuredCrySLPredicate ensPred, AnalysisSeedWithSpecification otherSeed, int paramIndex) { this.statement = statement; this.base = base; - this.callerMethod = callerMethod; this.ensPred = ensPred; - this.secondSeed = secondSeed; + this.otherSeed = otherSeed; + this.paramIndex = paramIndex; } @Override @@ -53,7 +46,7 @@ public void done(ForwardBoomerangResults results) { Map entry = row.getValue(); if (entry.containsKey(base)) { - secondSeed.addEnsuredPredicate(ensPred); + otherSeed.addEnsuredPredicate(ensPred, statement, paramIndex); } } } @@ -65,9 +58,8 @@ public int hashCode() { int result = 1; result = prime * result + getOuterType().hashCode(); result = prime * result + ((base == null) ? 0 : base.hashCode()); - result = prime * result + ((callerMethod == null) ? 0 : callerMethod.hashCode()); result = prime * result + ((ensPred == null) ? 0 : ensPred.hashCode()); - result = prime * result + ((secondSeed == null) ? 0 : secondSeed.hashCode()); + result = prime * result + ((otherSeed == null) ? 0 : otherSeed.hashCode()); result = prime * result + ((statement == null) ? 0 : statement.hashCode()); return result; } @@ -88,20 +80,15 @@ public boolean equals(Object obj) { return false; } else if (!base.equals(other.base)) return false; - if (callerMethod == null) { - if (other.callerMethod != null) - return false; - } else if (!callerMethod.equals(other.callerMethod)) - return false; if (ensPred == null) { if (other.ensPred != null) return false; } else if (!ensPred.equals(other.ensPred)) return false; - if (secondSeed == null) { - if (other.secondSeed != null) + if (otherSeed == null) { + if (other.otherSeed != null) return false; - } else if (!secondSeed.equals(other.secondSeed)) + } else if (!otherSeed.equals(other.otherSeed)) return false; if (statement == null) { return other.statement == null; @@ -150,41 +137,49 @@ public Set getExistingPredicates(Statement stmt, Val seed return set; } - private void onPredicateAdded(IAnalysisSeed seedObj, Statement statement, Val seed, EnsuredCrySLPredicate ensPred) { + private void onPredicateAdded(IAnalysisSeed seedObj, Statement statement, Val fact, EnsuredCrySLPredicate ensPred) { + if (seedObj instanceof AnalysisSeedWithSpecification) { + AnalysisSeedWithSpecification seedWithSpec = (AnalysisSeedWithSpecification) seedObj; + + if (seedWithSpec.getFact().getVariableName().equals(fact.getVariableName())) { + seedWithSpec.addEnsuredPredicate(ensPred, statement, -1); + } + } + if (statement.containsInvokeExpr()) { InvokeExpr invokeExpr = statement.getInvokeExpr(); if (invokeExpr.isInstanceInvokeExpr()) { - Method callerMethod = statement.getMethod(); Val base = invokeExpr.getBase(); - boolean paramMatch = false; - for (Val arg : invokeExpr.getArgs()) { - if (!seed.isNull() && seed.getType().equals(arg.getType()) && seed.getVariableName().equals(arg.getVariableName())) { - paramMatch = true; + + for (int i = 0; i < invokeExpr.getArgs().size(); i++) { + Val arg = invokeExpr.getArg(i); + + if (!fact.getVariableName().equals(arg.getVariableName())) { + continue; } - } - if (paramMatch) { - for (AnalysisSeedWithSpecification secondSeed : cryptoScanner.getAnalysisSeedsWithSpec()) { - secondSeed.registerResultsHandler(new AddPredicateToOtherSeed(statement, base, callerMethod, ensPred, secondSeed)); + + for (AnalysisSeedWithSpecification otherSeed : cryptoScanner.getAnalysisSeedsWithSpec()) { + otherSeed.registerResultsHandler(new AddPredicateToOtherSeed(statement, base, ensPred, otherSeed, i)); } } } if (invokeExpr.isStaticInvokeExpr() && statement.isAssign()) { - boolean paramMatch = false; - for (Val arg : invokeExpr.getArgs()) { - if (!seed.isNull() && seed.equals(arg)) - paramMatch = true; - } - if (paramMatch) { - for (AnalysisSeedWithSpecification spec : cryptoScanner.getAnalysisSeedsWithSpec()) { - if (spec.getOrigin().equals(statement)) { - spec.addEnsuredPredicate(ensPred); + for (int i = 0; i < invokeExpr.getArgs().size(); i++) { + Val arg = invokeExpr.getArg(i); + + if (!fact.getVariableName().equals(arg.getVariableName())) { + continue; + } + + for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) { + if (seed.getOrigin().equals(statement)) { + seed.addEnsuredPredicate(ensPred, statement, i); } } } } - } } @@ -208,49 +203,20 @@ public void checkPredicates() { private void collectMissingRequiredPredicates() { for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) { requiredPredicateErrors.put(seed, new ArrayList<>()); - Collection missingPredicates = seed.checkPredicates(); + Collection missingPredicates = seed.computeMissingPredicates(); for (ISLConstraint pred : missingPredicates) { if (pred instanceof RequiredCrySLPredicate) { - collectMissingPred(seed, (RequiredCrySLPredicate) pred); - } else if (pred instanceof AlternativeReqPredicate) { - collectMissingPred(seed, (AlternativeReqPredicate) pred); - } - } - } - } - - private void collectMissingPred(AnalysisSeedWithSpecification seed, RequiredCrySLPredicate missingPred) { - // Check for predicate errors with 'this' as parameter - if (missingPred.getPred().getParameters().stream().anyMatch(param -> param instanceof CrySLObject && param.getName().equals("this"))) { - RequiredPredicateError reqPredError = new RequiredPredicateError(seed, missingPred.getLocation(), seed.getSpecification(), new CallSiteWithExtractedValue(new CallSiteWithParamIndex(missingPred.getLocation(), null, -1, "this"), null), Collections.singletonList(missingPred.getPred())); - addRequiredPredicateErrorOnSeed(reqPredError, seed); - - return; - } - - for (CallSiteWithParamIndex v : seed.getParameterAnalysis().getAllQuerySites()) { - - if (missingPred.getPred().getInvolvedVarNames().contains(v.getVarName()) && v.stmt().equals(missingPred.getLocation())) { - RequiredPredicateError reqPredError = new RequiredPredicateError(seed, missingPred.getLocation(), seed.getSpecification(), new CallSiteWithExtractedValue(v, null), Collections.singletonList(missingPred.getPred())); - addRequiredPredicateErrorOnSeed(reqPredError, seed); - } - } - } - - private void collectMissingPred(AnalysisSeedWithSpecification seed, AlternativeReqPredicate missingPred) { - // Check for predicate errors with 'this' as parameter in all alternatives - if (missingPred.getAlternatives().parallelStream().anyMatch(p -> p.getParameters().stream().anyMatch(param -> param instanceof CrySLObject && param.getName().equals("this")))) { - RequiredPredicateError reqPredError = new RequiredPredicateError(seed, missingPred.getLocation(), seed.getSpecification(), new CallSiteWithExtractedValue(new CallSiteWithParamIndex(missingPred.getLocation(), null, -1, "this"), null), missingPred.getAlternatives()); - addRequiredPredicateErrorOnSeed(reqPredError, seed); + RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred; - return; - } + RequiredPredicateError reqPredError = new RequiredPredicateError(seed, reqPred); + addRequiredPredicateErrorOnSeed(reqPredError, seed); + } else if (pred instanceof AlternativeReqPredicate) { + AlternativeReqPredicate altReqPred = (AlternativeReqPredicate) pred; - for (CallSiteWithParamIndex v : seed.getParameterAnalysis().getAllQuerySites()) { - if (missingPred.getAlternatives().parallelStream().anyMatch(e -> e.getInvolvedVarNames().contains(v.getVarName())) && v.stmt().equals(missingPred.getLocation())) { - RequiredPredicateError reqPredError = new RequiredPredicateError(seed, missingPred.getLocation(), seed.getSpecification(), new CallSiteWithExtractedValue(v, null), missingPred.getAlternatives()); - addRequiredPredicateErrorOnSeed(reqPredError, seed); + RequiredPredicateError reqPredError = new RequiredPredicateError(seed, altReqPred); + addRequiredPredicateErrorOnSeed(reqPredError, seed); + } } } } @@ -286,7 +252,7 @@ private void checkForContradictions() { } for (Statement generatingPredicateStmt : expectedPredicateObjectBased.rowKeySet()) { for (Map.Entry> exPredCell : existingPredicates.row(generatingPredicateStmt).entrySet()) { - Set preds = new HashSet(); + Set preds = new HashSet<>(); for (EnsuredCrySLPredicate exPred : exPredCell.getValue()) { preds.add(exPred.getPredicate().getPredName()); } @@ -300,24 +266,4 @@ private void checkForContradictions() { } } - private Table> computeMissingPredicates() { - Table> res = HashBasedTable.create(); - for (Cell> c : expectedPredicateObjectBased.cellSet()) { - Set exPreds = existingPredicatesObjectBased.get(c.getRowKey(), c.getColumnKey()); - if (c.getValue() == null) - continue; - HashSet expectedPreds = new HashSet<>(c.getValue()); - if (exPreds == null) { - exPreds = Sets.newHashSet(); - } - for (EnsuredCrySLPredicate p : exPreds) { - expectedPreds.remove(p.getPredicate()); - } - if (!expectedPreds.isEmpty()) { - res.put(c.getRowKey(), c.getColumnKey(), expectedPreds); - } - } - return res; - } - } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/RequiredCrySLPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/RequiredCrySLPredicate.java index 1bc884653..0d4daf35f 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/RequiredCrySLPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/RequiredCrySLPredicate.java @@ -10,10 +10,12 @@ public class RequiredCrySLPredicate implements ISLConstraint { private final CrySLPredicate predicate; private final Statement statement; + private final int paramIndex; - public RequiredCrySLPredicate(CrySLPredicate predicate, Statement statement) { + public RequiredCrySLPredicate(CrySLPredicate predicate, Statement statement, int paramIndex) { this.predicate = predicate; this.statement = statement; + this.paramIndex = paramIndex; } @Override @@ -22,6 +24,7 @@ public int hashCode() { int result = 1; result = prime * result + ((predicate == null) ? 0 : predicate.hashCode()); result = prime * result + ((statement == null) ? 0 : statement.hashCode()); + result = prime * result + paramIndex; return result; } @@ -40,8 +43,13 @@ public boolean equals(Object obj) { } else if (!predicate.equals(other.predicate)) return false; if (statement == null) { - return other.statement == null; - } else return statement.equals(other.statement); + if (other.statement != null) { + return false; + } + } else if (!statement.equals(other.statement)) { + return false; + } + return paramIndex == other.paramIndex; } public CrySLPredicate getPred() { @@ -52,9 +60,13 @@ public Statement getLocation() { return statement; } + public int getParamIndex() { + return paramIndex; + } + @Override public String toString() { - return "misses " + predicate + " @ " + statement.toString(); + return predicate + " @ " + statement.toString() + " @ index " + paramIndex; } @Override diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java index 65911655b..166bade3c 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java @@ -1,14 +1,14 @@ package crypto.analysis.errors; -import boomerang.scene.Statement; +import crypto.analysis.AlternativeReqPredicate; +import crypto.analysis.AnalysisSeedWithSpecification; import crypto.analysis.HiddenPredicate; -import crypto.analysis.IAnalysisSeed; -import crypto.extractparameter.CallSiteWithExtractedValue; +import crypto.analysis.RequiredCrySLPredicate; import crypto.rules.CrySLPredicate; -import crypto.rules.CrySLRule; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; import java.util.stream.Collectors; @@ -17,16 +17,24 @@ */ public class RequiredPredicateError extends AbstractError { - private final Collection contradictedPredicate; - private final CallSiteWithExtractedValue extractedValues; private final Collection hiddenPredicates; + private final Collection contradictedPredicates; + private final int paramIndex; - public RequiredPredicateError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule, CallSiteWithExtractedValue cs, Collection contradictedPredicates) { - super(seed, errorStmt, rule); + public RequiredPredicateError(AnalysisSeedWithSpecification seed, RequiredCrySLPredicate violatedPred) { + super(seed, violatedPred.getLocation(), seed.getSpecification()); - this.contradictedPredicate = contradictedPredicates; - this.extractedValues = cs; this.hiddenPredicates = new HashSet<>(); + this.contradictedPredicates = Collections.singletonList(violatedPred.getPred()); + this.paramIndex = violatedPred.getParamIndex(); + } + + public RequiredPredicateError(AnalysisSeedWithSpecification seed, AlternativeReqPredicate violatedPred) { + super(seed, violatedPred.getLocation(), seed.getSpecification()); + + this.hiddenPredicates = new HashSet<>(); + this.contradictedPredicates = violatedPred.getAlternatives(); + this.paramIndex = violatedPred.getParamIndex(); } public void addHiddenPredicates(Collection hiddenPredicates) { @@ -46,20 +54,20 @@ public void mapPrecedingErrors() { * @return list of contradicting predicates */ public Collection getContradictedPredicates() { - return contradictedPredicate; - } - - public CallSiteWithExtractedValue getExtractedValues() { - return extractedValues; + return contradictedPredicates; } public Collection getHiddenPredicates() { return hiddenPredicates; } + public int getParamIndex() { + return paramIndex; + } + @Override public String toErrorMarkerString() { - StringBuilder msg = new StringBuilder(extractedValues.toString()); + StringBuilder msg = new StringBuilder(getParamIndexAsText()); msg.append(" was not properly generated as "); String predicateName = getContradictedPredicates().stream().map(CrySLPredicate::getPredName).collect(Collectors.joining(" OR ")); String[] parts = predicateName.split("(?=[A-Z])"); @@ -67,20 +75,47 @@ public String toErrorMarkerString() { for (int i = 1; i < parts.length; i++) { msg.append(parts[i]); } + return msg.toString(); + } - if (predicateName.equals("preparedIV") && extractedValues.toString().equals("Third parameter")) { - msg.append(" [ with CBC, It's required to use IVParameterSpec]"); + 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; } - return msg.toString(); + res += "parameter"; + return res; } @Override public int hashCode() { return Arrays.hashCode(new Object[]{ super.hashCode(), - contradictedPredicate, - extractedValues, - hiddenPredicates + hiddenPredicates, + contradictedPredicates, + paramIndex }); } @@ -91,26 +126,20 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; RequiredPredicateError other = (RequiredPredicateError) obj; - if (contradictedPredicate == null) { - if (other.getContradictedPredicates() != null) return false; - } else if (!contradictedPredicate.equals(other.getContradictedPredicates())) { - return false; - } - - if (extractedValues == null) { - if (other.getExtractedValues() != null) return false; - } else if (!extractedValues.equals(other.getExtractedValues())) { + if (hiddenPredicates == null) { + if (other.getHiddenPredicates() != null) return false; + } else if (!hiddenPredicates.equals(other.hiddenPredicates)) { return false; } - if (hiddenPredicates == null) { - if (other.getHiddenPredicates() != null) return false; - } else if (!hiddenPredicates.equals(other.getHiddenPredicates())) { + if (contradictedPredicates == null) { + if (other.getContradictedPredicates() != null) return false; + } else if (!contradictedPredicates.equals(other.getContradictedPredicates())) { return false; } - return true; - } + return paramIndex == other.getParamIndex(); + } @Override public String toString() { diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java b/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java index e404647fc..a086bbc6c 100644 --- a/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java +++ b/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java @@ -19,6 +19,7 @@ import crypto.rules.ICrySLPredicateParameter; import crypto.rules.ISLConstraint; +import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; import java.util.HashSet; @@ -138,7 +139,7 @@ private void partitionConstraints() { ISLConstraint left = ((CrySLConstraint) cons).getLeft(); if (left instanceof CrySLPredicate && !predefinedPreds.contains(((CrySLPredicate) left).getPredName())) { - requiredPredicates.addAll(collectAlternativePredicates((CrySLConstraint) cons, Lists.newArrayList())); + requiredPredicates.addAll(collectAlternativePredicates((CrySLConstraint) cons, new ArrayList<>())); } else { relConstraints.add(cons); } @@ -154,13 +155,24 @@ private Collection collectAlternativePredicates(CrySLCo if (alts.isEmpty()) { for (CallSiteWithParamIndex cwpi : this.getParameterAnalysisQuerySites()) { for (ICrySLPredicateParameter p : left.getParameters()) { - if (p.getName().equals("transformation")) + if (p.getName().equals("transformation")) { continue; + } + if (cwpi.getVarName().equals(p.getName())) { - alts.add(new AlternativeReqPredicate(left, cwpi.stmt())); + alts.add(new AlternativeReqPredicate(left, cwpi.stmt(), cwpi.getIndex())); } } } + + // Extract predicates with 'this' as parameter + if (left.getParameters().stream().anyMatch(param -> param.getName().equals("this"))) { + AlternativeReqPredicate altPred = new AlternativeReqPredicate(left, object.getOrigin(), -1); + + if (!alts.contains(altPred)) { + alts.add(altPred); + } + } } else { for (AlternativeReqPredicate alt : alts) { alt.addAlternative(left); @@ -194,14 +206,18 @@ private Collection retrieveValuesForPred(CrySLPredicate } if (cwpi.getVarName().equals(p.getName())) { - result.add(new RequiredCrySLPredicate(pred, cwpi.stmt())); + result.add(new RequiredCrySLPredicate(pred, cwpi.stmt(), cwpi.getIndex())); } } } // Extract predicates with 'this' as parameter if (pred.getParameters().stream().anyMatch(param -> param.getName().equals("this"))) { - result.add(new RequiredCrySLPredicate(pred, object.getOrigin())); + RequiredCrySLPredicate reqPred = new RequiredCrySLPredicate(pred, object.getOrigin(), -1); + + if (!result.contains(reqPred)) { + result.add(reqPred); + } } return result; diff --git a/CryptoAnalysis/src/main/java/crypto/cryslhandler/StateMachineGraphBuilder.java b/CryptoAnalysis/src/main/java/crypto/cryslhandler/StateMachineGraphBuilder.java index 82ed9cad3..cdc8376d5 100644 --- a/CryptoAnalysis/src/main/java/crypto/cryslhandler/StateMachineGraphBuilder.java +++ b/CryptoAnalysis/src/main/java/crypto/cryslhandler/StateMachineGraphBuilder.java @@ -190,6 +190,7 @@ private SubStateMachine buildSubSMG(final Order order, final Collection label = new HashSet<>(retrieveAllMethodsFromEvents()); for (StateNode startNode : startNodes) { diff --git a/CryptoAnalysis/src/test/java/test/assertions/ConstraintErrorCountAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/ConstraintErrorCountAssertion.java index 817a6f41a..c6a4a1ced 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/ConstraintErrorCountAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/ConstraintErrorCountAssertion.java @@ -4,7 +4,7 @@ public class ConstraintErrorCountAssertion implements Assertion { - private int expectedErrorCounts; + private final int expectedErrorCounts; private int actualErrorCounts; public ConstraintErrorCountAssertion(int numberOfCounts) { @@ -25,4 +25,9 @@ public boolean isImprecise() { return expectedErrorCounts != actualErrorCounts; } + @Override + public String toString() { + return "Expected " + expectedErrorCounts + " constraint errors, but got " + actualErrorCounts; + } + } diff --git a/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java index e47bb90c0..9e94cc215 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/HasEnsuredPredicateAssertion.java @@ -7,6 +7,7 @@ import test.Assertion; import java.util.Collection; +import java.util.stream.Collectors; public class HasEnsuredPredicateAssertion implements Assertion { @@ -52,10 +53,12 @@ public void reported(Val seed, EnsuredCrySLPredicate pred) { @Override public String toString() { + Collection aliases = val.stream().map(Val::getVariableName).collect(Collectors.toList()); + if (predName == null) { - return "Expected a predicate for "+ val +" @ " + stmt; + return "Expected a predicate for " + aliases +" @ " + stmt; } else { - return "Expected '" + predName + "' ensured on " + val + " @ " + stmt; + return "Expected '" + predName + "' ensured on " + aliases + " @ " + stmt; } } } diff --git a/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java index 1ba086b00..078036fff 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java +++ b/CryptoAnalysis/src/test/java/test/assertions/NotHasEnsuredPredicateAssertion.java @@ -4,10 +4,10 @@ import boomerang.scene.Val; import crypto.analysis.EnsuredCrySLPredicate; import crypto.analysis.HiddenPredicate; -import soot.jimple.Stmt; import test.Assertion; import java.util.Collection; +import java.util.stream.Collectors; public class NotHasEnsuredPredicateAssertion implements Assertion { @@ -53,10 +53,12 @@ public void reported(Val value, EnsuredCrySLPredicate pred) { @Override public String toString() { + Collection aliases = val.stream().map(Val::getVariableName).collect(Collectors.toList()); + if (predName == null) { - return "Did not expect a predicate for " + val + " @ " + stmt; + return "Did not expect a predicate for " + aliases + " @ " + stmt; } else { - return "Did not expect '" + predName + "' ensured on " + val + " @ " + stmt; + return "Did not expect '" + predName + "' ensured on " + aliases + " @ " + stmt; } } } diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicate/RequiredPredicatesTest.java b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicate/RequiredPredicatesTest.java index d742270f3..ded2bcc02 100644 --- a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicate/RequiredPredicatesTest.java +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicate/RequiredPredicatesTest.java @@ -63,7 +63,6 @@ public void notPred1onPos1() { // AND // same predicate - @Ignore @Test public void pred1onPos1_AND_pred1onPos2() { A pred1onA = new A(); @@ -314,6 +313,7 @@ public void notPred1onPos1_AND_notPred2onPos2() { // OR // same predicate + @Ignore("Requires negated conditional predicates. Alternative predicate have to belong to the same object") @Test public void pred1onPos1_OR_pred1onPos2(){ A pred1onA = new A(); @@ -442,6 +442,9 @@ public void notPred1onPos1_OR_notPred1onPos2(){ } // multi predicates + @Ignore("Can be tested since negated conditions in the REQUIRES section are not supported" + + "Alternative predicates on different objects o1 and o2 (p1[o1] || p2[o2] have to be rewritten as" + + "!p1[o1] => p2[o2]; and !p2[o2] => p1[o1];") @Test public void pred1onPos1_OR_pred2onPos2() { A pred1onA = new A(); @@ -582,7 +585,7 @@ public void notPred1onP1_OR_notPred2onP2() { } // 3 cases same predicate - + @Ignore("Negated conditions are not supported see above") @Test public void pred1onPos1_OR_pred1onPos2_OR_pred1onPos3() { A pred1onA = new A(); diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/RequiredPredicateWithThisTest.java b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/RequiredPredicateWithThisTest.java index 74fb3437e..c2ea53994 100644 --- a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/RequiredPredicateWithThisTest.java +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/RequiredPredicateWithThisTest.java @@ -51,13 +51,29 @@ public void positiveRequiredAlternativePredicateWithThis() { Source source = new Source(); source.causeConstraintError(false); - TargetWithAlternatives target = source.generateTargetWithAlternatives(); - target.doNothing("Nothing"); - Assertions.hasEnsuredPredicate(target, "generatedTargetWithAlternatives"); + TargetWithAlternatives target1 = source.generateTargetWithAlternatives(); + target1.doNothing(); + Assertions.hasEnsuredPredicate(target1, "generatedTargetWithAlternatives"); - UsingTarget usingTarget = new UsingTarget(); - usingTarget.useTarget(target); - Assertions.hasEnsuredPredicate(usingTarget); + UsingTarget usingTarget1 = new UsingTarget(); + usingTarget1.useTarget(target1); + Assertions.hasEnsuredPredicate(usingTarget1); + + TargetWithAlternatives target2 = source.generateTargetAlternative1(); + target2.doNothing(); + Assertions.hasEnsuredPredicate(target2, "generatedAlternative1"); + + UsingTarget usingTarget2 = new UsingTarget(); + usingTarget2.useTarget(target2); + Assertions.hasEnsuredPredicate(usingTarget2); + + TargetWithAlternatives target3 = source.generateTargetAlternative2(); + target3.doNothing(); + Assertions.hasEnsuredPredicate(target3, "generatedAlternative2"); + + UsingTarget usingTarget3 = new UsingTarget(); + usingTarget3.useTarget(target3); + Assertions.hasEnsuredPredicate(usingTarget3); Assertions.predicateErrors(0); } @@ -68,15 +84,35 @@ public void negativeRequiredAlternativePredicateWithThis() { source.causeConstraintError(true); // No ensured predicate is passed to target -> RequiredPredicateError - TargetWithAlternatives target = source.generateTargetWithAlternatives(); - target.doNothing("Nothing"); - Assertions.notHasEnsuredPredicate(target); + TargetWithAlternatives target1 = source.generateTargetWithAlternatives(); + target1.doNothing(); + Assertions.notHasEnsuredPredicate(target1); // RequiredPredicateError for calling useTarget with insecure target - UsingTarget usingTarget = new UsingTarget(); - usingTarget.useTarget(target); - Assertions.notHasEnsuredPredicate(usingTarget); + UsingTarget usingTarget1 = new UsingTarget(); + usingTarget1.useTarget(target1); + Assertions.notHasEnsuredPredicate(usingTarget1); - Assertions.predicateErrors(2); + // No ensured predicate is passed to target -> RequiredPredicateError + TargetWithAlternatives target2 = source.generateTargetAlternative1(); + target2.doNothing(); + Assertions.notHasEnsuredPredicate(target2); + + // RequiredPredicateError for calling useTarget with insecure target + UsingTarget usingTarget2 = new UsingTarget(); + usingTarget2.useTarget(target2); + Assertions.notHasEnsuredPredicate(usingTarget2); + + // No ensured predicate is passed to target -> RequiredPredicateError + TargetWithAlternatives target3 = source.generateTargetAlternative2(); + target3.doNothing(); + Assertions.notHasEnsuredPredicate(target3); + + // RequiredPredicateError for calling useTarget with insecure target + UsingTarget usingTarget3 = new UsingTarget(); + usingTarget3.useTarget(target3); + Assertions.notHasEnsuredPredicate(usingTarget3); + + Assertions.predicateErrors(6); } } diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/Source.java b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/Source.java index fb501831a..2eddf8fc1 100644 --- a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/Source.java +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/Source.java @@ -12,4 +12,12 @@ public TargetWithAlternatives generateTargetWithAlternatives() { return new TargetWithAlternatives(); } + public TargetAlternative1 generateTargetAlternative1() { + return new TargetAlternative1(); + } + + public TargetAlternative2 generateTargetAlternative2() { + return new TargetAlternative2(); + } + } diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative1.java b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative1.java new file mode 100644 index 000000000..01f578731 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative1.java @@ -0,0 +1,4 @@ +package tests.error.predicate.requiredpredicateswiththis; + +public class TargetAlternative1 extends TargetWithAlternatives { +} diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative2.java b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative2.java new file mode 100644 index 000000000..95519ba43 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetAlternative2.java @@ -0,0 +1,4 @@ +package tests.error.predicate.requiredpredicateswiththis; + +public class TargetAlternative2 extends TargetWithAlternatives { +} diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetWithAlternatives.java b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetWithAlternatives.java index 0c87364e6..92fa68b2f 100644 --- a/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetWithAlternatives.java +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/requiredpredicateswiththis/TargetWithAlternatives.java @@ -2,5 +2,5 @@ public class TargetWithAlternatives { - public void doNothing(String word) {} + public void doNothing() {} } diff --git a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodUsesTest.java b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodUsesTest.java index cb5349b67..3cad3c79d 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodUsesTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodUsesTest.java @@ -182,7 +182,8 @@ public void avoidImproperKeyLenExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -202,7 +203,8 @@ public void avoidImproperKeyLenExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -216,7 +218,8 @@ public void avoidImproperKeyLenExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -230,7 +233,8 @@ public void avoidImproperKeyLenExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -240,7 +244,8 @@ public void avoidImproperKeyLenExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -343,7 +348,8 @@ public void avoidInsecurePaddingExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -363,7 +369,8 @@ public void avoidInsecurePaddingExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -383,7 +390,8 @@ public void avoidInsecurePaddingExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -779,7 +787,8 @@ public void secureConfigsRSAExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -799,7 +808,8 @@ public void secureConfigsRSAExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -813,7 +823,8 @@ public void secureConfigsRSAExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -827,7 +838,8 @@ public void secureConfigsRSAExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case @@ -847,7 +859,8 @@ public void secureConfigsRSAExamples() { // positive test case setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + // This is correct because there are two different 'SHA-256' variables, i.e. the pred is ensured on the first but not on the second one + setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); // negative test case diff --git a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java index c60eee177..07c306ab0 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java @@ -894,7 +894,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -904,7 +904,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -914,7 +914,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -924,7 +924,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -934,7 +934,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -944,7 +944,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -954,7 +954,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -964,7 +964,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", RequiredPredicateError.class, 5); + setErrorsCount("", RequiredPredicateError.class, 6); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -974,7 +974,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + setErrorsCount("", RequiredPredicateError.class, 1); // negative test case setErrorsCount("", TypestateError.class, 1); @@ -984,7 +984,7 @@ public void weakConfigsRSAExamples() { // positive test case setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", RequiredPredicateError.class, 0); + setErrorsCount("", RequiredPredicateError.class, 1); // negative test case setErrorsCount("", TypestateError.class, 1); diff --git a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/Source.crysl b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/Source.crysl index 20a727a40..eed43839a 100644 --- a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/Source.crysl +++ b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/Source.crysl @@ -4,17 +4,21 @@ OBJECTS boolean constraintError; tests.error.predicate.requiredpredicateswiththis.SimpleTarget target1; tests.error.predicate.requiredpredicateswiththis.TargetWithAlternatives target2; + tests.error.predicate.requiredpredicateswiththis.TargetAlternative1 target3; + tests.error.predicate.requiredpredicateswiththis.TargetAlternative2 target4; EVENTS Con: Source(); causeError: causeConstraintError(constraintError); passPred1: target1 = generateTarget(); passPred2: target2 = generateTargetWithAlternatives(); + passPred3: target3 = generateTargetAlternative1(); + passPred4: target4 = generateTargetAlternative2(); - passPred := passPred1 | passPred2; + passPred := passPred1 | passPred2 | passPred3 | passPred4; ORDER - Con, causeError, passPred + Con, causeError, passPred* CONSTRAINTS constraintError in {false}; @@ -22,3 +26,5 @@ CONSTRAINTS ENSURES generatedTarget[target1]; generatedTargetWithAlternatives[target2]; + generatedAlternative1[target3]; + generatedAlternative2[target4]; diff --git a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative1.crysl b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative1.crysl new file mode 100644 index 000000000..964147043 --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative1.crysl @@ -0,0 +1,4 @@ +SPEC tests.error.predicate.requiredpredicateswiththis.TargetAlternative1 + +REQUIRES + generatedAlternative1[this]; diff --git a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative2.crysl b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative2.crysl new file mode 100644 index 000000000..a17178763 --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetAlternative2.crysl @@ -0,0 +1,4 @@ +SPEC tests.error.predicate.requiredpredicateswiththis.TargetAlternative2 + +REQUIRES + generatedAlternative2[this]; diff --git a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetWithDifferentAlternatives.crysl b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetWithAlternatives.crysl similarity index 54% rename from CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetWithDifferentAlternatives.crysl rename to CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetWithAlternatives.crysl index b041f18ef..8eb8a6eb0 100644 --- a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetWithDifferentAlternatives.crysl +++ b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/TargetWithAlternatives.crysl @@ -1,14 +1,11 @@ SPEC tests.error.predicate.requiredpredicateswiththis.TargetWithAlternatives -OBJECTS - java.lang.String word; - EVENTS Con: TargetWithAlternatives(); - dN: doNothing(word); + dN: doNothing(); ORDER Con, dN* REQUIRES - generatedTargetWithAlternatives[this] || generatedWord[word]; + generatedTargetWithAlternatives[this] || generatedAlternative1[this] || generatedAlternative2[this]; diff --git a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/UsingTarget.crysl b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/UsingTarget.crysl index f159b052a..db3e39b07 100644 --- a/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/UsingTarget.crysl +++ b/CryptoAnalysis/src/test/resources/testrules/requiredPredicateWithThis/UsingTarget.crysl @@ -16,7 +16,7 @@ ORDER REQUIRES generatedTarget[target1]; - generatedTargetWithAlternatives[target2]; + generatedTargetWithAlternatives[target2] || generatedAlternative1[target2] || generatedAlternative2[target2]; ENSURES usedTarget[this]; diff --git a/CryptoAnalysis/src/test/resources/testrules/requiredPredicates/Requires.crysl b/CryptoAnalysis/src/test/resources/testrules/requiredPredicates/Requires.crysl index 87f51107e..f539d3120 100644 --- a/CryptoAnalysis/src/test/resources/testrules/requiredPredicates/Requires.crysl +++ b/CryptoAnalysis/src/test/resources/testrules/requiredPredicates/Requires.crysl @@ -191,7 +191,11 @@ REQUIRES pred1[p1inO2] || !pred1[p2inO2]; !pred1[p1inO3] || pred1[p2inO3]; !pred1[p1inO4] || !pred1[p2inO4]; - pred1[p1inO5] || pred2[p2inO5]; + + // pred1[p1inO5] or pred2[p2inO5]; + // !pred1[p1inO5] => pred2[p2inO5]; negated condition not supported + // !pred2[p2inO5] => pred1[p1inO5]; negated condition not supported + pred1[p1inO6] || !pred2[p2inO6]; !pred1[p1inO7] || pred2[p2inO7]; !pred1[p1inO8] || !pred2[p2inO8]; From b1866944d50bea72e9418f62c5a855559bc88dc4 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Sat, 6 Jul 2024 13:27:17 +0200 Subject: [PATCH 04/16] Simplify ensuring predicates on other seeds --- .../AnalysisSeedWithEnsuredPredicate.java | 4 - .../AnalysisSeedWithSpecification.java | 132 +++++++----------- .../java/crypto/analysis/CryptoScanner.java | 17 --- .../java/crypto/analysis/IAnalysisSeed.java | 4 - 4 files changed, 47 insertions(+), 110 deletions(-) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java index e2276566d..bc02e9939 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java @@ -18,10 +18,6 @@ public AnalysisSeedWithEnsuredPredicate(CryptoScanner scanner, Statement stateme super(scanner, statement, fact, results); } - public static AnalysisSeedWithEnsuredPredicate makeSeedForComparison(CryptoScanner scanner, Statement statement, Val fact) { - return new AnalysisSeedWithEnsuredPredicate(scanner, statement, fact, null); - } - @Override public void execute() { if (analysisResults == null) { diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index b92354b29..715bb0df2 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -5,7 +5,6 @@ import boomerang.scene.ControlFlowGraph; import boomerang.scene.DeclaredMethod; import boomerang.scene.Statement; -import boomerang.scene.Type; import boomerang.scene.Val; import com.google.common.collect.HashMultimap; import com.google.common.collect.Lists; @@ -64,7 +63,6 @@ public class AnalysisSeedWithSpecification extends IAnalysisSeed { private Map allCallsOnObject; private final Map>> ensuredPredicates = new HashMap<>(); - private final Collection indirectlyEnsuredPredicates = Sets.newHashSet(); private final Collection hiddenPredicates = Sets.newHashSet(); private final Collection resultHandlers = Sets.newHashSet(); @@ -74,10 +72,6 @@ public AnalysisSeedWithSpecification(CryptoScanner scanner, Statement statement, this.specification = specification; } - public static AnalysisSeedWithSpecification makeSeedForComparison(CryptoScanner scanner, Statement statement, Val fact, CrySLRule rule) { - return new AnalysisSeedWithSpecification(scanner, statement, fact, null, rule); - } - @Override public String toString() { return "AnalysisSeedWithSpec [" + super.toString() + " with spec " + specification.getClassName() + "]"; @@ -106,7 +100,6 @@ public void execute() { evaluateIncompleteOperations(); // Check the REQUIRES section and ensure predicates in ENSURES section - activateIndirectlyEnsuredPredicates(); checkConstraintsAndEnsurePredicates(); scanner.getAnalysisReporter().onSeedFinished(this); @@ -489,102 +482,71 @@ private Collection getTargetStates(TransitionFunction value) { * @param fact holds the value for the other seed's type */ private void expectPredicateOnOtherObject(EnsuredCrySLPredicate ensPred, Statement statement, Val fact) { - boolean specificationExists = false; - - // Check, whether there is a specification (i.e. a CrySL rule) for the target object - for (CrySLRule rule : scanner.getRuleset()) { - if (fact.isNull()) { - continue; - } + for (IAnalysisSeed otherSeed : scanner.getDiscoveredSeeds()) { + if (otherSeed.getFact().equals(fact) && otherSeed.getOrigin().equals(statement)) { + if (otherSeed instanceof AnalysisSeedWithSpecification) { + AnalysisSeedWithSpecification seedWithSpec = (AnalysisSeedWithSpecification) otherSeed; - Type baseType = fact.getType(); - if (!baseType.isRefType()) { - continue; - } - - if (baseType.getWrappedClass().getName().equals(rule.getClassName())) { - Optional seed = scanner.getSeedWithSpec(AnalysisSeedWithSpecification.makeSeedForComparison(scanner, statement, fact, rule)); + seedWithSpec.addEnsuredPredicateFromOtherRule(ensPred); + } else if (otherSeed instanceof AnalysisSeedWithEnsuredPredicate) { + AnalysisSeedWithEnsuredPredicate seedWithoutSpec = (AnalysisSeedWithEnsuredPredicate) otherSeed; - if (seed.isEmpty()) { - LOGGER.debug("{} has not been discovered in the Typestate Analysis", seed); - continue; + seedWithoutSpec.addEnsuredPredicate(ensPred); + predicateHandler.expectPredicate(seedWithoutSpec, statement, ensPred.getPredicate()); } - - seed.get().addEnsuredPredicateFromOtherRule(ensPred); - specificationExists = true; } } - - // If no specification has been found, create a seed without a specification - if (!specificationExists) { - Optional seed = scanner.getSeedWithoutSpec(AnalysisSeedWithEnsuredPredicate.makeSeedForComparison(scanner, statement, fact)); - - if (seed.isEmpty()) { - LOGGER.debug("{} has not been discovered in the Typestate Analysis", seed); - return; - } - - predicateHandler.expectPredicate(seed.get(), statement, ensPred.getPredicate()); - seed.get().addEnsuredPredicate(ensPred); - } } - private void addEnsuredPredicateFromOtherRule(EnsuredCrySLPredicate ensuredCrySLPredicate) { - indirectlyEnsuredPredicates.add(ensuredCrySLPredicate); + /** + * Check the predicates that were ensured from other seeds and passed to this seed + */ + private void addEnsuredPredicateFromOtherRule(EnsuredCrySLPredicate pred) { if (analysisResults == null) { return; } - activateIndirectlyEnsuredPredicates(); - } + Collection parameters = pred.getPredicate().getParameters(); + String specName = specification.getClassName(); + boolean hasThisParameter = parameters.stream().anyMatch(p -> p instanceof CrySLObject && ((CrySLObject) p).getJavaType().equals(specName)); - /** - * Activate the predicates that were ensured from other seeds and passed to this seed - */ - private void activateIndirectlyEnsuredPredicates() { - for (EnsuredCrySLPredicate pred : indirectlyEnsuredPredicates) { - Collection parameters = pred.getPredicate().getParameters(); - String specName = specification.getClassName(); - boolean hasThisParameter = parameters.stream().anyMatch(p -> p instanceof CrySLObject && ((CrySLObject) p).getJavaType().equals(specName)); - - if (!hasThisParameter) { - continue; - } + if (!hasThisParameter) { + return; + } - /* Replace the original parameter corresponding to this seed with 'this'. For example, - * the KeyGenerator ensures 'generatedKey[key, algorithm]' on a SecretKey 'key'. Therefore, - * the seed for the SecretKey ensures 'generated[this, algorithm]'. - */ - List updatedParams = parameters.stream().map( - p -> p instanceof CrySLObject && ((CrySLObject) p).getJavaType().equals(specName) ? - new CrySLObject("this", specName) : p).collect(Collectors.toList()); + /* Replace the original parameter corresponding to this seed with 'this'. For example, + * the KeyGenerator ensures 'generatedKey[key, algorithm]' on a SecretKey 'key'. Therefore, + * the seed for the SecretKey ensures 'generated[this, algorithm]'. + */ + List updatedParams = parameters.stream().map( + p -> p instanceof CrySLObject && ((CrySLObject) p).getJavaType().equals(specName) ? + new CrySLObject("this", specName) : p).collect(Collectors.toList()); - CrySLPredicate updatedPred = new CrySLPredicate(null, pred.getPredicate().getPredName(), updatedParams, false); + CrySLPredicate updatedPred = new CrySLPredicate(null, pred.getPredicate().getPredName(), updatedParams, false); - EnsuredCrySLPredicate predWithThis; - if (pred instanceof HiddenPredicate) { - HiddenPredicate hiddenPredicate = (HiddenPredicate) pred; - predWithThis = new HiddenPredicate(updatedPred, hiddenPredicate.getParametersToValues(), hiddenPredicate.getGeneratingSeed(), hiddenPredicate.getType()); - } else { - predWithThis = new EnsuredCrySLPredicate(updatedPred, pred.getParametersToValues()); - } + EnsuredCrySLPredicate predWithThis; + if (pred instanceof HiddenPredicate) { + HiddenPredicate hiddenPredicate = (HiddenPredicate) pred; + predWithThis = new HiddenPredicate(updatedPred, hiddenPredicate.getParametersToValues(), hiddenPredicate.getGeneratingSeed(), hiddenPredicate.getType()); + } else { + predWithThis = new EnsuredCrySLPredicate(updatedPred, pred.getParametersToValues()); + } - /* Add the predicate with 'this' to the ensured predicates, check the required predicate constraints - * and ensure it in all accepting states that do not negate it - */ - for (Table.Cell c : analysisResults.asStatementValWeightTable().cellSet()) { - Collection states = getTargetStates(c.getValue()); + /* Add the predicate with 'this' to the ensured predicates, check the required predicate constraints + * and ensure it in all accepting states that do not negate it + */ + for (Table.Cell c : analysisResults.asStatementValWeightTable().cellSet()) { + Collection states = getTargetStates(c.getValue()); - for (State state : states) { - if (isPredicateNegatingState(predWithThis.getPredicate(), state)) { - continue; - } + for (State state : states) { + if (isPredicateNegatingState(predWithThis.getPredicate(), state)) { + continue; + } - Statement statement = c.getRowKey().getStart(); - Val val = c.getColumnKey(); - if (state.isAccepting()) { - predicateHandler.addNewPred(this, statement, val, predWithThis); - } + Statement statement = c.getRowKey().getStart(); + Val val = c.getColumnKey(); + if (state.isAccepting()) { + predicateHandler.addNewPred(this, statement, val, predWithThis); } } } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/CryptoScanner.java b/CryptoAnalysis/src/main/java/crypto/analysis/CryptoScanner.java index 10675af75..c7fdb9f05 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/CryptoScanner.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/CryptoScanner.java @@ -20,7 +20,6 @@ import java.util.HashSet; import java.util.List; import java.util.Map; -import java.util.Optional; import java.util.Set; public abstract class CryptoScanner { @@ -118,22 +117,6 @@ public Collection getAnalysisSeedsWithSpec() { return seeds; } - public Optional getSeedWithSpec(AnalysisSeedWithSpecification seedAtStatement) { - if (discoveredSeeds.containsKey(seedAtStatement)) { - AnalysisSeedWithSpecification seed = (AnalysisSeedWithSpecification) discoveredSeeds.get(seedAtStatement); - return Optional.of(seed); - } - return Optional.empty(); - } - - public Optional getSeedWithoutSpec(AnalysisSeedWithEnsuredPredicate seedAtStatement) { - if (discoveredSeeds.containsKey(seedAtStatement)) { - AnalysisSeedWithEnsuredPredicate seed = (AnalysisSeedWithEnsuredPredicate) discoveredSeeds.get(seedAtStatement); - return Optional.of(seed); - } - return Optional.empty(); - } - public PredicateHandler getPredicateHandler() { return predicateHandler; } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java b/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java index f33063229..b51328e8b 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java @@ -6,8 +6,6 @@ import boomerang.scene.Type; import boomerang.scene.Val; import crypto.analysis.errors.AbstractError; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; import typestate.TransitionFunction; import java.math.BigInteger; @@ -18,8 +16,6 @@ public abstract class IAnalysisSeed { - protected static final Logger LOGGER = LoggerFactory.getLogger(IAnalysisSeed.class); - protected final CryptoScanner scanner; protected final PredicateHandler predicateHandler; protected final Collection errorCollection; From 3d7ef6feedbb6fe936ad66f2f275b995aa71dd6e Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 8 Jul 2024 04:04:14 +0000 Subject: [PATCH 05/16] Bump com.fasterxml.jackson.core:jackson-databind from 2.17.1 to 2.17.2 Bumps [com.fasterxml.jackson.core:jackson-databind](https://github.com/FasterXML/jackson) from 2.17.1 to 2.17.2. - [Commits](https://github.com/FasterXML/jackson/commits) --- updated-dependencies: - dependency-name: com.fasterxml.jackson.core:jackson-databind dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] --- CryptoAnalysis/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CryptoAnalysis/pom.xml b/CryptoAnalysis/pom.xml index 11a8eb0db..d0a8f5a9d 100644 --- a/CryptoAnalysis/pom.xml +++ b/CryptoAnalysis/pom.xml @@ -394,7 +394,7 @@ com.fasterxml.jackson.core jackson-databind - 2.17.1 + 2.17.2 commons-io From 7d6ccfae3cc974d44763b2358307fc5b2560099d Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 8 Jul 2024 04:04:18 +0000 Subject: [PATCH 06/16] Bump com.fasterxml.jackson.core:jackson-core from 2.17.1 to 2.17.2 Bumps [com.fasterxml.jackson.core:jackson-core](https://github.com/FasterXML/jackson-core) from 2.17.1 to 2.17.2. - [Commits](https://github.com/FasterXML/jackson-core/compare/jackson-core-2.17.1...jackson-core-2.17.2) --- updated-dependencies: - dependency-name: com.fasterxml.jackson.core:jackson-core dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] --- CryptoAnalysis/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CryptoAnalysis/pom.xml b/CryptoAnalysis/pom.xml index 11a8eb0db..df5d54355 100644 --- a/CryptoAnalysis/pom.xml +++ b/CryptoAnalysis/pom.xml @@ -389,7 +389,7 @@ com.fasterxml.jackson.core jackson-core - 2.17.1 + 2.17.2 com.fasterxml.jackson.core From bb80044473beab972c85680135899cab701aa1c2 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 8 Jul 2024 04:04:20 +0000 Subject: [PATCH 07/16] Bump com.google.crypto.tink:tink from 1.3.0 to 1.14.0 Bumps [com.google.crypto.tink:tink](https://github.com/tink-crypto/tink-java) from 1.3.0 to 1.14.0. - [Release notes](https://github.com/tink-crypto/tink-java/releases) - [Commits](https://github.com/tink-crypto/tink-java/commits/v1.14.0) --- updated-dependencies: - dependency-name: com.google.crypto.tink:tink dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] --- CryptoAnalysis/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CryptoAnalysis/pom.xml b/CryptoAnalysis/pom.xml index 11a8eb0db..401dfd331 100644 --- a/CryptoAnalysis/pom.xml +++ b/CryptoAnalysis/pom.xml @@ -349,7 +349,7 @@ com.google.crypto.tink tink - 1.3.0 + 1.14.0 From 637d2740fc97063c985539a203f25de8ad596245 Mon Sep 17 00:00:00 2001 From: svenfeld Date: Mon, 8 Jul 2024 12:03:19 +0200 Subject: [PATCH 08/16] Use EciesKeyManager instead of deprecated HybridKeyTemplates --- .../java/tests/tink/TestHybridEncryption.java | 40 ++++++------------- 1 file changed, 12 insertions(+), 28 deletions(-) diff --git a/CryptoAnalysis/src/test/java/tests/tink/TestHybridEncryption.java b/CryptoAnalysis/src/test/java/tests/tink/TestHybridEncryption.java index ca2d1d781..a5a77cff1 100644 --- a/CryptoAnalysis/src/test/java/tests/tink/TestHybridEncryption.java +++ b/CryptoAnalysis/src/test/java/tests/tink/TestHybridEncryption.java @@ -4,13 +4,14 @@ import com.google.crypto.tink.HybridEncrypt; import com.google.crypto.tink.KeysetHandle; import com.google.crypto.tink.aead.AeadKeyTemplates; +import com.google.crypto.tink.hybrid.EciesAeadHkdfPrivateKeyManager; import com.google.crypto.tink.hybrid.HybridDecryptFactory; import com.google.crypto.tink.hybrid.HybridEncryptFactory; import com.google.crypto.tink.hybrid.HybridKeyTemplates; import com.google.crypto.tink.proto.EcPointFormat; import com.google.crypto.tink.proto.EllipticCurveType; import com.google.crypto.tink.proto.HashType; -import com.google.crypto.tink.proto.KeyTemplate; +import com.google.crypto.tink.KeyTemplate; import org.junit.Ignore; import org.junit.Test; import test.TestConstants; @@ -28,12 +29,9 @@ protected String getRulesetPath() { @Test public void generateNewECIES_P256_HKDF_HMAC_SHA256_AES128_GCMKeySet() throws GeneralSecurityException { - KeyTemplate kt = HybridKeyTemplates.createEciesAeadHkdfKeyTemplate(EllipticCurveType.NIST_P256, - HashType.SHA256, - EcPointFormat.UNCOMPRESSED, - AeadKeyTemplates.AES128_GCM, - new byte[0]); - + + KeyTemplate kt = EciesAeadHkdfPrivateKeyManager.eciesP256HkdfHmacSha256Aes128GcmTemplate(); + KeysetHandle ksh = KeysetHandle.generateNew(kt); Assertions.hasEnsuredPredicate(kt); Assertions.mustBeInAcceptingState(kt); @@ -42,13 +40,10 @@ public void generateNewECIES_P256_HKDF_HMAC_SHA256_AES128_GCMKeySet() throws Gen @Test public void generateNewECIES_P256_HKDF_HMAC_SHA256_AES128_CTR_HMAC_SHA256KeySet() throws GeneralSecurityException { - KeyTemplate kt = HybridKeyTemplates.createEciesAeadHkdfKeyTemplate( - EllipticCurveType.NIST_P256, - HashType.SHA256, - EcPointFormat.UNCOMPRESSED, - AeadKeyTemplates.AES128_CTR_HMAC_SHA256, - new byte[0]); - + + + + KeyTemplate kt = EciesAeadHkdfPrivateKeyManager.eciesP256HkdfHmacSha256Aes128CtrHmacSha256Template(); KeysetHandle ksh = KeysetHandle.generateNew(kt); Assertions.hasEnsuredPredicate(kt); Assertions.mustBeInAcceptingState(kt); @@ -61,15 +56,10 @@ public void generateInvalidKey() { Assertions.notHasEnsuredPredicate(kt); } - + @Test public void encryptUsingECIES_P256_HKDF_HMAC_SHA256_AES128_CTR_HMAC_SHA256KeySet() throws GeneralSecurityException { - KeyTemplate kt = HybridKeyTemplates.createEciesAeadHkdfKeyTemplate( - EllipticCurveType.NIST_P256, - HashType.SHA256, - EcPointFormat.UNCOMPRESSED, - AeadKeyTemplates.AES128_CTR_HMAC_SHA256, - new byte[0]); + KeyTemplate kt = EciesAeadHkdfPrivateKeyManager.eciesP256HkdfHmacSha256Aes128CtrHmacSha256Template(); KeysetHandle ksh = KeysetHandle.generateNew(kt); KeysetHandle publicKsh = ksh.getPublicKeysetHandle(); @@ -88,13 +78,7 @@ public void encryptUsingECIES_P256_HKDF_HMAC_SHA256_AES128_CTR_HMAC_SHA256KeySet @Test public void decryptUsingECIES_P256_HKDF_HMAC_SHA256_AES128_CTR_HMAC_SHA256KeySet() throws GeneralSecurityException { - KeyTemplate kt = HybridKeyTemplates.createEciesAeadHkdfKeyTemplate( - EllipticCurveType.NIST_P256, - HashType.SHA256, - EcPointFormat.UNCOMPRESSED, - AeadKeyTemplates.AES128_CTR_HMAC_SHA256, - new byte[0]); - + KeyTemplate kt = EciesAeadHkdfPrivateKeyManager.eciesP256HkdfHmacSha256Aes128CtrHmacSha256Template(); KeysetHandle ksh = KeysetHandle.generateNew(kt); HybridDecrypt cipher = HybridDecryptFactory.getPrimitive(ksh); From b59df09cca677660f615682b3b122c24d027fc3a Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 15 Jul 2024 04:04:41 +0000 Subject: [PATCH 09/16] Bump org.apache.maven.plugins:maven-surefire-plugin from 3.3.0 to 3.3.1 Bumps [org.apache.maven.plugins:maven-surefire-plugin](https://github.com/apache/maven-surefire) from 3.3.0 to 3.3.1. - [Release notes](https://github.com/apache/maven-surefire/releases) - [Commits](https://github.com/apache/maven-surefire/compare/surefire-3.3.0...surefire-3.3.1) --- updated-dependencies: - dependency-name: org.apache.maven.plugins:maven-surefire-plugin dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] --- CryptoAnalysis/pom.xml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CryptoAnalysis/pom.xml b/CryptoAnalysis/pom.xml index 5106dc5e5..bf2898896 100644 --- a/CryptoAnalysis/pom.xml +++ b/CryptoAnalysis/pom.xml @@ -134,7 +134,7 @@ org.apache.maven.plugins maven-surefire-plugin - 3.3.0 + 3.3.1 false -Xmx8G -Xms256M -Xss8M -Dmaven.home="${maven.home}" @@ -145,7 +145,7 @@ org.apache.maven.surefire surefire-junit4 - 3.3.0 + 3.3.1 junit From 95e9d90ba8857b769faf7bc8ec29270fe6f57a58 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 15 Jul 2024 04:04:55 +0000 Subject: [PATCH 10/16] Bump org.apache.maven.plugins:maven-release-plugin from 3.1.0 to 3.1.1 Bumps [org.apache.maven.plugins:maven-release-plugin](https://github.com/apache/maven-release) from 3.1.0 to 3.1.1. - [Release notes](https://github.com/apache/maven-release/releases) - [Commits](https://github.com/apache/maven-release/compare/maven-release-3.1.0...maven-release-3.1.1) --- updated-dependencies: - dependency-name: org.apache.maven.plugins:maven-release-plugin dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] --- pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pom.xml b/pom.xml index 9ceac5e81..f4d909ad2 100644 --- a/pom.xml +++ b/pom.xml @@ -88,7 +88,7 @@ org.apache.maven.plugins maven-release-plugin - 3.1.0 + 3.1.1 @{project.version} From bf516dbd2f270a80cd16124e99b9d39ec610ac58 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 15 Jul 2024 04:04:56 +0000 Subject: [PATCH 11/16] Bump org.apache.maven.surefire:surefire-junit4 from 3.3.0 to 3.3.1 Bumps org.apache.maven.surefire:surefire-junit4 from 3.3.0 to 3.3.1. --- updated-dependencies: - dependency-name: org.apache.maven.surefire:surefire-junit4 dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] --- CryptoAnalysis/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CryptoAnalysis/pom.xml b/CryptoAnalysis/pom.xml index 5106dc5e5..cfebe3aa7 100644 --- a/CryptoAnalysis/pom.xml +++ b/CryptoAnalysis/pom.xml @@ -145,7 +145,7 @@ org.apache.maven.surefire surefire-junit4 - 3.3.0 + 3.3.1 junit From aba497ffab89cc274bfa47313cb8c54fcfe1deef Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Thu, 18 Jul 2024 10:19:53 +0200 Subject: [PATCH 12/16] Adapt test case from #215 --- .../AnalysisSeedWithSpecification.java | 25 +++++++------------ .../MatcherTransitionCollection.java | 12 +++------ .../test/java/tests/jca/BouncyCastleTest.java | 3 +++ 3 files changed, 16 insertions(+), 24 deletions(-) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index 715bb0df2..682dadd91 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -162,33 +162,26 @@ private Optional isForbiddenMethod(DeclaredMethod declared private void evaluateTypestateOrder() { Collection allTypestateChangeStatements = new HashSet<>(); for (Table.Cell cell : analysisResults.asStatementValWeightTable().cellSet()) { - allTypestateChangeStatements.addAll(cell.getValue().getLastStateChangeStatements()); + Collection edges = cell.getValue().getLastStateChangeStatements(); + allTypestateChangeStatements.addAll(edges); } for (Table.Cell c : analysisResults.asStatementValWeightTable().cellSet()) { ControlFlowGraph.Edge curr = c.getRowKey(); - // For some reason, constructors are the start and not the target statement... - Statement errorStatement; - Statement start = curr.getStart(); - Statement target = curr.getTarget(); - if (start.containsInvokeExpr()) { - DeclaredMethod declaredMethod = start.getInvokeExpr().getMethod(); - - if (declaredMethod.isConstructor()) { - errorStatement = start; - } else { - errorStatement = target; - } + // 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 { - errorStatement = target; + typestateChangeStatement = curr.getTarget(); } if (allTypestateChangeStatements.contains(curr)) { Collection targetStates = getTargetStates(c.getValue()); for (State newStateAtCurr : targetStates) { - typeStateChangeAtStatement(errorStatement, newStateAtCurr); + typeStateChangeAtStatement(typestateChangeStatement, newStateAtCurr); } } } @@ -465,7 +458,7 @@ private boolean containsTargetState(TransitionFunction value, State stateNode) { return getTargetStates(value).contains(stateNode); } - private Collection getTargetStates(TransitionFunction value) { + private Collection getTargetStates(TransitionFunction value) { Collection res = Sets.newHashSet(); for (ITransition t : value.values()) { if (t.to() != null) diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/MatcherTransitionCollection.java b/CryptoAnalysis/src/main/java/crypto/typestate/MatcherTransitionCollection.java index 55a6f43c6..5b35583bb 100644 --- a/CryptoAnalysis/src/main/java/crypto/typestate/MatcherTransitionCollection.java +++ b/CryptoAnalysis/src/main/java/crypto/typestate/MatcherTransitionCollection.java @@ -85,11 +85,7 @@ private TransitionFunction getDefaultTransitionFunction(ControlFlowGraph.Edge st return new TransitionFunction(initialTransitions, Collections.singleton(stmt)); } - public Collection getInitialTransitions() { - return smg.getInitialTransitions(); - } - - public Set getAllTransitions() { + public Collection getAllTransitions() { return transitions; } @@ -115,18 +111,18 @@ private void initializeErrorTransitions() { for (StateNode node : smg.getNodes()) { // Collect the methods that are on an outgoing edge - Set existingMethods = new HashSet<>(); + Collection existingMethods = new HashSet<>(); for (TransitionEdge edge : smg.getAllOutgoingEdges(node)) { existingMethods.addAll(edge.getLabel()); } // Remove the existing methods; all remaining methods lead to an error state - Set remainingMethods = new HashSet<>(allMethods); + Collection remainingMethods = new HashSet<>(allMethods); remainingMethods.removeAll(existingMethods); // Create the error state, where typestate errors are reported WrappedState state = createWrappedState(node); - ReportingErrorStateNode repErrorState = new ReportingErrorStateNode(remainingMethods); + ReportingErrorStateNode repErrorState = new ReportingErrorStateNode(existingMethods); LabeledMatcherTransition repErrorTransition = new LabeledMatcherTransition(state, remainingMethods, repErrorState); transitions.add(repErrorTransition); diff --git a/CryptoAnalysis/src/test/java/tests/jca/BouncyCastleTest.java b/CryptoAnalysis/src/test/java/tests/jca/BouncyCastleTest.java index 42694eaa0..96505cd20 100644 --- a/CryptoAnalysis/src/test/java/tests/jca/BouncyCastleTest.java +++ b/CryptoAnalysis/src/test/java/tests/jca/BouncyCastleTest.java @@ -117,6 +117,9 @@ public void testORingTwoPredicates2() throws IllegalStateException, InvalidCiphe GCMBlockCipher cipher1 = (GCMBlockCipher) GCMBlockCipher.newInstance(engine); cipher1.init(false, params); cipher1.processAADBytes(input, 0, input.length); + Assertions.hasEnsuredPredicate(cipher1); + + // Missing call to 'processBytes' causes TypestateError -> No predicate at 'doFinal' call cipher1.doFinal(output, 0); Assertions.notHasEnsuredPredicate(cipher1); Assertions.mustNotBeInAcceptingState(cipher1); From 98aeed956790a05508ddb53209bf347070617366 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Thu, 18 Jul 2024 13:07:20 +0200 Subject: [PATCH 13/16] Add test case from #227 --- .../crypto/reporting/ReportGenerator.java | 2 +- .../tests/headless/ReportedIssueTest.java | 2 + .../java/issue227/AbstractWrappedHasher.java | 8 ++++ .../src/main/java/issue227/Hasher.java | 6 +++ .../src/main/java/issue227/Main.java | 17 ++++++++ .../src/main/java/issue227/WrappedHasher.java | 41 +++++++++++++++++++ 6 files changed, 75 insertions(+), 1 deletion(-) create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/AbstractWrappedHasher.java create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Hasher.java create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Main.java create mode 100644 CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/WrappedHasher.java diff --git a/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java b/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java index 4f5cf2f67..bde3ab961 100644 --- a/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java +++ b/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java @@ -9,7 +9,6 @@ import crypto.utils.ErrorUtils; import java.util.Collection; -import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Set; @@ -38,6 +37,7 @@ public static String generateReport(Collection seeds, Collection< report.append("\t\tVariable: ").append(seed.getFact().getVariableName()).append("\n"); report.append("\t\tType: ").append(seed.getType()).append("\n"); report.append("\t\tStatement: ").append(seed.getOrigin()).append("\n"); + report.append("\t\tLine: ").append(seed.getOrigin().getStartLineNumber()).append("\n"); report.append("\t\tMethod: ").append(seed.getMethod()).append("\n"); report.append("\t\tSHA-256: ").append(seed.getObjectId()).append("\n"); report.append("\t\tSecure: ").append(seed.isSecure()).append("\n"); diff --git a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java index 720dfbdc3..bf919d9f9 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java @@ -21,6 +21,8 @@ public void reportedIssues() { setErrorsCount("", RequiredPredicateError.class, 1); + setErrorsCount("", TypestateError.class, 0); + setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", RequiredPredicateError.class, 1); diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/AbstractWrappedHasher.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/AbstractWrappedHasher.java new file mode 100644 index 000000000..294831293 --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/AbstractWrappedHasher.java @@ -0,0 +1,8 @@ +package issue227; + +public abstract class AbstractWrappedHasher { + + public abstract void update(byte b); + + public abstract void putLong(long l); +} diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Hasher.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Hasher.java new file mode 100644 index 000000000..8bbd6b3e7 --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Hasher.java @@ -0,0 +1,6 @@ +package issue227; + +public interface Hasher { + + byte[] hash(); +} diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Main.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Main.java new file mode 100644 index 000000000..80d11cf3d --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/Main.java @@ -0,0 +1,17 @@ +package issue227; + +import java.util.Arrays; + +public class Main { + + public static void main(String[] args) { + String algorithmName = "SHA-256"; + WrappedHasher wrappedHasher = new WrappedHasher(algorithmName); + + long l = 123L; + wrappedHasher.putLong(l); + + byte[] hash = wrappedHasher.hash(); + System.out.println("Got " + Arrays.toString(hash)); + } +} diff --git a/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/WrappedHasher.java b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/WrappedHasher.java new file mode 100644 index 000000000..cdafaa84f --- /dev/null +++ b/CryptoAnalysisTargets/ReportedIssues/src/main/java/issue227/WrappedHasher.java @@ -0,0 +1,41 @@ +package issue227; + +import java.nio.ByteBuffer; +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; + +public class WrappedHasher extends AbstractWrappedHasher implements Hasher { + + private final MessageDigest md; + + public WrappedHasher(String algorithmName) { + try { + md = MessageDigest.getInstance(algorithmName); + } catch (NoSuchAlgorithmException e) { + throw new RuntimeException(e); + } + } + + @Override + public void update(byte b) { + md.update(b); + } + + public void update(byte[] b) { + md.update(b); + } + + @Override + public void putLong(long l) { + ByteBuffer buffer = ByteBuffer.allocate((int) l); + buffer.putLong(l); + + byte[] array = buffer.array(); + update(array); + } + + @Override + public byte[] hash() { + return md.digest(); + } +} From e88ecf5a68d7f08ab55896a7367b6a8caca588c0 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Thu, 18 Jul 2024 15:53:54 +0200 Subject: [PATCH 14/16] Add test case from #271 --- .../tests/headless/ReportedIssueTest.java | 17 ++++++ .../KotlinExamples/Issue271/pom.xml | 56 +++++++++++++++++++ .../src/main/java/example/Issue271Kotlin.kt | 17 ++++++ .../src/main/java/example/Issue271Java.java | 21 +++++++ 4 files changed, 111 insertions(+) create mode 100644 CryptoAnalysisTargets/KotlinExamples/Issue271/pom.xml create mode 100644 CryptoAnalysisTargets/KotlinExamples/Issue271/src/main/java/example/Issue271Kotlin.kt create mode 100644 CryptoAnalysisTargets/KotlinExamples/issue271/src/main/java/example/Issue271Java.java diff --git a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java index bf919d9f9..90ab65f79 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/ReportedIssueTest.java @@ -77,4 +77,21 @@ public void reportedIssues() { scanner.run(); assertErrors(scanner.getErrorCollection()); } + + @Test + public void issue271Test() { + // Related to https://github.com/CROSSINGTUD/CryptoAnalysis/issues/271 + String mavenProjectPath = new File("../CryptoAnalysisTargets/KotlinExamples/Issue271").getAbsolutePath(); + MavenProject mavenProject = createAndCompile(mavenProjectPath); + HeadlessCryptoScanner scanner = createScanner(mavenProject); + + setErrorsCount("", IncompleteOperationError.class, 0); + setErrorsCount("", IncompleteOperationError.class, 0); + + setErrorsCount("", IncompleteOperationError.class, 0); + setErrorsCount("", IncompleteOperationError.class, 0); + + scanner.run(); + assertErrors(scanner.getErrorCollection()); + } } diff --git a/CryptoAnalysisTargets/KotlinExamples/Issue271/pom.xml b/CryptoAnalysisTargets/KotlinExamples/Issue271/pom.xml new file mode 100644 index 000000000..094ae61b2 --- /dev/null +++ b/CryptoAnalysisTargets/KotlinExamples/Issue271/pom.xml @@ -0,0 +1,56 @@ + + + + 4.0.0 + + example + Issue271 + 0.0.1-SNAPSHOT + issue271 + + + 2.0.0 + + + + + org.jetbrains.kotlin + kotlin-stdlib + ${kotlin.version} + + + + + + + org.jetbrains.kotlin + kotlin-maven-plugin + ${kotlin.version} + + + compile + process-sources + + compile + + + + test-compile + + test-compile + + + + + + maven-compiler-plugin + 3.8.0 + + 11 + 11 + + + + + diff --git a/CryptoAnalysisTargets/KotlinExamples/Issue271/src/main/java/example/Issue271Kotlin.kt b/CryptoAnalysisTargets/KotlinExamples/Issue271/src/main/java/example/Issue271Kotlin.kt new file mode 100644 index 000000000..490d9788f --- /dev/null +++ b/CryptoAnalysisTargets/KotlinExamples/Issue271/src/main/java/example/Issue271Kotlin.kt @@ -0,0 +1,17 @@ +package example; + +import java.security.MessageDigest + +fun main() { + testFail("abc123ABC") + testOk("abc123ABC") +} + +fun testFail(input: String) { + val someManipulation = input.substring(0, 2) + MessageDigest.getInstance("SHA-256").digest(someManipulation.toByteArray()) +} + +fun testOk(input: String) { + MessageDigest.getInstance("SHA-256").digest(input.toByteArray()) +} diff --git a/CryptoAnalysisTargets/KotlinExamples/issue271/src/main/java/example/Issue271Java.java b/CryptoAnalysisTargets/KotlinExamples/issue271/src/main/java/example/Issue271Java.java new file mode 100644 index 000000000..154deaa00 --- /dev/null +++ b/CryptoAnalysisTargets/KotlinExamples/issue271/src/main/java/example/Issue271Java.java @@ -0,0 +1,21 @@ +package example; + +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; + +public class Issue271Java { + + public static void main(String [] args) throws NoSuchAlgorithmException { + testFail("abc123ABC"); + testOk("abc123ABC"); + } + + public static void testFail(String input) throws NoSuchAlgorithmException { + String someManipulation = input.substring(0, 2); + MessageDigest.getInstance("SHA-256").digest(someManipulation.getBytes()); + } + + public static void testOk(String input) throws NoSuchAlgorithmException { + MessageDigest.getInstance("SHA-256").digest(input.getBytes()); + } +} From 39ea59e35317879e8643dbdc7867503ec10c268f Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 22 Jul 2024 04:53:20 +0000 Subject: [PATCH 15/16] Bump org.apache.maven.plugins:maven-javadoc-plugin from 3.7.0 to 3.8.0 Bumps [org.apache.maven.plugins:maven-javadoc-plugin](https://github.com/apache/maven-javadoc-plugin) from 3.7.0 to 3.8.0. - [Release notes](https://github.com/apache/maven-javadoc-plugin/releases) - [Commits](https://github.com/apache/maven-javadoc-plugin/compare/maven-javadoc-plugin-3.7.0...maven-javadoc-plugin-3.8.0) --- updated-dependencies: - dependency-name: org.apache.maven.plugins:maven-javadoc-plugin dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] --- pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pom.xml b/pom.xml index f4d909ad2..9058edb9a 100644 --- a/pom.xml +++ b/pom.xml @@ -152,7 +152,7 @@ it has to be correct. --> org.apache.maven.plugins maven-javadoc-plugin - 3.7.0 + 3.8.0 attach-javadoc From fee624ff4e23cc067af3b1f4427aa540a19a40a8 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 22 Jul 2024 04:53:26 +0000 Subject: [PATCH 16/16] Bump org.apache.commons:commons-lang3 from 3.14.0 to 3.15.0 Bumps org.apache.commons:commons-lang3 from 3.14.0 to 3.15.0. --- updated-dependencies: - dependency-name: org.apache.commons:commons-lang3 dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] --- CryptoAnalysis/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CryptoAnalysis/pom.xml b/CryptoAnalysis/pom.xml index bf2898896..cd8b946e8 100644 --- a/CryptoAnalysis/pom.xml +++ b/CryptoAnalysis/pom.xml @@ -405,7 +405,7 @@ org.apache.commons commons-lang3 - 3.14.0 + 3.15.0 info.picocli