Avoid bug, where getEncoded from class key is not resolved

CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java

@@ -8,6 +8,7 @@
 import java.net.URL;
 import java.net.URLClassLoader;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.HashSet;
 import java.util.List;
@@ -103,6 +104,12 @@ public class CrySLModelReader {
 	private static final String THIS = "this";
 	private static final String NULL = "null";
 	private static final String UNDERSCORE = "_";
+
+	/**
+	 * For some reason, xtext is not able to resolve a call to 'getEncoded()' for the class java.security.key
+	 * and its subclasses. In these cases, we have to manually resolve the call
+	 */
+	private static final Set<String> buggedKeyRules = new HashSet<>(Arrays.asList("java.security.Key", "javax.crypto.SecretKey", "java.security.PublicKey", "java.security.PrivateKey"));
 
 	/**
 	 * Creates a CrySLModelReader
@@ -213,8 +220,14 @@ private CrySLRule createRuleFromResource(Resource resource) throws CryptoAnalysi
 			throw new CryptoAnalysisException("Internal error creating a CrySL rule: 'resource parameter was null'.");
 		}
 
+		String currentClass = ((Domainmodel)resource.getContents().get(0)).getJavaType().getQualifiedName();
+
 		if (runValidator(resource, Severity.WARNING)) {
-			throw new CryptoAnalysisException("Skipping rule since it contains errors: " + resource.getURI());
+			if (buggedKeyRules.contains(currentClass)) {
+				LOGGER.info("Class " + currentClass + " is of type java.security.key. The call to 'getEncoded()' will be resolved manually.");
+			} else {
+				throw new CryptoAnalysisException("Skipping rule since it contains errors: " + resource.getURI());
+			}
 		}
 
 		try {
@@ -585,6 +598,10 @@ private ISLConstraint getBuiltinPredicate(BuiltinPredicate builtinPredicate) {
 		}
 		return new CrySLPredicate(null, name, parameters, negated);
 	}
+
+	public static Set<String> getBuggedKeyRules() {
+		return buggedKeyRules;
+	}
 
 	public static String filterQuotes(final String dirty) {
 		return CharMatcher.anyOf("\"").removeFrom(dirty);

CryptoAnalysis/src/main/java/crypto/cryslhandler/StateMachineGraphBuilder.java

@@ -204,8 +204,30 @@ private SubStateMachine buildSubSMG(final Order order, final Set<StateNode> star
 			Event event = ((Primary) order).getEvent();
 			StateNode node = this.result.createNewNode();
 			List<CrySLMethod> label = CrySLReaderUtils.resolveEventToCryslMethods(event);
-			for (StateNode startNode : startNodes)
-				this.result.createNewEdge(label, startNode, node);
+
+			/**
+			 * In some scenarios, xtext is not able to resolve the JVMExecutable 'getEncoded()' from the 
+			 * class java.security.Key or its subclasses. In these cases, xtext defaults to the constructor.
+			 * However, these classes have no constructors, since they are interfaces. To deal with the problem,
+			 * we manually change the constructor call to the 'getEncoded()' call.
+			 */
+			List<CrySLMethod> updatedLabels = new ArrayList<>(label);
+
+			for (CrySLMethod method : label) {
+				if (CrySLModelReader.getBuggedKeyRules().contains(method.getMethodName())) {
+					String updatedLabel = method.getMethodName() + ".getEncoded";
+					CrySLMethod updatedMethod = new CrySLMethod(updatedLabel, method.getParameters(), method.getRetObject());
+
+					updatedLabels.add(updatedMethod);
+				} else {
+					updatedLabels.add(method);
+				}
+			}
+
+			for (StateNode startNode : startNodes) {
+				this.result.createNewEdge(updatedLabels, startNode, node);
+			}
+
 			return new SubStateMachine(node, node);
 		}
 

CryptoAnalysis/src/main/java/crypto/typestate/CrySLMethodToSootMethod.java

@@ -56,10 +56,10 @@ private Collection<SootMethod> _convert(CrySLMethod label) {
 		Set<SootMethod> res = Sets.newHashSet();
 		String methodName = label.getMethodName();
 		String declaringClass = getDeclaringClass(methodName);
-//		Scene.v().forceResolve(declaringClass, SootClass.BODIES);
 		if (!Scene.v().containsClass(declaringClass)){
 			return res;
 		}
+		Scene.v().forceResolve(declaringClass, SootClass.BODIES);
 		SootClass sootClass = Scene.v().getSootClass(declaringClass);
 		List<SootClass> classes = Lists.newArrayList(sootClass);
 		String methodNameWithoutDeclaringClass = getMethodNameWithoutDeclaringClass(methodName);