Merge pull request #487 from CROSSINGTUD/issue_418_419

Update negates mechanism

CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java

@@ -122,15 +122,8 @@ public void execute() {
 		runExtractParameterAnalysis();
 		checkInternalConstraints();
 
-		Multimap<Statement, State> unitToStates = HashMultimap.create();
-		for (Cell<Statement, Val, TransitionFunction> 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<Statement, Val, TransitionFunction> c : results.asStatementValWeightTable().cellSet()) {
+			Collection<? extends State> 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<Statement> 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<Statement, Val, TransitionFunction> 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<Statement, Val, TransitionFunction> 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<StateNode> conditionalMethods, State state) {
@@ -591,6 +605,60 @@ private boolean isConditionalState(Set<StateNode> conditionalMethods, State stat
 		}
 		return false;
 	}
+
+	private boolean isPredicateNegatingState(CrySLPredicate ensPred, State stateNode, List<CrySLPredicate> 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<ISLConstraint> getMissingPredicates() {
 		return missingPredicates;

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<CrySLPredicate> predicates = Lists.newArrayList();
+		final List<CrySLPredicate> 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<Event> changeDeclaringClass(JvmTypeReference currentClass, EventsBlock eventsBlock) {
@@ -562,11 +565,28 @@ private Set<StateNode> getStatesForMethods(final List<CrySLMethod> condition) {
 
 		for (final TransitionEdge transition : this.smg.getAllTransitions()) {
 			if(transition.getLabel().containsAll(condition)) {
-				predicateGenerationNodes.add(transition.getRight());
+				Set<StateNode> reachableNodes = getAllReachableNodes(transition.getRight(), Sets.newHashSet());
+
+				predicateGenerationNodes.addAll(reachableNodes);
 			}
 		}
 		return predicateGenerationNodes;
 	}
+
+	private Set<StateNode> getAllReachableNodes(final StateNode startNode, Set<StateNode> visited) {
+		if (visited.contains(startNode)) {
+			return visited;
+		}
+
+		visited.add(startNode);
+
+		for (TransitionEdge edge : this.smg.getAllOutgoingEdges(startNode)) {
+			Set<StateNode> reachableNodes = getAllReachableNodes(edge.getRight(), visited);
+
+			visited.addAll(reachableNodes);
+		}
+		return visited;
+	}
 
 	private ISLConstraint getBuiltinPredicate(BuiltinPredicate builtinPredicate) {
 		String name = builtinPredicate.getPredicate().getLiteral();

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<CrySLPredicate> predicates;
 
-	public CrySLRule(String className, List<Entry<String, String>> objects, List<CrySLForbiddenMethod> forbiddenMethods, StateMachineGraph usagePattern, List<ISLConstraint> constraints, List<CrySLPredicate> predicates) {
+	protected final List<CrySLPredicate> negatedPredicates;
+
+	public CrySLRule(String className, List<Entry<String, String>> objects, List<CrySLForbiddenMethod> forbiddenMethods, StateMachineGraph usagePattern, List<ISLConstraint> constraints, List<CrySLPredicate> predicates, List<CrySLPredicate> 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<ISLConstraint> getConstraints() {
 	public List<CrySLPredicate> getPredicates() {
 		return predicates;
 	}
+
+	/**
+	 * @return the negated predicates
+	 */
+	public List<CrySLPredicate> 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();
 	}
 

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);

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() {

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