Add simple example for issue #219

src/test/java/de/fraunhofer/aisec/codyze/crymlin/IssueTest.java

@@ -0,0 +1,14 @@
+
+package de.fraunhofer.aisec.codyze.crymlin;
+
+import org.junit.jupiter.api.Test;
+
+class IssueTest extends AbstractMarkTest {
+
+	@Test
+	void issue219() throws Exception {
+		var findings = performTest("issues/219/Main.java", "issues/219/");
+		findings.forEach(System.out::println);
+	}
+
+}

src/test/resources/issues/219/Main.java

@@ -0,0 +1,9 @@
+import java.security.SecureRandom;
+
+public class Main {
+
+    public void test() {
+        SecureRandom secureRandom = SecureRandom.getInstance("SHA1PRNG");
+    }
+
+}

src/test/resources/issues/219/PBEParameterSpec.mark

@@ -0,0 +1,20 @@
+package java.jca
+
+entity PBEParameterSpec {
+
+	var salt;
+	var iterationCount;
+	var paramSpec;
+
+	op instantiate {
+		javax.crypto.spec.PBEParameterSpec(
+			salt : byte[],
+			iterationCount : int
+		);
+		javax.crypto.spec.PBEParameterSpec(
+			salt : byte[],
+			iterationCount : int,
+			paramSpec : java.security.AlgorithmParameter
+		);
+	}
+}

src/test/resources/issues/219/SecureRandom.mark

@@ -0,0 +1,58 @@
+package java.jca
+
+entity SecureRandom {
+
+    var algorithm;
+    var provider;
+    var params;
+    var seed;
+    var numBytes;
+    var randomBytes;
+
+    op instantiate {
+        java.security.SecureRandom.getInstance(algorithm : java.lang.String);
+        java.security.SecureRandom.getInstance(
+            algorithm : java.lang.String,
+            provider : java.lang.String | java.security.Provider
+        );
+        java.security.SecureRandom.getInstance(
+            algorithm : java.lang.String,
+            params : java.security.SecureRandomParameters
+        );
+        java.security.SecureRandom.getInstance(
+            algorithm : java.lang.String,
+            params : java.security.SecureRandomParameters,
+            provider : java.lang.String | java.security.Provider
+        );
+        java.security.SecureRandom.getInstanceStrong();
+
+        // forbidden calls because they don't respect BC as provider
+        forbidden java.security.SecureRandom();
+        forbidden java.security.SecureRandom(
+            seed : byte[]
+        );
+    }
+
+    op seed {
+        java.security.SecureRandom.setSeed(seed : byte[] | long);
+    }
+
+    op reseed {
+        java.security.SecureRandom.reseed();
+        java.security.SecureRandom.reseed(params : java.security.SecureRandomParameters);
+    }
+
+    op generateSeed {
+        seed = java.security.SecureRandom.generateSeed(numBytes : int);
+    }
+
+    op generate {
+        java.security.SecureRandom.next(numBytes : int);
+        java.security.SecureRandom.nextBytes(randomBytes : bytes[]);
+        java.security.SecureRandom.nextBytes(
+            randomBytes : bytes[],
+            params : java.security.SecureRandomParameters
+        );
+    }
+
+}

src/test/resources/issues/219/rules.mark

@@ -0,0 +1,11 @@
+package issue_219
+
+rule JCAProvider_PBEParameterSpec_2{
+	using
+		PBEParameterSpec as pbeps,
+		SecureRandom as sr
+	ensure
+		_is(pbeps.salt, sr)
+	onfail
+		NotRandomizedSaltPBEParameterSpec
+}