From a131e3b5f99f824edb4c95d70913c44b87b9508b Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Mon, 8 Sep 2025 12:57:05 +0200 Subject: [PATCH 1/5] Fix predicate after logic --- .../AnalysisSeedWithSpecification.java | 72 +++++++++++++- .../java/crypto/analysis/IAnalysisSeed.java | 2 +- .../crypto/extractparameter/UnknownVal.java | 20 ++++ .../crypto/predicates/UnEnsuredPredicate.java | 8 +- .../src/test/java/test/TestRules.java | 2 + .../flowsensitivity/PredicateAfterTest.java | 94 +++++++++++++++++++ .../flowsensitivity/PredicateBranching.java | 19 ++++ .../flowsensitivity/PredicateGenerator.java | 19 ++++ .../flowsensitivity/PredicateReceiver.java | 15 +++ .../flowSensitivity/PredicateBranching.crysl | 12 +++ .../flowSensitivity/PredicateGenerator.crysl | 11 +++ .../flowSensitivity/PredicateReceiver.crysl | 13 +++ .../handler/OpalFrameworkHandler.java | 7 +- pom.xml | 2 +- 14 files changed, 285 insertions(+), 11 deletions(-) create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java create mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl create mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl create mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index 7e74bb25a..b68721aef 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -46,6 +46,7 @@ import java.util.Objects; import java.util.Optional; import java.util.stream.Collectors; +import typestate.StatementSequence; import typestate.TransitionFunction; import typestate.finiteautomata.State; import typestate.finiteautomata.Transition; @@ -174,7 +175,7 @@ private void evaluateIncompleteOperations() { Table weights = analysisResults.computeFinalWeights(); for (TransitionFunction weight : weights.values()) { - for (Transition transition : weight.getStateChangeStatements().keySet()) { + for (Transition transition : weight.getStateChangeSequences().keySet()) { State targetState = transition.to(); if (targetState.isAccepting()) { @@ -188,10 +189,19 @@ private void evaluateIncompleteOperations() { } if (t.getLeft().equals(wrappedState.delegate())) { - Collection lastStatements = - weight.getStateChangeStatements().get(transition); Collection labels = t.getLabel(); + Collection stmtSequences = + weight.getStateChangeSequences().get(transition); + Collection lastStatements = + stmtSequences.stream() + .map( + e -> + e.getSequence() + .get(e.getSequence().size() - 1) + .getStatement()) + .toList(); + for (Statement stmt : lastStatements) { incompleteOperations.putAll(stmt, labels); } @@ -418,6 +428,19 @@ private void propagatePredicate( allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateMayNotBeReached); } + /* To ensure a predicate with an 'after' condition, we have to make sure that there is + * no sequence of calls that does not contain an event from the 'after' event. If there + * is a sequence, we cannot ensure the predicate (over approximation) + */ + if (predicate instanceof CrySLCondPredicate condPredicate) { + boolean generatingEventMissing = + isGeneratingEventMissing(statement, condPredicate.getConditionalEvents()); + + if (generatingEventMissing) { + allViolations.add(UnEnsuredPredicate.Violations.GeneratingEventIsNotCalled); + } + } + if (isIndirectlyEnsured) { propagateIndirectlyEnsuredPredicate( predicate.toNormalCrySLPredicate(), statement, allViolations); @@ -428,6 +451,45 @@ private void propagatePredicate( } } + private boolean isGeneratingEventMissing(Statement statement, Collection events) { + Collection weights = statementValWeightTable.row(statement).values(); + + for (TransitionFunction weight : weights) { + Collection sequences = weight.getStateChangeSequences().values(); + + /* Check whether there is a sequence of calls that does not contain a method + * from the 'after' condition; + */ + for (StatementSequence sequence : sequences) { + if (isSequenceWithoutEvent(sequence, events)) { + return true; + } + } + } + return false; + } + + private boolean isSequenceWithoutEvent( + StatementSequence sequence, Collection events) { + for (StatementSequence.Entry entry : sequence.getSequence()) { + Statement statement = entry.getStatement(); + + if (!statement.containsInvokeExpr()) { + continue; + } + + DeclaredMethod declaredMethod = statement.getInvokeExpr().getDeclaredMethod(); + for (CrySLMethod event : events) { + // If the call matches at least one event, there is a corresponding call + if (MatcherUtils.matchCryslMethodAndDeclaredMethod(event, declaredMethod)) { + return false; + } + } + } + + return true; + } + private void propagateIndirectlyEnsuredPredicate( CrySLPredicate predicate, Statement statement, @@ -639,7 +701,7 @@ private boolean isPredicateGeneratingState(CrySLPredicate ensPred, State stateNo // Predicate has a condition, i.e. "after" is specified -> Active predicate for // corresponding states if (ensPred instanceof CrySLCondPredicate condPred) { - if (isConditionalState(condPred.getConditionalMethods(), stateNode)) { + if (isConditionalState(condPred.getConditionalNodes(), stateNode)) { return true; } } @@ -681,7 +743,7 @@ private boolean isPredicateNegatingState(CrySLPredicate ensPred, State stateNode return true; } - for (StateNode s : condNegPred.getConditionalMethods()) { + for (StateNode s : condNegPred.getConditionalNodes()) { if (WrappedState.of(s).equals(stateNode)) { return true; } diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java b/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java index 15c2f2d7b..09a1a19b1 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java @@ -92,7 +92,7 @@ public Collection getStatesAtStatement(Statement statement) { private Collection getTargetStates(TransitionFunctionImpl transitionFunction) { Collection states = new HashSet<>(); - for (Transition transition : transitionFunction.getStateChangeStatements().keySet()) { + for (Transition transition : transitionFunction.getStateChangeSequences().keySet()) { states.add(transition.to()); } diff --git a/CryptoAnalysis/src/main/java/crypto/extractparameter/UnknownVal.java b/CryptoAnalysis/src/main/java/crypto/extractparameter/UnknownVal.java index 3dcecaa21..ac0fb440e 100644 --- a/CryptoAnalysis/src/main/java/crypto/extractparameter/UnknownVal.java +++ b/CryptoAnalysis/src/main/java/crypto/extractparameter/UnknownVal.java @@ -154,6 +154,26 @@ public long getLongValue() { throw new RuntimeException("Unknown Val is not a long constant"); } + @Override + public boolean isFloatConstant() { + return false; + } + + @Override + public float getFloatValue() { + throw new RuntimeException("Unknown Val is not a float constant"); + } + + @Override + public boolean isDoubleConstant() { + return false; + } + + @Override + public double getDoubleValue() { + throw new RuntimeException("Unknown Val is not a double constant"); + } + @Override public IArrayRef getArrayBase() { throw new RuntimeException("Unknown Val has no array base"); diff --git a/CryptoAnalysis/src/main/java/crypto/predicates/UnEnsuredPredicate.java b/CryptoAnalysis/src/main/java/crypto/predicates/UnEnsuredPredicate.java index 8d415f1a5..2e3f282d9 100644 --- a/CryptoAnalysis/src/main/java/crypto/predicates/UnEnsuredPredicate.java +++ b/CryptoAnalysis/src/main/java/crypto/predicates/UnEnsuredPredicate.java @@ -62,7 +62,13 @@ public enum Violations { * Violation if there is no dataflow path where the seed reaches an accepting state to * generate a predicate. */ - GeneratingStateIsNeverReached + GeneratingStateIsNeverReached, + + /** + * Violation if an accepting state is reached, but the predicate has an 'after' condition + * and the event is not called + */ + GeneratingEventIsNotCalled } public UnEnsuredPredicate( diff --git a/CryptoAnalysis/src/test/java/test/TestRules.java b/CryptoAnalysis/src/test/java/test/TestRules.java index 6714cf2ea..3ed254a39 100644 --- a/CryptoAnalysis/src/test/java/test/TestRules.java +++ b/CryptoAnalysis/src/test/java/test/TestRules.java @@ -63,6 +63,8 @@ public class TestRules { public static final String TRANSFORMATION = "transformation"; + public static final String FLOW_SENSITIVITY = "flowSensitivity"; + public static final String SEEDS = "seeds"; public static final String ISSUE_314 = "issue314"; diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java new file mode 100644 index 000000000..e5c7e0e97 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java @@ -0,0 +1,94 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity; + +import org.junit.jupiter.api.Disabled; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.extension.ExtendWith; +import test.Ruleset; +import test.TestRules; +import test.TestRunnerInterceptor; +import test.assertions.Assertions; + +@ExtendWith(TestRunnerInterceptor.class) +@Ruleset(TestRules.FLOW_SENSITIVITY) +public class PredicateAfterTest { + + private boolean staticallyUnknown() { + return Math.random() > 0.5; + } + + @Test + public void positivePredicateAfterBranchingTest() { + PredicateBranching branching = new PredicateBranching(); + branching.operation1(); + Assertions.hasEnsuredPredicate(branching, "generatedPredicateBranching"); + + branching.operation2(); + Assertions.hasEnsuredPredicate(branching, "generatedPredicateBranching"); + + Assertions.typestateErrors(branching, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void negativePredicateAfterBranchingTest() { + PredicateBranching branching = new PredicateBranching(); + if (staticallyUnknown()) { + // After this call, there is only one path with the corresponding event Op1 + branching.operation1(); + Assertions.hasEnsuredPredicate(branching, "generatedPredicateBranching"); + } + + // After this call, there is a sequence where Op1 is not called -> do not ensure predicate + branching.operation2(); + Assertions.notHasEnsuredPredicate(branching, "generatedPredicateBranching"); + + Assertions.typestateErrors(branching, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void positivePredicateAfterGeneratedTest() { + PredicateGenerator generator = new PredicateGenerator(); + PredicateReceiver receiver = generator.generate(); + + String secret = receiver.generateWord(); + Assertions.hasEnsuredPredicate(secret, "generatedWord"); + + Assertions.typestateErrors(generator, 0); + Assertions.typestateErrors(receiver, 0); + Assertions.incompleteOperationErrors(0); + } + + @Disabled("Requires rework of detection of seeds with multiple definition sites") + @Test + public void negativePredicateAfterGeneratedTest() { + PredicateGenerator generator = new PredicateGenerator(); + PredicateReceiver receiver = generator.generate(); + + String secret = null; + if (staticallyUnknown()) { + secret = receiver.generateWord(); + Assertions.hasEnsuredPredicate(secret, "generatedWord"); + } + + /* TODO + * This requires a new approach because we need to make sure that both + * 'secret' definitions (null and generateWord()) define the same seed. + * Note that this holds for seeds with and without rules + */ + Assertions.notHasEnsuredPredicate(secret, "generatedWord"); + + Assertions.typestateErrors(generator, 0); + Assertions.typestateErrors(receiver, 0); + Assertions.incompleteOperationErrors(0); + } +} diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java new file mode 100644 index 000000000..866d802e7 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java @@ -0,0 +1,19 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity; + +public class PredicateBranching { + + public PredicateBranching() {} + + public void operation1() {} + + public void operation2() {} +} diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java new file mode 100644 index 000000000..2fe53da84 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java @@ -0,0 +1,19 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity; + +public class PredicateGenerator { + + public PredicateGenerator() {} + + public PredicateReceiver generate() { + return () -> "secret"; + } +} diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java new file mode 100644 index 000000000..2c33d9b64 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java @@ -0,0 +1,15 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity; + +public interface PredicateReceiver { + + String generateWord(); +} diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl new file mode 100644 index 000000000..98095f5d6 --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl @@ -0,0 +1,12 @@ +SPEC tests.misc.flowsensitivity.PredicateBranching + +EVENTS + Con: PredicateBranching(); + Op1: operation1(); + Op2: operation2(); + +ORDER + Con, Op1?, Op2 + +ENSURES + generatedPredicateBranching[this] after Op1; diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl new file mode 100644 index 000000000..a2287a0ec --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl @@ -0,0 +1,11 @@ +SPEC tests.misc.flowsensitivity.PredicateGenerator + +OBJECTS + tests.misc.flowsensitivity.PredicateReceiver receiver; + +EVENTS + Con: PredicateGenerator(); + Gen: generate(); + +ORDER + Con, Gen diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl new file mode 100644 index 000000000..b3f00a223 --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl @@ -0,0 +1,13 @@ +SPEC tests.misc.flowsensitivity.PredicateReceiver + +OBJECTS + java.lang.String word; + +EVENTS + Gen: word = generateWord(); + +ORDER + Gen* + +ENSURES + generatedWord[word] after Gen; diff --git a/CryptoAnalysisScopes/src/main/java/de/fraunhofer/iem/cryptoanalysis/handler/OpalFrameworkHandler.java b/CryptoAnalysisScopes/src/main/java/de/fraunhofer/iem/cryptoanalysis/handler/OpalFrameworkHandler.java index cc189c64a..32f848704 100644 --- a/CryptoAnalysisScopes/src/main/java/de/fraunhofer/iem/cryptoanalysis/handler/OpalFrameworkHandler.java +++ b/CryptoAnalysisScopes/src/main/java/de/fraunhofer/iem/cryptoanalysis/handler/OpalFrameworkHandler.java @@ -11,6 +11,7 @@ import boomerang.scope.Method; import boomerang.scope.Val; +import boomerang.scope.opal.OpalScopeConverter; import boomerang.scope.opal.tac.OpalMethod; import boomerang.scope.opal.tac.OpalVal; import boomerang.scope.opal.transformation.TacLocal; @@ -28,7 +29,7 @@ public class OpalFrameworkHandler implements FrameworkHandler { @Override public Val createIntConstant(@NonNull int value, @NonNull Method method) { if (method instanceof OpalMethod opalMethod) { - return OpalVal.createUnsafe(new IntConst(PC, value), opalMethod); + return OpalScopeConverter.createOpalValUnsafe(new IntConst(PC, value), opalMethod); } throw new RuntimeException("Cannot create int constant without OpalMethod"); @@ -37,7 +38,7 @@ public Val createIntConstant(@NonNull int value, @NonNull Method method) { @Override public Val createLongConstant(@NonNull long value, @NonNull Method method) { if (method instanceof OpalMethod opalMethod) { - return OpalVal.createUnsafe(new LongConst(PC, value), opalMethod); + return OpalScopeConverter.createOpalValUnsafe(new LongConst(PC, value), opalMethod); } throw new RuntimeException("Cannot create long constant without OpalMethod"); @@ -46,7 +47,7 @@ public Val createLongConstant(@NonNull long value, @NonNull Method method) { @Override public Val createStringConstant(@NonNull String value, @NonNull Method method) { if (method instanceof OpalMethod opalMethod) { - return OpalVal.createUnsafe(new StringConst(PC, value), opalMethod); + return OpalScopeConverter.createOpalValUnsafe(new StringConst(PC, value), opalMethod); } throw new RuntimeException("Cannot create String constant without OpalMethod"); diff --git a/pom.xml b/pom.xml index 5fae7af4e..1ea7b5645 100644 --- a/pom.xml +++ b/pom.xml @@ -47,7 +47,7 @@ ${project.basedir} 17 - 4.3.2 + 4.3.3-SNAPSHOT 4.6.0 2.0.0 5.0.0 From 00b3b856bb0b7fde1b65ad6b0f5e05caae87bed2 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Tue, 9 Sep 2025 09:56:14 +0200 Subject: [PATCH 2/5] Evaluate constraints based on called statements --- .../AnalysisSeedWithSpecification.java | 72 ++++++++- .../src/test/java/test/TestRules.java | 4 +- .../src/test/java/test/TestRunner.java | 2 +- .../src/test/java/tests/jca/KeyPairTest.java | 12 ++ .../constraints/FlowSensitiveConstraint.java | 19 +++ .../FlowSensitiveConstraintsTest.java | 145 ++++++++++++++++++ .../constraints/OverriddenConstraint.java | 17 ++ .../{ => predicates}/PredicateAfterTest.java | 4 +- .../{ => predicates}/PredicateBranching.java | 2 +- .../{ => predicates}/PredicateGenerator.java | 2 +- .../{ => predicates}/PredicateReceiver.java | 2 +- .../flowSensitivity/PredicateGenerator.crysl | 11 -- .../constraints/FlowSensitiveConstraint.crysl | 18 +++ .../constraints/OverriddenConstraint.crysl | 17 ++ .../{ => predicates}/PredicateBranching.crysl | 2 +- .../predicates/PredicateGenerator.crysl | 11 ++ .../{ => predicates}/PredicateReceiver.crysl | 2 +- 17 files changed, 320 insertions(+), 22 deletions(-) create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraint.java create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraintsTest.java create mode 100644 CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/OverriddenConstraint.java rename CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/{ => predicates}/PredicateAfterTest.java (97%) rename CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/{ => predicates}/PredicateBranching.java (92%) rename CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/{ => predicates}/PredicateGenerator.java (92%) rename CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/{ => predicates}/PredicateReceiver.java (91%) delete mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl create mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/FlowSensitiveConstraint.crysl create mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/OverriddenConstraint.crysl rename CryptoAnalysis/src/test/resources/testrules/flowSensitivity/{ => predicates}/PredicateBranching.crysl (73%) create mode 100644 CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateGenerator.crysl rename CryptoAnalysis/src/test/resources/testrules/flowSensitivity/{ => predicates}/PredicateReceiver.crysl (69%) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index b68721aef..0b4e7a3a0 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -14,6 +14,7 @@ import boomerang.scope.InvokeExpr; import boomerang.scope.Statement; import boomerang.scope.Val; +import boomerang.utils.MethodWrapper; import com.google.common.collect.HashMultimap; import com.google.common.collect.Multimap; import com.google.common.collect.Table; @@ -42,6 +43,7 @@ import de.fraunhofer.iem.cryptoanalysis.scope.CryptoAnalysisScope; import java.util.Collection; import java.util.HashSet; +import java.util.List; import java.util.Map; import java.util.Objects; import java.util.Optional; @@ -399,7 +401,7 @@ private void propagatePredicate( } if (!satisfiesConstraintSystem) { - violations.add(UnEnsuredPredicate.Violations.ConstraintsAreNotSatisfied); + // violations.add(UnEnsuredPredicate.Violations.ConstraintsAreNotSatisfied); } // Check whether there is a predicate condition and whether it is satisfied @@ -408,6 +410,23 @@ private void propagatePredicate( } for (Statement statement : relevantStatements.keySet()) { + Collection allViolations = new HashSet<>(violations); + + /* Check whether there is a constraint violation on a statement up until the current statement. + * This includes the statements that have been called until the current statement. For example, + * we have a sequence Con -> A -> B -> C and the current statement is B, then we evaluate the + * constraints only on the statements Con, A, B because C has not been called yet + */ + Collection callsAtStatement = getCallsAtStatement(statement); + Collection consErrors = + constraintsAnalysis.evaluateConstraints(callsAtStatement); + Collection predErrors = + constraintsAnalysis.evaluateRequiredPredicates(callsAtStatement); + + if (!consErrors.isEmpty() || !predErrors.isEmpty()) { + allViolations.add(UnEnsuredPredicate.Violations.ConstraintsAreNotSatisfied); + } + /* Check for all states whether an accepting state is reached: * 1) All states are accepting -> Predicate is generated * 2) No state is accepting -> Predicate is definitely not generated @@ -421,7 +440,6 @@ private void propagatePredicate( boolean someStatesNonGenerating = states.stream().anyMatch(s -> !doesStateGeneratePredicate(s, predicate)); - Collection allViolations = new HashSet<>(violations); if (allStatesNonGenerating) { allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateIsNeverReached); } else if (someStatesNonGenerating) { @@ -451,6 +469,56 @@ private void propagatePredicate( } } + private Collection getCallsAtStatement(Statement statement) { + Collection weights = statementValWeightTable.row(statement).values(); + + Collection calls = new HashSet<>(); + for (TransitionFunction weight : weights) { + Collection sequences = weight.getStateChangeSequences().values(); + + for (StatementSequence sequence : sequences) { + Collection statements = sanitizeStatements(sequence); + + calls.addAll(statements); + } + } + + return calls; + } + + /** + * Method to sanitize duplicate statements from a call sequence. This method returns a set with + * the statements sanitizes from the end of the sequence. For example, if we have a sequence Con + * -> A -> B -> A, then the method returns a set with Con, B, A where A is the second one in the + * sequence. This way, we can ensure that the call to A is the last 'state' of the call sequence + * and possible violations at the first A are overridden. + * + * @param sequence the sequence to sanitize + * @return the sanitized statements + */ + private Collection sanitizeStatements(StatementSequence sequence) { + Collection sanitizedStatements = new HashSet<>(); + Collection addedMethods = new HashSet<>(); + + List entries = sequence.getSequence(); + for (int i = entries.size() - 1; i >= 0; i--) { + Statement statement = entries.get(i).getStatement(); + + if (!statement.containsInvokeExpr()) { + continue; + } + + MethodWrapper declaredMethod = + statement.getInvokeExpr().getDeclaredMethod().toMethodWrapper(); + if (!addedMethods.contains(declaredMethod)) { + addedMethods.add(declaredMethod); + sanitizedStatements.add(statement); + } + } + + return sanitizedStatements; + } + private boolean isGeneratingEventMissing(Statement statement, Collection events) { Collection weights = statementValWeightTable.row(statement).values(); diff --git a/CryptoAnalysis/src/test/java/test/TestRules.java b/CryptoAnalysis/src/test/java/test/TestRules.java index 3ed254a39..1cffa8498 100644 --- a/CryptoAnalysis/src/test/java/test/TestRules.java +++ b/CryptoAnalysis/src/test/java/test/TestRules.java @@ -63,7 +63,9 @@ public class TestRules { public static final String TRANSFORMATION = "transformation"; - public static final String FLOW_SENSITIVITY = "flowSensitivity"; + public static final String FLOW_SENSITIVITY_CONSTRAINTS = "flowSensitivity/constraints"; + + public static final String FLOW_SENSITIVITY_PREDICATES = "flowSensitivity/predicates"; public static final String SEEDS = "seeds"; diff --git a/CryptoAnalysis/src/test/java/test/TestRunner.java b/CryptoAnalysis/src/test/java/test/TestRunner.java index 18e71aac9..873a931e8 100644 --- a/CryptoAnalysis/src/test/java/test/TestRunner.java +++ b/CryptoAnalysis/src/test/java/test/TestRunner.java @@ -66,7 +66,7 @@ public class TestRunner { private static final String OPAL = "opal"; /** Use this variable to configure the framework when running the tests locally */ - private static final String LOCAL_TEST_FRAMEWORK = SOOT; + private static final String LOCAL_TEST_FRAMEWORK = SOOT_UP; private final TestSetup testSetup; private final CryptoScanner scanner; diff --git a/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java b/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java index 67be4d94a..2f2301dfd 100644 --- a/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java +++ b/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java @@ -71,6 +71,18 @@ public void positiveRsaParameterSpecTestBigInteger() throws GeneralSecurityExcep Assertions.hasEnsuredPredicate(keyPair); } + @Test + public void test() throws GeneralSecurityException { + int keySize = 4096; + KeyPairGenerator generator = KeyPairGenerator.getInstance("RSA"); + RSAKeyGenParameterSpec parameters = + new RSAKeyGenParameterSpec(keySize, BigInteger.valueOf(65537)); + Assertions.hasEnsuredPredicate(parameters); + generator.initialize(parameters); + KeyPair keyPair = generator.generateKeyPair(); + Assertions.hasEnsuredPredicate(keyPair); + } + @Test public void negativeRsaParameterSpecTestBigInteger() throws GeneralSecurityException { // Since 3.0.0: key size of 2048 is not allowed diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraint.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraint.java new file mode 100644 index 000000000..a2ab840b3 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraint.java @@ -0,0 +1,19 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity.constraints; + +public class FlowSensitiveConstraint { + + public FlowSensitiveConstraint() {} + + public void operation1() {} + + public void operation2(@SuppressWarnings("unused") int i) {} +} diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraintsTest.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraintsTest.java new file mode 100644 index 000000000..e2da1e0e8 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraintsTest.java @@ -0,0 +1,145 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity.constraints; + +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.extension.ExtendWith; +import test.Ruleset; +import test.TestRules; +import test.TestRunnerInterceptor; +import test.assertions.Assertions; + +@ExtendWith(TestRunnerInterceptor.class) +@Ruleset(TestRules.FLOW_SENSITIVITY_CONSTRAINTS) +public class FlowSensitiveConstraintsTest { + + private boolean staticallyUnknown() { + return Math.random() > 0.5; + } + + @Test + public void positiveSimpleConstraintsTest() { + FlowSensitiveConstraint constraint = new FlowSensitiveConstraint(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + constraint.operation1(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + constraint.operation2(10); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + Assertions.constraintErrors(constraint, 0); + Assertions.typestateErrors(constraint, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void negativeSimpleConstraintsTest() { + FlowSensitiveConstraint constraint = new FlowSensitiveConstraint(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + constraint.operation1(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + // At this point, we violate the constraint; hence, the object is not secure AFTER this + // statement + constraint.operation2(100); + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + + Assertions.constraintErrors(constraint, 1); + Assertions.typestateErrors(constraint, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void satisfiedToViolatedConstraint() { + OverriddenConstraint constraint = new OverriddenConstraint(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + // satisfied + constraint.operation(10); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + // violated + constraint.operation(100); + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + + Assertions.constraintErrors(constraint, 1); + Assertions.typestateErrors(constraint, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void violatedToSatisfiedConstraint() { + OverriddenConstraint constraint = new OverriddenConstraint(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + // violated + constraint.operation(100); + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + + // satisfied + constraint.operation(10); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + Assertions.constraintErrors(constraint, 1); + Assertions.typestateErrors(constraint, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void satisfiedToViolatedBranchedConstraint() { + OverriddenConstraint constraint = new OverriddenConstraint(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + if (staticallyUnknown()) { + // satisfied + constraint.operation(10); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + } + + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + if (staticallyUnknown()) { + // violated + constraint.operation(100); + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + } + + // Violated because there is a sequence to the violating call + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + + Assertions.constraintErrors(constraint, 1); + Assertions.typestateErrors(constraint, 0); + Assertions.incompleteOperationErrors(0); + } + + @Test + public void violatedToSatisfiedBranchedConstraint() { + OverriddenConstraint constraint = new OverriddenConstraint(); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + if (staticallyUnknown()) { + // violated + constraint.operation(100); + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + } + + Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint"); + + // satisfied + constraint.operation(10); + Assertions.hasEnsuredPredicate(constraint, "generatedConstraint"); + + Assertions.constraintErrors(constraint, 1); + Assertions.typestateErrors(constraint, 0); + Assertions.incompleteOperationErrors(0); + } +} diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/OverriddenConstraint.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/OverriddenConstraint.java new file mode 100644 index 000000000..9a645ba17 --- /dev/null +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/OverriddenConstraint.java @@ -0,0 +1,17 @@ +/******************************************************************************** + * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany + *

+ * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License 2.0 which is available at + * http://www.eclipse.org/legal/epl-2.0. + *

+ * SPDX-License-Identifier: EPL-2.0 + ********************************************************************************/ +package tests.misc.flowsensitivity.constraints; + +public class OverriddenConstraint { + + public OverriddenConstraint() {} + + public void operation(@SuppressWarnings("unused") int i) {} +} diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateAfterTest.java similarity index 97% rename from CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java rename to CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateAfterTest.java index e5c7e0e97..74f843995 100644 --- a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateAfterTest.java +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateAfterTest.java @@ -7,7 +7,7 @@ *

* SPDX-License-Identifier: EPL-2.0 ********************************************************************************/ -package tests.misc.flowsensitivity; +package tests.misc.flowsensitivity.predicates; import org.junit.jupiter.api.Disabled; import org.junit.jupiter.api.Test; @@ -18,7 +18,7 @@ import test.assertions.Assertions; @ExtendWith(TestRunnerInterceptor.class) -@Ruleset(TestRules.FLOW_SENSITIVITY) +@Ruleset(TestRules.FLOW_SENSITIVITY_PREDICATES) public class PredicateAfterTest { private boolean staticallyUnknown() { diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateBranching.java similarity index 92% rename from CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java rename to CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateBranching.java index 866d802e7..16782ffc8 100644 --- a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateBranching.java +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateBranching.java @@ -7,7 +7,7 @@ *

* SPDX-License-Identifier: EPL-2.0 ********************************************************************************/ -package tests.misc.flowsensitivity; +package tests.misc.flowsensitivity.predicates; public class PredicateBranching { diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateGenerator.java similarity index 92% rename from CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java rename to CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateGenerator.java index 2fe53da84..b9cca6de4 100644 --- a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateGenerator.java +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateGenerator.java @@ -7,7 +7,7 @@ *

* SPDX-License-Identifier: EPL-2.0 ********************************************************************************/ -package tests.misc.flowsensitivity; +package tests.misc.flowsensitivity.predicates; public class PredicateGenerator { diff --git a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateReceiver.java similarity index 91% rename from CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java rename to CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateReceiver.java index 2c33d9b64..059b1ea9f 100644 --- a/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/PredicateReceiver.java +++ b/CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateReceiver.java @@ -7,7 +7,7 @@ *

* SPDX-License-Identifier: EPL-2.0 ********************************************************************************/ -package tests.misc.flowsensitivity; +package tests.misc.flowsensitivity.predicates; public interface PredicateReceiver { diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl deleted file mode 100644 index a2287a0ec..000000000 --- a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateGenerator.crysl +++ /dev/null @@ -1,11 +0,0 @@ -SPEC tests.misc.flowsensitivity.PredicateGenerator - -OBJECTS - tests.misc.flowsensitivity.PredicateReceiver receiver; - -EVENTS - Con: PredicateGenerator(); - Gen: generate(); - -ORDER - Con, Gen diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/FlowSensitiveConstraint.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/FlowSensitiveConstraint.crysl new file mode 100644 index 000000000..d251d84cf --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/FlowSensitiveConstraint.crysl @@ -0,0 +1,18 @@ +SPEC tests.misc.flowsensitivity.constraints.FlowSensitiveConstraint + +OBJECTS + int i; + +EVENTS + Con: FlowSensitiveConstraint(); + Op1: operation1(); + Op2: operation2(i); + +ORDER + Con, Op1, Op2 + +CONSTRAINTS + i == 10; + +ENSURES + generatedConstraint[this] after Con; diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/OverriddenConstraint.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/OverriddenConstraint.crysl new file mode 100644 index 000000000..baf544a21 --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/constraints/OverriddenConstraint.crysl @@ -0,0 +1,17 @@ +SPEC tests.misc.flowsensitivity.constraints.OverriddenConstraint + +OBJECTS + int i; + +EVENTS + Con: OverriddenConstraint(); + Op: operation(i); + +ORDER + Con, Op* + +CONSTRAINTS + i == 10; + +ENSURES + generatedConstraint[this] after Con; diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateBranching.crysl similarity index 73% rename from CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl rename to CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateBranching.crysl index 98095f5d6..f9827566a 100644 --- a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateBranching.crysl +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateBranching.crysl @@ -1,4 +1,4 @@ -SPEC tests.misc.flowsensitivity.PredicateBranching +SPEC tests.misc.flowsensitivity.predicates.PredicateBranching EVENTS Con: PredicateBranching(); diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateGenerator.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateGenerator.crysl new file mode 100644 index 000000000..a407f6660 --- /dev/null +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateGenerator.crysl @@ -0,0 +1,11 @@ +SPEC tests.misc.flowsensitivity.predicates.PredicateGenerator + +OBJECTS + tests.misc.flowsensitivity.predicates.PredicateReceiver receiver; + +EVENTS + Con: PredicateGenerator(); + Gen: generate(); + +ORDER + Con, Gen diff --git a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateReceiver.crysl similarity index 69% rename from CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl rename to CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateReceiver.crysl index b3f00a223..a22f6476e 100644 --- a/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/PredicateReceiver.crysl +++ b/CryptoAnalysis/src/test/resources/testrules/flowSensitivity/predicates/PredicateReceiver.crysl @@ -1,4 +1,4 @@ -SPEC tests.misc.flowsensitivity.PredicateReceiver +SPEC tests.misc.flowsensitivity.predicates.PredicateReceiver OBJECTS java.lang.String word; From a2b6b362dd18c9fa345fd816973d6a755dc7c9f9 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Tue, 9 Sep 2025 13:34:39 +0200 Subject: [PATCH 3/5] Split predicate evaluation and propagation --- .../AnalysisSeedWithSpecification.java | 97 +++++++++++-------- .../implication/PredicateImplicationTest.java | 2 +- .../java/tests/jca/CogniCryptTestGenTest.java | 2 - .../src/test/java/tests/jca/KeyPairTest.java | 12 --- 4 files changed, 57 insertions(+), 56 deletions(-) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index 0b4e7a3a0..567847dd7 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -41,7 +41,9 @@ import crysl.rule.StateNode; import crysl.rule.TransitionEdge; import de.fraunhofer.iem.cryptoanalysis.scope.CryptoAnalysisScope; +import java.util.ArrayList; import java.util.Collection; +import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; @@ -58,12 +60,16 @@ public class AnalysisSeedWithSpecification extends IAnalysisSeed { private final CrySLRule specification; private final ConstraintsAnalysis constraintsAnalysis; - private boolean internalConstraintsSatisfied; private final Collection allCallsOnObject; private final Multimap relevantStatements = HashMultimap.create(); private final Collection indirectlyEnsuredPredicates = new HashSet<>(); + private record PredicateToPropagate( + CrySLPredicate predicate, + Statement statement, + Collection violations) {} + public AnalysisSeedWithSpecification( CryptoScanner scanner, Statement statement, @@ -372,27 +378,57 @@ private CrySLPredicate formatCrySLPredicate(CrySLPredicate predicate) { @Override public void propagatePredicates() { - // Check whether all constraints from the CONSTRAINTS and REQUIRES section is satisfied - boolean satisfiesConstraintSystem = isConstraintSystemSatisfied(); + Collection predsToPropagate = new ArrayList<>(); + Collection indirectPredsToPropagate = new ArrayList<>(); Collection predsToBeEnsured = specification.getPredicates(); for (CrySLPredicate predToBeEnsured : predsToBeEnsured) { - propagatePredicate(predToBeEnsured, satisfiesConstraintSystem); + Map> predResults = + propagatePredicate(predToBeEnsured); + + for (Statement statement : predResults.keySet()) { + Collection violations = predResults.get(statement); + + predsToPropagate.add( + new PredicateToPropagate( + predToBeEnsured.toNormalCrySLPredicate(), statement, violations)); + } } for (AbstractPredicate indirectPred : indirectlyEnsuredPredicates) { - propagatePredicate(indirectPred.getPredicate(), satisfiesConstraintSystem, true); + CrySLPredicate predicate = indirectPred.getPredicate(); + Map> predResults = + propagatePredicate(predicate); + + for (Statement statement : predResults.keySet()) { + Collection violations = predResults.get(statement); + + indirectPredsToPropagate.add( + new PredicateToPropagate( + predicate.toNormalCrySLPredicate(), statement, violations)); + } } + + // Propagate predicates + propagatePredicates(predsToPropagate, false); + propagatePredicates(indirectPredsToPropagate, true); } - private void propagatePredicate(CrySLPredicate predicate, boolean satisfiesConstraintSystem) { - propagatePredicate(predicate, satisfiesConstraintSystem, false); + private void propagatePredicates( + Collection predsToPropagate, boolean isIndirectlyEnsured) { + for (PredicateToPropagate predicate : predsToPropagate) { + if (isIndirectlyEnsured) { + propagateIndirectlyEnsuredPredicate( + predicate.predicate(), predicate.statement(), predicate.violations()); + } else { + propagateEnsuredPredicate( + predicate.predicate(), predicate.statement(), predicate.violations()); + } + } } - private void propagatePredicate( - CrySLPredicate predicate, - boolean satisfiesConstraintSystem, - boolean isIndirectlyEnsured) { + private Map> propagatePredicate( + CrySLPredicate predicate) { Collection violations = new HashSet<>(); // Check whether there is a ForbiddenMethodError from previous checks @@ -400,15 +436,7 @@ private void propagatePredicate( violations.add(UnEnsuredPredicate.Violations.CallToForbiddenMethod); } - if (!satisfiesConstraintSystem) { - // violations.add(UnEnsuredPredicate.Violations.ConstraintsAreNotSatisfied); - } - - // Check whether there is a predicate condition and whether it is satisfied - if (constraintsAnalysis.isPredConditionViolated(predicate)) { - violations.add(UnEnsuredPredicate.Violations.ConditionIsNotSatisfied); - } - + Map> result = new HashMap<>(); for (Statement statement : relevantStatements.keySet()) { Collection allViolations = new HashSet<>(violations); @@ -427,6 +455,11 @@ private void propagatePredicate( allViolations.add(UnEnsuredPredicate.Violations.ConstraintsAreNotSatisfied); } + // Check whether there is a predicate condition and whether it is satisfied + if (constraintsAnalysis.isPredConditionViolated(predicate, callsAtStatement)) { + violations.add(UnEnsuredPredicate.Violations.ConditionIsNotSatisfied); + } + /* Check for all states whether an accepting state is reached: * 1) All states are accepting -> Predicate is generated * 2) No state is accepting -> Predicate is definitely not generated @@ -459,14 +492,10 @@ private void propagatePredicate( } } - if (isIndirectlyEnsured) { - propagateIndirectlyEnsuredPredicate( - predicate.toNormalCrySLPredicate(), statement, allViolations); - } else { - propagateEnsuredPredicate( - predicate.toNormalCrySLPredicate(), statement, allViolations); - } + result.put(statement, allViolations); } + + return result; } private Collection getCallsAtStatement(Statement statement) { @@ -857,7 +886,6 @@ private void checkInternalConstraints() { constraintsAnalysis.initialize(); Collection violatedConstraints = constraintsAnalysis.evaluateConstraints(); - this.internalConstraintsSatisfied = violatedConstraints.isEmpty(); for (AbstractConstraintsError error : violatedConstraints) { this.addError(error); @@ -867,19 +895,6 @@ private void checkInternalConstraints() { scanner.getAnalysisReporter().afterConstraintsCheck(this, violatedConstraints.size()); } - /** - * Check, whether the internal constraints and predicate constraints are satisfied. Requires a - * previous call to {@link #checkInternalConstraints()} - * - * @return true if all internal and required predicate constraints are satisfied - */ - private boolean isConstraintSystemSatisfied() { - Collection violatedPredicates = - constraintsAnalysis.evaluateRequiredPredicates(); - - return internalConstraintsSatisfied && violatedPredicates.isEmpty(); - } - /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * Additional methods * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ diff --git a/CryptoAnalysis/src/test/java/tests/error/predicate/implication/PredicateImplicationTest.java b/CryptoAnalysis/src/test/java/tests/error/predicate/implication/PredicateImplicationTest.java index 8f4fdd5b1..fc94c526e 100644 --- a/CryptoAnalysis/src/test/java/tests/error/predicate/implication/PredicateImplicationTest.java +++ b/CryptoAnalysis/src/test/java/tests/error/predicate/implication/PredicateImplicationTest.java @@ -75,7 +75,7 @@ public void testImplicationUnsatisfiedOnReturn() { // i == 10 => generatedReceiver Receiver receiver = generator.generateReceiver(); - Assertions.notHasEnsuredPredicate(receiver); + Assertions.hasEnsuredPredicate(receiver); // Condition satisfied (true) => predicate has to be ensured (false) receiver.condition(10); diff --git a/CryptoAnalysis/src/test/java/tests/jca/CogniCryptTestGenTest.java b/CryptoAnalysis/src/test/java/tests/jca/CogniCryptTestGenTest.java index d684f873c..69551fa2b 100644 --- a/CryptoAnalysis/src/test/java/tests/jca/CogniCryptTestGenTest.java +++ b/CryptoAnalysis/src/test/java/tests/jca/CogniCryptTestGenTest.java @@ -461,12 +461,10 @@ public void messageDigestInvalidTest11() throws NoSuchAlgorithmException { public void messageDigestInvalidTest12() throws NoSuchAlgorithmException, DigestException { // Related to issue 296: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/296 int off = 0; - byte[] inByteArr = null; int len = 0; byte[] out = null; MessageDigest messageDigest0 = MessageDigest.getInstance("SHA-256"); - out = messageDigest0.digest(inByteArr); // update is skipped messageDigest0.digest(out, off, len); Assertions.notHasEnsuredPredicate(out); diff --git a/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java b/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java index 2f2301dfd..67be4d94a 100644 --- a/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java +++ b/CryptoAnalysis/src/test/java/tests/jca/KeyPairTest.java @@ -71,18 +71,6 @@ public void positiveRsaParameterSpecTestBigInteger() throws GeneralSecurityExcep Assertions.hasEnsuredPredicate(keyPair); } - @Test - public void test() throws GeneralSecurityException { - int keySize = 4096; - KeyPairGenerator generator = KeyPairGenerator.getInstance("RSA"); - RSAKeyGenParameterSpec parameters = - new RSAKeyGenParameterSpec(keySize, BigInteger.valueOf(65537)); - Assertions.hasEnsuredPredicate(parameters); - generator.initialize(parameters); - KeyPair keyPair = generator.generateKeyPair(); - Assertions.hasEnsuredPredicate(keyPair); - } - @Test public void negativeRsaParameterSpecTestBigInteger() throws GeneralSecurityException { // Since 3.0.0: key size of 2048 is not allowed From 8dad5a3a89c656d0f93a99e4ee9fc175633992e1 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Tue, 9 Sep 2025 15:29:01 +0200 Subject: [PATCH 4/5] Fix remaining test cases --- .../src/test/java/scanner/setup/AbstractHeadlessTest.java | 2 +- .../test/java/scanner/targets/BragaCryptoGoodUsesTest.java | 5 +---- .../test/java/scanner/targets/BragaCryptoMisusesTest.java | 6 +++--- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java b/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java index d7c36a342..00343a001 100644 --- a/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java +++ b/HeadlessJavaScanner/src/test/java/scanner/setup/AbstractHeadlessTest.java @@ -34,7 +34,7 @@ public abstract class AbstractHeadlessTest { private static final String OPAL = "opal"; /** Use this variable to configure the framework when running the tests locally */ - private static final String LOCAL_TEST_FRAMEWORK = OPAL; + private static final String LOCAL_TEST_FRAMEWORK = SOOT_UP; protected static final String RULES_BASE_DIR = "." diff --git a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java index a599f431a..51efdb863 100644 --- a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java +++ b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoGoodUsesTest.java @@ -920,10 +920,7 @@ public void digSignDSAandECDSAExamples() { addErrorSpecification( new ErrorSpecification.Builder("example.RandomMessageNonceECDSA", "main", 1) - .withFPs( - RequiredPredicateError.class, - 2, - "setSeed is correctly called (cf. https://github.com/CROSSINGTUD/CryptoAnalysis/issues/295") + .withNoErrors(RequiredPredicateError.class) .build()); // positive test case diff --git a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java index 5baac53cc..097d5412d 100644 --- a/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java +++ b/HeadlessJavaScanner/src/test/java/scanner/targets/BragaCryptoMisusesTest.java @@ -1254,7 +1254,7 @@ public void predictableSeedExamples() { addErrorSpecification( new ErrorSpecification.Builder("br.predictableSeed.ReusedSeed", "main", 1) - .withTPs(RequiredPredicateError.class, 4) + .withNoErrors(RequiredPredicateError.class) .build()); addErrorSpecification( new ErrorSpecification.Builder("br.predictableSeed.LowEntropySeed1", "main", 1) @@ -1832,7 +1832,7 @@ public void weakSignatureECDSAExamples() { "pkc.sign.weakSignatureECDSA.RepeatedMessageNonceECDSA_1", "main", 1) - .withTPs(RequiredPredicateError.class, 2) + .withNoErrors(RequiredPredicateError.class) .build()); addErrorSpecification( new ErrorSpecification.Builder( @@ -1853,7 +1853,7 @@ public void weakSignatureECDSAExamples() { "pkc.sign.weakSignatureECDSA.RepeatedMessageNonceECDSA_4", "main", 1) - .withTPs(RequiredPredicateError.class, 2) + .withNoErrors(RequiredPredicateError.class) .build()); addErrorSpecification( new ErrorSpecification.Builder( From 0c6240513132a9bb30aec238623d391e6a4fa43b Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Wed, 1 Oct 2025 11:44:09 +0200 Subject: [PATCH 5/5] Update CrySL version --- pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pom.xml b/pom.xml index 1ea7b5645..d8f375044 100644 --- a/pom.xml +++ b/pom.xml @@ -51,7 +51,7 @@ 4.6.0 2.0.0 5.0.0 - 4.0.5 + 4.0.6 5.13.4 33.4.8-jre