From f480d90a68e8d179bef46871ad70e63ad13fe515 Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Fri, 17 Oct 2025 13:13:14 -0400 Subject: [PATCH] Crypto: Add missing block mode JCA Models, add block mode unit tests --- java/ql/lib/experimental/quantum/JCA.qll | 18 +++--- .../examples/WeakOrUnknownBlockMode/Test.java | 57 +++++++++++++++++++ .../WeakBlockMode.expected | 4 ++ .../WeakBlockMode.qlref | 4 ++ .../quantum/experimental/Standardization.qll | 2 + 5 files changed, 75 insertions(+), 10 deletions(-) create mode 100644 java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/Test.java create mode 100644 java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.expected create mode 100644 java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.qlref diff --git a/java/ql/lib/experimental/quantum/JCA.qll b/java/ql/lib/experimental/quantum/JCA.qll index b74b20d9836..d0b32b51f35 100644 --- a/java/ql/lib/experimental/quantum/JCA.qll +++ b/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] diff --git a/java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/Test.java b/java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/Test.java new file mode 100644 index 00000000000..0c8b3b6691d --- /dev/null +++ b/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(); + } +} \ No newline at end of file diff --git a/java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.expected b/java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.expected new file mode 100644 index 00000000000..859a138d3eb --- /dev/null +++ b/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 | diff --git a/java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.qlref b/java/ql/test/experimental/query-tests/quantum/examples/WeakOrUnknownBlockMode/WeakBlockMode.qlref new file mode 100644 index 00000000000..ec8500ddda7 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/shared/quantum/codeql/quantum/experimental/Standardization.qll b/shared/quantum/codeql/quantum/experimental/Standardization.qll index aac9e30c3b6..be281e2fbfd 100644 --- a/shared/quantum/codeql/quantum/experimental/Standardization.qll +++ b/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 {