Investigation of issue #219 (#445)

Add a test case to investigate issue #219. The result is expected. However, see discussion of #219.

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

@@ -0,0 +1,16 @@
+package de.fraunhofer.aisec.codyze.crymlin
+
+import java.lang.Exception
+import kotlin.Throws
+import org.junit.jupiter.api.Test
+
+class IssueTest : AbstractMarkTest() {
+
+    @Test
+    @Throws(Exception::class)
+    fun issue219() {
+        val findings = performTest("issues/219/Main.java", "issues/219/")
+
+        expected(findings, "line 6: Rule JCAProvider_PBEParameterSpec_2 violated")
+    }
+}

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
+}