rule correctness tests initial commit

.github/workflows/rule_correctness_test.yml

@@ -0,0 +1,19 @@
+name: Validate CrySL Rules
+
+on:
+  pull_request:
+
+jobs:
+  Validation:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+      - name: Set up JDK 17
+        uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-package: jdk
+          java-version: 17
+      - name: Validate Rules with Maven
+        run: mvn clean test -f RuleCorrectnessTests

BouncyCastle/src/PaddedBufferedBlockCipher.crysl

@@ -3,7 +3,7 @@ SPEC org.bouncycastle.crypto.paddings.PaddedBufferedBlockCipher
 OBJECTS
 	org.bouncycastle.crypto.CipherParameters params;
 	org.bouncycastle.crypto.paddings.BlockCipherPadding padding;
-	org.bouncycastle.crypto.engines.RijndaelEngine cipher;
+	org.bouncycastle.crypto.BlockCipher cipher;
 
 	byte plainTextByte;
 	byte[] plainText;
@@ -41,7 +41,7 @@ CONSTRAINTS
 	cipherTextOffset >= 0;
 
 REQUIRES
-	generatedRijndaelEngine[cipher];
+	generatedBlockCipher[cipher];
 	generatedParametersWithIV[params];
 	generatedPKCS7Padding[padding];
 

RuleCorrectnessTests/.gitignore

@@ -0,0 +1,12 @@
+target/
+pom.xml.tag
+pom.xml.releaseBackup
+pom.xml.versionsBackup
+pom.xml.next
+release.properties
+dependency-reduced-pom.xml
+buildNumber.properties
+.mvn/timing.properties
+.mvn/wrapper/maven-wrapper.jar
+.project
+.classpath

RuleCorrectnessTests/pom.xml

@@ -0,0 +1,80 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+
+    <parent>
+        <groupId>de.darmstadt.tu.crossing.CrySL</groupId>
+        <artifactId>de.darmstadt.tu.crossing.CrySL.parent</artifactId>
+        <version>4.0.2</version>
+    </parent>
+
+    <groupId>de.cognicrypt.crysl</groupId>
+    <artifactId>RuleCorrectnessTests</artifactId>
+    <version>1.0.0</version>
+    <packaging>jar</packaging>
+
+    <name>RuleCorrectnessTests</name>
+    <description>CrySL Rule Correctness Tests</description>
+    <url>https://github.com/CROSSINGTUD/CryptSL</url>
+
+    <properties>
+        <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
+    </properties>
+
+    <dependencies>
+        <dependency>
+            <groupId>de.darmstadt.tu.crossing.CrySL</groupId>
+            <artifactId>CrySLParser</artifactId>
+            <version>4.0.2</version>
+        </dependency>
+        <dependency>
+            <groupId>org.bouncycastle</groupId>
+            <artifactId>bcprov-jdk18on</artifactId>
+            <version>1.80</version>
+        </dependency>
+        <dependency>
+            <groupId>com.google.crypto.tink</groupId>
+            <artifactId>tink</artifactId>
+            <version>1.17.0</version>
+        </dependency>
+        <dependency>
+            <groupId>junit</groupId>
+            <artifactId>junit</artifactId>
+            <version>4.13.2</version>
+            <scope>test</scope>
+        </dependency>
+    </dependencies>
+    <build>
+        <plugins>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-surefire-plugin</artifactId>
+                <version>3.0.0</version>
+            </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-compiler-plugin</artifactId>
+                <version>3.14.0</version>
+                <configuration>
+                    <source>11</source>
+                    <target>11</target>
+                </configuration>
+            </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-source-plugin</artifactId>
+                <version>3.3.1</version>
+                <executions>
+                    <execution>
+                        <id>attach-sources</id>
+                        <goals>
+                            <goal>jar</goal>
+                        </goals>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+</project>

RuleCorrectnessTests/src/main/java/de/cognicrypt/crysl/Main.java

@@ -0,0 +1,7 @@
+package de.cognicrypt.crysl;
+
+public class Main {
+    public static void main(String[] args) {
+        System.out.println("Hello world!");
+    }
+}

RuleCorrectnessTests/src/test/java/de/rulecorrectness/tests/RuleCorrectnessTest.java

