diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index e10508d1a..a10accbd7 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -122,15 +122,8 @@ public void execute() { runExtractParameterAnalysis(); checkInternalConstraints(); - Multimap unitToStates = HashMultimap.create(); - for (Cell c : results.asStatementValWeightTable().cellSet()) { - unitToStates.putAll(c.getRowKey(), getTargetStates(c.getValue())); - for (EnsuredCrySLPredicate pred : indirectlyEnsuredPredicates) { - // TODO only maintain indirectly ensured predicate as long as they are not - // killed by the rule - predicateHandler.addNewPred(this, c.getRowKey(), c.getColumnKey(), pred); - } - } + // Analysis seed was not analyzed yet -> Activate predicates from other rules + activateIndirectlyEnsuredPredicates(); computeTypestateErrorUnits(); computeTypestateErrorsForEndOfObjectLifeTime(); @@ -169,6 +162,20 @@ private void runExtractParameterAnalysis() { this.parameterAnalysis = new ExtractParameterAnalysis(this.cryptoScanner, allCallsOnObject, spec.getFSM()); this.parameterAnalysis.run(); } + + private void activateIndirectlyEnsuredPredicates() { + for (Cell c : results.asStatementValWeightTable().cellSet()) { + Collection states = getTargetStates(c.getValue()); + + for (State state : states) { + for (EnsuredCrySLPredicate pred : indirectlyEnsuredPredicates) { + if (!isPredicateNegatingState(pred.getPredicate(), state, spec.getRule().getNegatedPredicates())) { + predicateHandler.addNewPred(this, c.getRowKey(), c.getColumnKey(), pred); + } + } + } + } + } private void computeTypestateErrorUnits() { Set allTypestateChangeStatements = Sets.newHashSet(); @@ -233,7 +240,7 @@ private void onAddedTypestateChange(Statement curr, State stateNode) { continue; } - if (isPredicateGeneratingState(predToBeEnsured, stateNode)) { + if (isPredicateGeneratingState(predToBeEnsured, stateNode) && !isPredicateNegatingState(predToBeEnsured, stateNode, spec.getRule().getNegatedPredicates())) { ensuresPred(predToBeEnsured, curr, stateNode); } } @@ -324,13 +331,12 @@ private void expectPredicateOnOtherObject(CrySLPredicate predToBeEnsured, Statem private void addEnsuredPredicateFromOtherRule(EnsuredCrySLPredicate ensuredCrySLPredicate) { indirectlyEnsuredPredicates.add(ensuredCrySLPredicate); - if (results == null) + if (results == null) { return; - for (Cell c : results.asStatementValWeightTable().cellSet()) { - for (EnsuredCrySLPredicate pred : indirectlyEnsuredPredicates) { - predicateHandler.addNewPred(this, c.getRowKey(), c.getColumnKey(), pred); - } } + + // Analysis seed was previously analyzed -> Activate predicate from other rule + activateIndirectlyEnsuredPredicates(); } private void expectPredicateWhenThisObjectIsInState(State stateNode, Statement currStmt, CrySLPredicate predToBeEnsured, boolean satisfiesConstraintSytem) { @@ -339,8 +345,6 @@ private void expectPredicateWhenThisObjectIsInState(State stateNode, Statement c if (!satisfiesConstraintSytem) return; for (Cell e : results.asStatementValWeightTable().cellSet()) { - // TODO check for any reachable state that don't kill - // predicates. if (containsTargetState(e.getValue(), stateNode)) { predicateHandler.addNewPred(this, e.getRowKey(), e.getColumnKey(), new EnsuredCrySLPredicate(predToBeEnsured, parameterAnalysis.getCollectedValues())); } @@ -578,7 +582,17 @@ public void addEnsuredPredicate(EnsuredCrySLPredicate ensPred) { } private boolean isPredicateGeneratingState(CrySLPredicate ensPred, State stateNode) { - return ensPred instanceof CrySLCondPredicate && isConditionalState(((CrySLCondPredicate) ensPred).getConditionalMethods(), stateNode) || (!(ensPred instanceof CrySLCondPredicate) && stateNode.isAccepting()); + // Predicate has a condition, i.e. "after" is specified -> Active predicate for corresponding states + if (ensPred instanceof CrySLCondPredicate && isConditionalState(((CrySLCondPredicate) ensPred).getConditionalMethods(), stateNode)) { + return true; + } + + // If there is no condition, the predicate is activated for all accepting states + if (!(ensPred instanceof CrySLCondPredicate) && stateNode.isAccepting()) { + return true; + } + + return false; } private boolean isConditionalState(Set conditionalMethods, State state) { @@ -591,6 +605,60 @@ private boolean isConditionalState(Set conditionalMethods, State stat } return false; } + + private boolean isPredicateNegatingState(CrySLPredicate ensPred, State stateNode, List negatedPredicates) { + // Check, whether the predicate is negated in the given state + for (CrySLPredicate negPred : negatedPredicates) { + // Compare names + if (!ensPred.getPredName().equals(negPred.getPredName())) { + continue; + } + + // Compare parameters + if (!doParametersMatch(ensPred, negPred)) { + continue; + } + + // Negated predicate does not have a condition, i.e. no "after" -> predicate is negated in all states + if (!(negPred instanceof CrySLCondPredicate)) { + return true; + } + + CrySLCondPredicate condNegPred = (CrySLCondPredicate) negPred; + + for (StateNode s : condNegPred.getConditionalMethods()) { + if (new WrappedState(s).equals(stateNode)) { + return true; + } + } + } + + return false; + } + + private boolean doParametersMatch(CrySLPredicate ensPred, CrySLPredicate negPred) { + // Compare number of parameters + if (!(ensPred.getParameters().size() == negPred.getParameters().size())) { + return false; + } + + // Compare type of parameters pairwise + for (int i = 0; i < ensPred.getParameters().size(); i++) { + CrySLObject ensParameter = (CrySLObject) ensPred.getParameters().get(i); + CrySLObject negParameter = (CrySLObject) negPred.getParameters().get(i); + + // If "_" is used as a parameter, the type is arbitrary + if (ensParameter.getJavaType().equals("null") || negParameter.getJavaType().equals("null")) { + continue; + } + + if (!ensParameter.getJavaType().equals(negParameter.getJavaType())) { + return false; + } + } + + return true; + } public Set getMissingPredicates() { return missingPredicates; diff --git a/CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java b/CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java index efc0517d0..a836852ed 100644 --- a/CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java +++ b/CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java @@ -18,6 +18,7 @@ import com.google.common.base.CharMatcher; import com.google.common.collect.Lists; +import com.google.common.collect.Sets; import com.google.inject.Injector; import org.apache.commons.lang3.NotImplementedException; @@ -261,11 +262,13 @@ private CrySLRule createRuleFromDomainmodel(Domainmodel model) throws CryptoAnal final EnsuresBlock ensuresBlock = model.getEnsures(); final NegatesBlock negatesBlock = model.getNegates(); + final List predicates = Lists.newArrayList(); + final List negatedPredicates = Lists.newArrayList(); predicates.addAll(getEnsuredPredicates(ensuresBlock)); - predicates.addAll(getNegatedPredicates(negatesBlock)); + negatedPredicates.addAll(getNegatedPredicates(negatesBlock)); - return new CrySLRule(currentClass, objects, forbiddenMethods, this.smg, constraints, predicates); + return new CrySLRule(currentClass, objects, forbiddenMethods, this.smg, constraints, predicates, negatedPredicates); } private List changeDeclaringClass(JvmTypeReference currentClass, EventsBlock eventsBlock) { @@ -562,11 +565,28 @@ private Set getStatesForMethods(final List condition) { for (final TransitionEdge transition : this.smg.getAllTransitions()) { if(transition.getLabel().containsAll(condition)) { - predicateGenerationNodes.add(transition.getRight()); + Set reachableNodes = getAllReachableNodes(transition.getRight(), Sets.newHashSet()); + + predicateGenerationNodes.addAll(reachableNodes); } } return predicateGenerationNodes; } + + private Set getAllReachableNodes(final StateNode startNode, Set visited) { + if (visited.contains(startNode)) { + return visited; + } + + visited.add(startNode); + + for (TransitionEdge edge : this.smg.getAllOutgoingEdges(startNode)) { + Set reachableNodes = getAllReachableNodes(edge.getRight(), visited); + + visited.addAll(reachableNodes); + } + return visited; + } private ISLConstraint getBuiltinPredicate(BuiltinPredicate builtinPredicate) { String name = builtinPredicate.getPredicate().getLiteral(); diff --git a/CryptoAnalysis/src/main/java/crypto/rules/CrySLRule.java b/CryptoAnalysis/src/main/java/crypto/rules/CrySLRule.java index 5c1ba792c..10315162f 100644 --- a/CryptoAnalysis/src/main/java/crypto/rules/CrySLRule.java +++ b/CryptoAnalysis/src/main/java/crypto/rules/CrySLRule.java @@ -13,9 +13,6 @@ public class CrySLRule implements java.io.Serializable { - /** - * - */ private static final long serialVersionUID = 1L; private final String className; @@ -30,13 +27,16 @@ public class CrySLRule implements java.io.Serializable { protected final List predicates; - public CrySLRule(String className, List> objects, List forbiddenMethods, StateMachineGraph usagePattern, List constraints, List predicates) { + protected final List negatedPredicates; + + public CrySLRule(String className, List> objects, List forbiddenMethods, StateMachineGraph usagePattern, List constraints, List predicates, List negatedPredicates) { this.className = className; this.objects = objects; this.forbiddenMethods =forbiddenMethods; this.usagePattern = usagePattern; this.constraints = constraints; this.predicates = predicates; + this.negatedPredicates = negatedPredicates; } @@ -106,6 +106,14 @@ public List getConstraints() { public List getPredicates() { return predicates; } + + /** + * @return the negated predicates + */ + public List getNegatedPredicates() { + return negatedPredicates; + } + /** * @return the constraints */ @@ -148,6 +156,14 @@ public String toString() { } } + if (this.negatedPredicates != null) { + outputSB.append("\nNegated predicates:"); + for (CrySLPredicate predicate : this.negatedPredicates) { + outputSB.append(predicate); + outputSB.append(","); + } + } + return outputSB.toString(); } diff --git a/CryptoAnalysis/src/test/java/tests/pattern/CipherTest.java b/CryptoAnalysis/src/test/java/tests/pattern/CipherTest.java index a50856ed8..c1c14a1fc 100644 --- a/CryptoAnalysis/src/test/java/tests/pattern/CipherTest.java +++ b/CryptoAnalysis/src/test/java/tests/pattern/CipherTest.java @@ -226,6 +226,7 @@ public void cipherUsagePatternTest1SilentForbiddenMethod() throws GeneralSecurit byte[] encText = cCipher.doFinal("".getBytes()); Assertions.mustBeInAcceptingState(cCipher); Assertions.notHasEnsuredPredicate(cCipher); + Assertions.notHasEnsuredPredicate(encText); cCipher.getIV(); } @@ -338,10 +339,9 @@ public void cipherUsagePatternTestWrongOffsetSize() throws GeneralSecurityExcept Assertions.extValue(0); Assertions.extValue(1); Assertions.extValue(2); - // TODO: Fails for reasons different from the ones I expected. cCipher.getIV(); - // Assertions.mustBeInAcceptingState(cCipher); - // Assertions.notasEnsuredPredicate(encText); + Assertions.mustBeInAcceptingState(cCipher); + Assertions.hasEnsuredPredicate(encText); } @Test @@ -408,6 +408,7 @@ public void cipherUsagePatternTest3() throws GeneralSecurityException { Assertions.extValue(0); SecretKey key = keygen.generateKey(); Assertions.mustBeInAcceptingState(keygen); + Assertions.hasEnsuredPredicate(key); Cipher cCipher = Cipher.getInstance("AES"); cCipher.init(Cipher.ENCRYPT_MODE, new SecretKeySpec(new byte[18], "AES")); Assertions.extValue(0); diff --git a/CryptoAnalysis/src/test/java/tests/pattern/ExtractValueTest.java b/CryptoAnalysis/src/test/java/tests/pattern/ExtractValueTest.java index c09d8eaaa..2f64c92ac 100644 --- a/CryptoAnalysis/src/test/java/tests/pattern/ExtractValueTest.java +++ b/CryptoAnalysis/src/test/java/tests/pattern/ExtractValueTest.java @@ -29,6 +29,7 @@ public void charArrayExtractionTest(){ char[] v = new char[] {'p'}; final PBEKeySpec pbekeyspec = new PBEKeySpec(v, null, 65000, 128); Assertions.extValue(0); + Assertions.notHasEnsuredPredicate(pbekeyspec); } @Test public void testIntraproceduralStringFlow() throws GeneralSecurityException { @@ -63,7 +64,6 @@ public void testIntraproceduralNativeNoCalleeIntFlow() throws GeneralSecurityExc Assertions.extValue(0); } private String getAESReturn() { - int x = 222; return "AES"; } private String getAES() { diff --git a/CryptoAnalysis/src/test/java/tests/pattern/IssuesTest.java b/CryptoAnalysis/src/test/java/tests/pattern/IssuesTest.java index 1dcfe13fd..72b9c62f2 100644 --- a/CryptoAnalysis/src/test/java/tests/pattern/IssuesTest.java +++ b/CryptoAnalysis/src/test/java/tests/pattern/IssuesTest.java @@ -1,10 +1,18 @@ package tests.pattern; +import java.io.UnsupportedEncodingException; import java.security.GeneralSecurityException; import java.security.KeyFactory; import java.security.PublicKey; +import java.security.SecureRandom; import java.security.spec.X509EncodedKeySpec; +import javax.crypto.Cipher; +import javax.crypto.KeyGenerator; +import javax.crypto.SecretKey; +import javax.crypto.spec.IvParameterSpec; +import javax.security.auth.DestroyFailedException; + import org.junit.Test; import crypto.analysis.CrySLRulesetSelector.Ruleset; @@ -18,6 +26,48 @@ protected Ruleset getRuleSet() { return Ruleset.JavaCryptographicArchitecture; } + @Test + public void testIssue418() throws GeneralSecurityException { + // Related to issue 418: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/418 + SecureRandom sr = SecureRandom.getInstance("SHA1PRNG"); + Assertions.hasEnsuredPredicate(sr); + + byte[] secureBytes = new byte[32]; + (new SecureRandom()).nextBytes(secureBytes); + Assertions.hasEnsuredPredicate(secureBytes); + + sr.setSeed(secureBytes); + + Assertions.hasEnsuredPredicate(sr); + Assertions.predicateErrors(0); + Assertions.constraintErrors(0); + Assertions.typestateErrors(0); + } + + @Test + public void testIssue419() throws GeneralSecurityException, UnsupportedEncodingException, DestroyFailedException { + // Related to issue 419: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/419 + KeyGenerator keyGenerator = KeyGenerator.getInstance("AES"); + SecretKey secretKey = keyGenerator.generateKey(); + Assertions.hasEnsuredPredicate(secretKey); + + secretKey.destroy(); + Assertions.notHasEnsuredPredicate(secretKey); + + // generate secure iv + byte[] ivBytes = new byte[16]; + new SecureRandom().nextBytes(ivBytes); + IvParameterSpec iv = new IvParameterSpec(ivBytes); + Cipher cipher = Cipher.getInstance("AES/CBC/PKCS5Padding"); + + cipher.init(Cipher.ENCRYPT_MODE, secretKey, iv); + + // encrypt + byte[] plainText = "ThisIsThePlainText".getBytes("UTF-8"); + byte[] cipherText = cipher.doFinal(plainText); + Assertions.notHasEnsuredPredicate(cipherText); + } + @Test public void testIssue421() throws GeneralSecurityException { // Related to issue 421: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/421 diff --git a/CryptoAnalysis/src/test/java/tests/pattern/PBETest.java b/CryptoAnalysis/src/test/java/tests/pattern/PBETest.java index 08127eda1..1536b0c9e 100644 --- a/CryptoAnalysis/src/test/java/tests/pattern/PBETest.java +++ b/CryptoAnalysis/src/test/java/tests/pattern/PBETest.java @@ -53,6 +53,7 @@ public void pbeUsagePatternMinPBEIterationsMinimized() throws GeneralSecurityExc char[] corPwd = generateRandomPassword();; PBEKeySpec pbekeyspec = new PBEKeySpec(corPwd, salt, 100000, 128); Assertions.extValue(1); + Assertions.hasEnsuredPredicate(pbekeyspec); } @Test @@ -116,7 +117,9 @@ public void pbeUsagePattern2() throws GeneralSecurityException, IOException { Assertions.extValue(3); Assertions.mustNotBeInAcceptingState(pbekeyspec); Assertions.hasEnsuredPredicate(pbekeyspec); + pbekeyspec.clearPassword(); + Assertions.mustBeInAcceptingState(pbekeyspec); Assertions.notHasEnsuredPredicate(pbekeyspec); } @@ -134,6 +137,7 @@ public void pbeUsagePatternForbMeth() throws GeneralSecurityException, IOExcepti char[] falsePwd = "password".toCharArray(); final PBEKeySpec pbekeyspec = new PBEKeySpec(falsePwd); Assertions.callToForbiddenMethod(); + Assertions.notHasEnsuredPredicate(pbekeyspec); } } diff --git a/CryptoAnalysis/src/test/java/tests/pattern/SecretKeyTest.java b/CryptoAnalysis/src/test/java/tests/pattern/SecretKeyTest.java index 9a008382c..0cd3b6fb0 100644 --- a/CryptoAnalysis/src/test/java/tests/pattern/SecretKeyTest.java +++ b/CryptoAnalysis/src/test/java/tests/pattern/SecretKeyTest.java @@ -185,6 +185,7 @@ public void secretKeyTest4() throws NoSuchAlgorithmException, DestroyFailedExcep byte[] enc = key.getEncoded(); Assertions.mustBeInAcceptingState(key); enc = key.getEncoded(); + Assertions.hasEnsuredPredicate(enc); Assertions.mustBeInAcceptingState(key); ((SecretKey) key).destroy(); @@ -301,6 +302,7 @@ public void exceptionFlowTest() { Assertions.extValue(0); SecretKey key = keygen.generateKey(); Assertions.mustBeInAcceptingState(keygen); + Assertions.hasEnsuredPredicate(key); } @Test