Crypto: Add missing block mode JCA Models, add block mode unit tests

Author: bdrodes

java/ql/lib/experimental/quantum/JCA.qll

@@ -30,16 +30,6 @@ module JCAModel {
           ].toUpperCase())
   }
 
-  // TODO: Verify that the CFB% case works correctly
-  bindingset[mode]
-  predicate cipher_modes(string mode) {
-    mode.toUpperCase()
-        .matches([
-            "NONE", "CBC", "CCM", "CFB", "CFB%", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB",
-            "OFB%", "PCBC"
-          ].toUpperCase())
-  }
-
   // TODO: Verify that the OAEPWith% case works correctly
   bindingset[padding]
   predicate cipher_padding(string padding) {
@@ -184,6 +174,14 @@ module JCAModel {
     type = KeyOpAlg::SIV() and name = "SIV"
     or
     type = KeyOpAlg::OCB() and name = "OCB"
+    or
+    type = KeyOpAlg::CFB() and name = "CFB"
+    or
+    type = KeyOpAlg::OFB() and name = "OFB"
+    or
+    type = KeyOpAlg::PCBC() and name = "PCBC"
+    or
+    type = KeyOpAlg::KWP() and name = "KWP"
   }
 
   bindingset[name]

java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/Test.java

@@ -0,0 +1,57 @@
+import javax.crypto.Cipher;
+import javax.crypto.KeyGenerator;
+import javax.crypto.SecretKey;
+import javax.crypto.spec.IvParameterSpec;
+
+public class Test {
+    public static void main(String[] args) throws Exception {
+        SecretKey key = KeyGenerator.getInstance("AES").generateKey();
+        IvParameterSpec iv = new IvParameterSpec(new byte[16]);
+        byte[] data = "SensitiveData".getBytes();
+
+        // Insecure block mode: ECB
+        Cipher cipherECB = Cipher.getInstance("AES/ECB/PKCS5Padding"); // $Alert
+        cipherECB.init(Cipher.ENCRYPT_MODE, key);
+        byte[] ecbEncrypted = cipherECB.doFinal(data);
+        System.out.println("ECB encrypted: " + bytesToHex(ecbEncrypted));
+
+        // Insecure block mode: CFB
+        Cipher cipherCFB = Cipher.getInstance("AES/CFB/PKCS5Padding"); // $Alert
+        cipherCFB.init(Cipher.ENCRYPT_MODE, key, iv);
+        byte[] cfbEncrypted = cipherCFB.doFinal(data);
+        System.out.println("CFB encrypted: " + bytesToHex(cfbEncrypted));
+
+        // Insecure block mode: OFB
+        Cipher cipherOFB = Cipher.getInstance("AES/OFB/PKCS5Padding"); // $Alert
+        cipherOFB.init(Cipher.ENCRYPT_MODE, key, iv);
+        byte[] ofbEncrypted = cipherOFB.doFinal(data);
+        System.out.println("OFB encrypted: " + bytesToHex(ofbEncrypted));
+
+        // Insecure block mode: CTR
+        Cipher cipherCTR = Cipher.getInstance("AES/CTR/NoPadding"); // $Alert
+        cipherCTR.init(Cipher.ENCRYPT_MODE, key, iv);
+        byte[] ctrEncrypted = cipherCTR.doFinal(data);
+        System.out.println("CTR encrypted: " + bytesToHex(ctrEncrypted));
+
+        // Secure block mode: CBC with random IV
+        IvParameterSpec randomIv = new IvParameterSpec(KeyGenerator.getInstance("AES").generateKey().getEncoded());
+        Cipher cipherCBCRandomIV = Cipher.getInstance("AES/CBC/PKCS5Padding");
+        cipherCBCRandomIV.init(Cipher.ENCRYPT_MODE, key, randomIv);
+        byte[] cbcRandomIVEncrypted = cipherCBCRandomIV.doFinal(data);
+        System.out.println("CBC (random IV) encrypted: " + bytesToHex(cbcRandomIVEncrypted));
+
+        // Secure block mode: GCM (authenticated encryption)
+        IvParameterSpec gcmIv = new IvParameterSpec(new byte[12]);
+        Cipher cipherGCM = Cipher.getInstance("AES/GCM/NoPadding");
+        cipherGCM.init(Cipher.ENCRYPT_MODE, key, gcmIv);
+        byte[] gcmEncrypted = cipherGCM.doFinal(data);
+        System.out.println("GCM encrypted: " + bytesToHex(gcmEncrypted));
+    }
+
+    private static String bytesToHex(byte[] bytes) {
+        StringBuilder sb = new StringBuilder();
+        for (byte b : bytes)
+            sb.append(String.format("%02x", b));
+        return sb.toString();
+    }
+}

java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.expected

@@ -0,0 +1,4 @@
+| Test.java:13:47:13:68 | KeyOperationAlgorithm | Weak AES block mode instance $@. | Test.java:13:47:13:68 | ModeOfOperation | ModeOfOperation |
+| Test.java:19:47:19:68 | KeyOperationAlgorithm | Weak AES block mode instance $@. | Test.java:19:47:19:68 | ModeOfOperation | ModeOfOperation |
+| Test.java:25:47:25:68 | KeyOperationAlgorithm | Weak AES block mode instance $@. | Test.java:25:47:25:68 | ModeOfOperation | ModeOfOperation |
+| Test.java:31:47:31:65 | KeyOperationAlgorithm | Weak AES block mode instance $@. | Test.java:31:47:31:65 | ModeOfOperation | ModeOfOperation |

java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.qlref

@@ -0,0 +1,4 @@
+query: experimental/quantum/Examples/WeakBlockModes.ql
+postprocess:
+  - utils/test/PrettyPrintModels.ql
+  - utils/test/InlineExpectationsTestQuery.ql

shared/quantum/codeql/quantum/experimental/Standardization.qll

@@ -214,7 +214,9 @@ module Types {
       CCM() or // Used in lightweight cryptography (IoT, WPA2)
       SIV() or // Misuse-resistant encryption, used in secure storage
       OCB() or // Efficient AEAD mode
+      KWP() or
       OFB() or
+      PCBC() or
       OtherMode()
 
     class ModeOfOperationType extends TModeOfOperationType {