@@ -0,0 +1,83 @@
+package de.rulecorrectness.tests;
+
+
+import crysl.CrySLParser;
+import crysl.rule.CrySLRule;
+import org.junit.Test;
+import org.junit.Assert;
+
+import java.io.IOException;
+import java.util.Collection;
+import java.io.File;
+
+
+public class RuleCorrectnessTest {
+
+    /**
+     * Counts the total number of CrySL files in a given directory path
+     *
+     * @param directoryPath The path to the directory containing CrySL rules
+     * @return The number of .crysl files found
+     */
+    private int countCrySLFiles(String directoryPath) {
+        File directory = new File(directoryPath);
+        if (!directory.exists()) {
+            throw new RuntimeException("Directory does not exist: " + directoryPath);
+        }
+
+        int count = 0;
+        File[] allFiles = directory.listFiles();
+
+        if (allFiles != null) {
+            for (File file : allFiles) {
+                if (file.isFile() && file.getName().endsWith(".crysl")) {
+                    count++;
+                } else if (file.isDirectory()) {
+                    count += countCrySLFiles(file.getAbsolutePath());
+                }
+            }
+        }
+
+        return count;
+    }
+    @Test
+    public void jcaCorrectnessTest() throws IOException {
+        CrySLParser parser = new CrySLParser();
+        String jcaRulesPath = "./../JavaCryptographicArchitecture/src";
+        Collection<CrySLRule> jcaRules = parser.parseRulesFromPath(jcaRulesPath);
+        int ExpectedCount = countCrySLFiles(jcaRulesPath);
+
+        Assert.assertEquals(ExpectedCount, jcaRules.size());
+    }
+
+    @Test
+    public void BouncyCastleCorrectnessTest() throws IOException {
+        CrySLParser parser = new CrySLParser();
+        String bouncyCastlePath = "./../BouncyCastle/src";
+        Collection<CrySLRule> bouncyCastleRules = parser.parseRulesFromPath(bouncyCastlePath);
+        int ExpectedCount = countCrySLFiles(bouncyCastlePath);
+
+        Assert.assertEquals(ExpectedCount, bouncyCastleRules.size());
+    }
+
+    @Test
+    public void BouncyCastleJCACorrectnessTest() throws IOException {
+        CrySLParser parser = new CrySLParser();
+        String bouncyCastleJCAPath = "./../BouncyCastle-JCA/src";
+        Collection<CrySLRule> bouncyCastleJCARules = parser.parseRulesFromPath(bouncyCastleJCAPath);
+        int ExpectedCount = countCrySLFiles(bouncyCastleJCAPath);
+
+        Assert.assertEquals(ExpectedCount, bouncyCastleJCARules.size());
+    }
+
+    @Test
+    public void TinkCorrectnessTest() throws IOException {
+        CrySLParser parser = new CrySLParser();
+        String tinkPath = "./../Tink/src";
+        Collection<CrySLRule> tinkRules = parser.parseRulesFromPath(tinkPath);
+        int ExpectedCount = countCrySLFiles(tinkPath);
+
+        Assert.assertEquals(ExpectedCount, tinkRules.size());
+    }
+
+}

Tink/src/HybridKeyTemplates.crysl

@@ -22,8 +22,8 @@ OBJECTS
 	com.google.crypto.tink.proto.KeyTemplate ecies_aes128_ctr_hmac; 
 
 EVENTS
-   	ecies_aes128_gcm_evt: ecies_aes128_gcm = createEciesAeadHkdfKeyTemplate(_, _, _, _, _);
-	ecies_aes128_ctr_hmac_evt: ecies_aes128_ctr_hmac = createEciesAeadHkdfKeyTemplate(_, _, _, _, _);
+   	ecies_aes128_gcm_evt: ecies_aes128_gcm = createEciesAeadHkdfKeyTemplate(_, _, _, _, _, _);
+	ecies_aes128_ctr_hmac_evt: ecies_aes128_ctr_hmac = createEciesAeadHkdfKeyTemplate(_, _, _, _, _, _);
 
 	CreateKeyTemplates := ecies_aes128_gcm_evt | ecies_aes128_ctr_hmac_evt;
 

Tink/src/KeysetHandle.crysl

@@ -11,12 +11,12 @@ SPEC com.google.crypto.tink.KeysetHandle
 OBJECTS
     com.google.crypto.tink.KeyTemplate kt;
     com.google.crypto.tink.KeysetHandle publicKeysetHandle; 
-    com.google.crypto.tink.mac.HmacParameters hmacParams;
+    com.google.crypto.tink.Parameters params;
 
 
 EVENTS
     gen_evt        : generateNew(kt);
-    gen_hmac_evt   : generateNew(hmacParams);
+    gen_hmac_evt   : generateNew(params);
     gen_public_evt : publicKeysetHandle = getPublicKeysetHandle();
     read_evt       : read(_, _); 
     export_evt     : write(_, _); 
@@ -28,7 +28,7 @@ ORDER
 
 REQUIRES
 	genKeyTemplate[kt];
-	hmacParams[hmacParams];
+	genParams[params];
 
 
 ENSURES