Merge pull request #20696 from bdrodes/bad_mac_decrypt_then_mac

Crypto: Adding bad decrypt then mac order query.
2025-12-16 16:53:25 +01:00 · 2025-10-24 22:07:26 +02:00
parent a0a6f288b5 65d0ca9e53
commit e7bd435bee
9 changed files with 329 additions and 47 deletions
--- a/java/ql/integration-tests/java/query-suite/not_included_in_qls.expected
+++ b/java/ql/integration-tests/java/query-suite/not_included_in_qls.expected
@@ -228,6 +228,7 @@ ql/java/ql/src/experimental/Security/CWE/CWE-665/InsecureRmiJmxEnvironmentConfig
 ql/java/ql/src/experimental/Security/CWE/CWE-755/NFEAndroidDoS.ql
 ql/java/ql/src/experimental/Security/CWE/CWE-759/HashWithoutSalt.ql
 ql/java/ql/src/experimental/Security/CWE/CWE-939/IncorrectURLVerification.ql
+ql/java/ql/src/experimental/quantum/Examples/BadMacOrderDecryptThenMac.ql
 ql/java/ql/src/experimental/quantum/Examples/BadMacOrderDecryptToMac.ql
 ql/java/ql/src/experimental/quantum/Examples/BadMacOrderMacOnEncryptPlaintext.ql
 ql/java/ql/src/experimental/quantum/Examples/BrokenCrypto.ql
--- a/java/ql/src/experimental/quantum/Examples/BadMacOrder.qll
+++ b/java/ql/src/experimental/quantum/Examples/BadMacOrder.qll
@@ -7,6 +7,7 @@ import codeql.util.Option
 * that flows to the input artifact of a mac operation.
 */
 predicate isDecryptToMacFlow(ArtifactFlow::PathNode src, ArtifactFlow::PathNode sink) {
+  // Simply flow from decrypt output to a mac input
  ArtifactFlow::flowPath(src, sink) and
  exists(Crypto::CipherOperationNode cipherOp |
    cipherOp.getKeyOperationSubtype() = Crypto::TDecryptMode() and
@@ -17,6 +18,11 @@ predicate isDecryptToMacFlow(ArtifactFlow::PathNode src, ArtifactFlow::PathNode
  )
 }

+/**
+ * Experimental interface for graph generation, supply the
+ * node to determine if a issue exists, and if so
+ * the graph can add a property on the node.
+ */
 predicate isDecryptToMacNode(Crypto::ArtifactNode node) {
  exists(ArtifactFlow::PathNode src |
    isDecryptToMacFlow(src, _) and
@@ -24,6 +30,10 @@ predicate isDecryptToMacNode(Crypto::ArtifactNode node) {
  )
 }

+predicate isDecryptThenMacFlow(DecryptThenMacFlow::PathNode src, DecryptThenMacFlow::PathNode sink) {
+  DecryptThenMacFlow::flowPath(src, sink)
+}
+
 /**
 * Holds when the src node is used as plaintext input to both
 * an encryption operation and a mac operation, via the
@@ -31,16 +41,140 @@ predicate isDecryptToMacNode(Crypto::ArtifactNode node) {
 */
 predicate isPlaintextInEncryptionAndMac(
  PlaintextUseAsMacAndCipherInputFlow::PathNode src,
-  PlaintextUseAsMacAndCipherInputFlow::PathNode sink, InterimArg arg
+  PlaintextUseAsMacAndCipherInputFlow::PathNode sink, EncryptOrMacCallArg arg
 ) {
  PlaintextUseAsMacAndCipherInputFlow::flowPath(src, sink) and
-  arg = sink.getState().asSome()
+  arg = sink.getState().asSome() and
+  // the above pathing adds flow steps that may not have consideration for the calling context
+  // TODO: this is something we want to look into to improving, but for now
+  // we can filter bad flows with one additional flow check, that the source goes to both
+  // src and sink through a generic flow
+  // note that the flow path above ensures src gets to the interim arg, so we just need to
+  // verify the source to sink.
+  // TODO: having to copy the generic data flow config into a use-use variant
+  // should we fix this at the language level to allow use use more intuitively?
+  // Seems to be a common issue.
+  GenericDataSourceFlowUseUseFlow::flow(src.getNode(), sink.getNode())
 }

-module ArgToSinkConfig implements DataFlow::ConfigSig {
+/**
+ * A copy of GenericDataSourceFlow but with use-use flows enabled by removing the barrier out
+ */
+module GenericDataSourceFlowUseUseConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    source = any(Crypto::GenericSourceInstance i).getOutputNode()
+  }
+
+  predicate isSink(DataFlow::Node sink) {
+    sink = any(Crypto::FlowAwareElement other).getInputNode()
+  }
+
+  predicate isBarrierIn(DataFlow::Node node) {
+    node = any(Crypto::FlowAwareElement element).getOutputNode()
+  }
+
+  predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    node1.(AdditionalFlowInputStep).getOutput() = node2
+    or
+    exists(MethodCall m |
+      m.getMethod().hasQualifiedName("java.lang", "String", "getBytes") and
+      node1.asExpr() = m.getQualifier() and
+      node2.asExpr() = m
+    )
+  }
+}
+
+module GenericDataSourceFlowUseUseFlow = TaintTracking::Global<GenericDataSourceFlowUseUseConfig>;
+
+module WrapperArgFlowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    // Start from a parameter and not a call to avoid flow going out of
+    // the call. We want to flow down a call, so start from a parameter
+    // and barrier flows through returns
+    exists(Method m | m.getParameter(_) = source.asParameter())
+  }
+
+  predicate isSink(DataFlow::Node sink) {
+    exists(Crypto::CipherOperationNode cipherOp |
+      cipherOp.getAnInputArtifact().asElement() = sink.asExpr()
+    )
+    or
+    exists(Crypto::MacOperationNode macOp | macOp.getAnInputArtifact().asElement() = sink.asExpr())
+  }
+
+  predicate isBarrierIn(DataFlow::Node node) {
+    node = any(Crypto::FlowAwareElement element).getOutputNode()
+  }
+
+  predicate isBarrierOut(DataFlow::Node node) {
+    // stop all flow out of a call return
+    // TODO: this might be too strict and remove taint flow, need to reassess
+    node.asExpr() instanceof Call or
+    node = any(Crypto::FlowAwareElement element).getInputNode()
+  }
+
+  predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    node1.(AdditionalFlowInputStep).getOutput() = node2
+    or
+    exists(MethodCall m |
+      m.getMethod().hasQualifiedName("java.lang", "String", "getBytes") and
+      node1.asExpr() = m.getQualifier() and
+      node2.asExpr() = m
+    )
+  }
+}
+
+module WrapperArgFlow = TaintTracking::Global<WrapperArgFlowConfig>;
+
+predicate encryptWrapperArg(DataFlow::Node n, DataFlow::Node sink) {
+  exists(Crypto::CipherOperationNode cipherOp |
+    cipherOp.getKeyOperationSubtype() = Crypto::TEncryptMode() and
+    cipherOp.getAnInputArtifact().asElement() = sink.asExpr()
+  ) and
+  (
+    exists(Parameter p, DataFlow::Node src |
+      p = src.asParameter() and
+      WrapperArgFlow::flow(src, sink) and
+      n.asExpr() = p.getAnArgument()
+    )
+    or
+    n = sink // the call the target operation is considered a wrapper arg to itself
+  )
+}
+
+predicate decryptWrapperArg(DataFlow::Node n, DataFlow::Node sink) {
+  exists(Crypto::CipherOperationNode cipherOp |
+    cipherOp.getKeyOperationSubtype() = Crypto::TDecryptMode() and
+    cipherOp.getAnInputArtifact().asElement() = sink.asExpr()
+  ) and
+  (
+    exists(Parameter p, DataFlow::Node src |
+      p = src.asParameter() and
+      WrapperArgFlow::flow(src, sink) and
+      n.asExpr() = p.getAnArgument()
+    )
+    or
+    n = sink // the call the target operation is considered a wrapper arg to itself
+  )
+}
+
+predicate macWrapperArg(DataFlow::Node n, DataFlow::Node sink) {
+  exists(Crypto::MacOperationNode macOp | macOp.getAnInputArtifact().asElement() = sink.asExpr()) and
+  (
+    exists(Parameter p, DataFlow::Node src |
+      p = src.asParameter() and
+      WrapperArgFlow::flow(src, sink) and
+      n.asExpr() = p.getAnArgument()
+    )
+    or
+    n = sink // the call the target operation is considered a wrapper arg to itself
+  )
+}
+
+module ArgToEncryptOrMacConfig implements DataFlow::ConfigSig {
  predicate isSource(DataFlow::Node source) { exists(Call c | c.getAnArgument() = source.asExpr()) }

-  predicate isSink(DataFlow::Node sink) { targetSinks(sink) }
+  predicate isSink(DataFlow::Node sink) { encryptOrMacSink(sink) }

  // Don't go in to a known out node, this will prevent the plaintext
  // from tracing out of cipher operations for example, we just want to trace
@@ -62,12 +196,12 @@ module ArgToSinkConfig implements DataFlow::ConfigSig {
  }
 }

-module ArgToSinkFlow = TaintTracking::Global<ArgToSinkConfig>;
+module ArgToEncryptOrMacFlow = TaintTracking::Global<ArgToEncryptOrMacConfig>;

 /**
 * Target sinks for this query are either encryption operations or mac operation message inputs
 */
-predicate targetSinks(DataFlow::Node n) {
+predicate encryptOrMacSink(DataFlow::Node n) {
  exists(Crypto::CipherOperationNode cipherOp |
    cipherOp.getKeyOperationSubtype() = Crypto::TEncryptMode() and
    cipherOp.getAnInputArtifact().asElement() = n.asExpr()
@@ -77,44 +211,36 @@ predicate targetSinks(DataFlow::Node n) {
 }

 /**
- * An argument of a target sink or a parent call whose parameter flows to a target sink
+ * Target sinks for decryption operations
 */
-class InterimArg extends DataFlow::Node {
-  DataFlow::Node targetSink;
-
-  InterimArg() {
-    targetSinks(targetSink) and
-    (
-      this = targetSink
-      or
-      ArgToSinkFlow::flow(this, targetSink) and
-      this.getEnclosingCallable().calls+(targetSink.getEnclosingCallable())
-    )
-  }
-
-  DataFlow::Node getTargetSink() { result = targetSink }
+predicate decryptSink(DataFlow::Node n) {
+  exists(Crypto::CipherOperationNode cipherOp |
+    cipherOp.getKeyOperationSubtype() = Crypto::TDecryptMode() and
+    cipherOp.getAnInputArtifact().asElement() = n.asExpr()
+  )
 }

-/**
- * A wrapper class to represent a target argument dataflow node.
- */
-class TargetArg extends DataFlow::Node {
-  TargetArg() { targetSinks(this) }
+class EncryptOrMacCallArg extends DataFlow::Node {
+  boolean isEncryption;

-  predicate isCipher() {
+  EncryptOrMacCallArg() {
    exists(Crypto::CipherOperationNode cipherOp |
      cipherOp.getKeyOperationSubtype() = Crypto::TEncryptMode() and
      cipherOp.getAnInputArtifact().asElement() = this.asExpr()
-    )
+    ) and
+    isEncryption = true
+    or
+    exists(Crypto::MacOperationNode macOp | macOp.getAnInputArtifact().asElement() = this.asExpr()) and
+    isEncryption = false
  }

-  predicate isMac() {
-    exists(Crypto::MacOperationNode macOp | macOp.getAnInputArtifact().asElement() = this.asExpr())
-  }
+  predicate isEncryption() { isEncryption = true }
+
+  predicate isMac() { isEncryption = false }
 }

 module PlaintextUseAsMacAndCipherInputConfig implements DataFlow::StateConfigSig {
-  class FlowState = Option<TargetArg>::Option;
+  class FlowState = Option<EncryptOrMacCallArg>::Option;

  // TODO: can we approximate a message source better?
  predicate isSource(DataFlow::Node source, FlowState state) {
@@ -128,12 +254,9 @@ module PlaintextUseAsMacAndCipherInputConfig implements DataFlow::StateConfigSig
  }

  predicate isSink(DataFlow::Node sink, FlowState state) {
-    sink instanceof TargetArg and
-    (
-      sink.(TargetArg).isMac() and state.asSome().isCipher()
-      or
-      sink.(TargetArg).isCipher() and state.asSome().isMac()
-    )
+    sink.(EncryptOrMacCallArg).isMac() and state.asSome().isEncryption()
+    or
+    sink.(EncryptOrMacCallArg).isEncryption() and state.asSome().isMac()
  }

  predicate isBarrierOut(DataFlow::Node node, FlowState state) {
@@ -163,16 +286,51 @@ module PlaintextUseAsMacAndCipherInputConfig implements DataFlow::StateConfigSig
  predicate isAdditionalFlowStep(
    DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2
  ) {
-    (exists(state1.asSome()) or state1.isNone()) and
-    targetSinks(node1) and
-    node1 instanceof TargetArg and
-    //use-use flow, either flow directly from the node1 use
-    //or find a parent call in the call in the call stack
-    //and continue flow from that parameter
-    node2.(InterimArg).getTargetSink() = node1 and
+    // TODO: should we consider isSome cases?
+    state1.isNone() and
+    (
+      encryptWrapperArg(node2, node1)
+      or
+      macWrapperArg(node2, node1)
+    ) and
    state2.asSome() = node1
  }
 }

 module PlaintextUseAsMacAndCipherInputFlow =
  TaintTracking::GlobalWithState<PlaintextUseAsMacAndCipherInputConfig>;
+
+module DecryptThenMacConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    exists(Crypto::CipherOperationNode cipherOp |
+      cipherOp.getKeyOperationSubtype() = Crypto::TDecryptMode() and
+      cipherOp.getAnInputArtifact().asElement() = source.asExpr()
+    )
+  }
+
+  predicate isSink(DataFlow::Node sink) {
+    exists(Crypto::MacOperationNode macOp | macOp.getAnInputArtifact().asElement() = sink.asExpr())
+  }
+
+  // Don't go in to a known out node, prevents
+  // from tracing out of an operation
+  // NOTE: we are not using a barrier out on input nodes, because
+  // that would remove 'use-use' flows, which we need
+  predicate isBarrierIn(DataFlow::Node node) {
+    node = any(Crypto::FlowAwareElement element).getOutputNode()
+  }
+
+  predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    node1.(AdditionalFlowInputStep).getOutput() = node2
+    or
+    exists(MethodCall m |
+      m.getMethod().hasQualifiedName("java.lang", "String", "getBytes") and
+      node1.asExpr() = m.getQualifier() and
+      node2.asExpr() = m
+    )
+    or
+    decryptWrapperArg(node2, node1)
+  }
+}
+
+module DecryptThenMacFlow = TaintTracking::Global<DecryptThenMacConfig>;
--- a/java/ql/src/experimental/quantum/Examples/BadMacOrderDecryptThenMac.ql
+++ b/java/ql/src/experimental/quantum/Examples/BadMacOrderDecryptThenMac.ql
@@ -0,0 +1,19 @@
+/**
+ * @name Bad MAC order: decrypt then mac
+ * @description Decryption on cipher text, then MAC on cipher text, is incorrect order
+ * @id java/quantum/examples/bad-mac-order-decrypt-then-mac
+ * @kind path-problem
+ * @problem.severity error
+ * @tags quantum
+ *       experimental
+ */
+
+import java
+import BadMacOrder
+import DecryptThenMacFlow::PathGraph
+
+from DecryptThenMacFlow::PathNode src, DecryptThenMacFlow::PathNode sink
+where isDecryptThenMacFlow(src, sink)
+select sink, src, sink,
+  "Incorrect decryption and MAC order: " +
+    "Decryption of cipher text occurs before validation of MAC on cipher text."
--- a/java/ql/src/experimental/quantum/Examples/BadMacOrderMacOnEncryptPlaintext.ql
+++ b/java/ql/src/experimental/quantum/Examples/BadMacOrderMacOnEncryptPlaintext.ql
@@ -14,7 +14,7 @@ import PlaintextUseAsMacAndCipherInputFlow::PathGraph

 from
  PlaintextUseAsMacAndCipherInputFlow::PathNode src,
-  PlaintextUseAsMacAndCipherInputFlow::PathNode sink, InterimArg arg
+  PlaintextUseAsMacAndCipherInputFlow::PathNode sink, EncryptOrMacCallArg arg
 where isPlaintextInEncryptionAndMac(src, sink, arg)
 select sink, src, sink,
  "Incorrect MAC usage: Encryption plaintext also used for MAC. Flow shows plaintext to final use through intermediate mac or encryption operation here $@",
--- a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.expected
+++ b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.expected
@@ -0,0 +1,36 @@
+#select
+| BadMacUse.java:152:42:152:51 | ciphertext | BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:152:42:152:51 | ciphertext | Incorrect decryption and MAC order: Decryption of cipher text occurs before validation of MAC on cipher text. |
+edges
+| BadMacUse.java:84:42:84:53 | bytes : byte[] | BadMacUse.java:92:31:92:35 | bytes : byte[] | provenance |  |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:100:39:100:48 | ciphertext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:100:39:100:48 | ciphertext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:108:39:108:47 | plaintext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:108:39:108:47 | plaintext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:118:52:118:60 | plaintext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:118:52:118:60 | plaintext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:146:48:146:57 | ciphertext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:146:48:146:57 | ciphertext : byte[] | provenance | Config |
+| BadMacUse.java:99:39:99:55 | ciphertext : byte[] | BadMacUse.java:100:39:100:48 | ciphertext : byte[] | provenance |  |
+| BadMacUse.java:100:39:100:48 | ciphertext : byte[] | BadMacUse.java:84:42:84:53 | bytes : byte[] | provenance |  |
+| BadMacUse.java:100:39:100:48 | ciphertext : byte[] | BadMacUse.java:84:42:84:53 | bytes : byte[] | provenance |  |
+| BadMacUse.java:108:39:108:47 | plaintext : byte[] | BadMacUse.java:84:42:84:53 | bytes : byte[] | provenance |  |
+| BadMacUse.java:118:52:118:60 | plaintext : byte[] | BadMacUse.java:84:42:84:53 | bytes : byte[] | provenance |  |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] | BadMacUse.java:99:39:99:55 | ciphertext : byte[] | provenance |  |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] | BadMacUse.java:152:42:152:51 | ciphertext | provenance |  |
+nodes
+| BadMacUse.java:84:42:84:53 | bytes : byte[] | semmle.label | bytes : byte[] |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | semmle.label | bytes : byte[] |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | semmle.label | bytes : byte[] |
+| BadMacUse.java:99:39:99:55 | ciphertext : byte[] | semmle.label | ciphertext : byte[] |
+| BadMacUse.java:100:39:100:48 | ciphertext : byte[] | semmle.label | ciphertext : byte[] |
+| BadMacUse.java:100:39:100:48 | ciphertext : byte[] | semmle.label | ciphertext : byte[] |
+| BadMacUse.java:108:39:108:47 | plaintext : byte[] | semmle.label | plaintext : byte[] |
+| BadMacUse.java:118:52:118:60 | plaintext : byte[] | semmle.label | plaintext : byte[] |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] | semmle.label | ciphertext : byte[] |
+| BadMacUse.java:152:42:152:51 | ciphertext | semmle.label | ciphertext |
+subpaths
+testFailures
+| BadMacUse.java:50:56:50:65 | // $Source | Missing result: Source |
+| BadMacUse.java:63:118:63:127 | // $Source | Missing result: Source |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | Unexpected result: Source |
+| BadMacUse.java:146:95:146:104 | // $Source | Missing result: Source |
--- a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.qlref
+++ b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.qlref
@@ -0,0 +1,4 @@
+query: experimental/quantum/Examples/BadMacOrderDecryptThenMac.ql
+postprocess:
+  - utils/test/PrettyPrintModels.ql
+  - utils/test/InlineExpectationsTestQuery.ql
--- a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptToMac.expected
+++ b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptToMac.expected
@@ -34,3 +34,4 @@ testFailures
 | BadMacUse.java:63:118:63:127 | // $Source | Missing result: Source |
 | BadMacUse.java:92:16:92:36 | doFinal(...) : byte[] | Unexpected result: Source |
 | BadMacUse.java:124:42:124:51 | ciphertext | Unexpected result: Alert |
+| BadMacUse.java:146:95:146:104 | // $Source | Missing result: Source |
--- a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderMacOnEncryptPlaintext.expected
+++ b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderMacOnEncryptPlaintext.expected
@@ -1,14 +1,51 @@
 #select
 | BadMacUse.java:76:44:76:52 | plaintext | BadMacUse.java:63:82:63:97 | plaintext : byte[] | BadMacUse.java:76:44:76:52 | plaintext | Incorrect MAC usage: Encryption plaintext also used for MAC. Flow shows plaintext to final use through intermediate mac or encryption operation here $@ | BadMacUse.java:71:42:71:50 | plaintext | plaintext |
+| BadMacUse.java:152:42:152:51 | ciphertext | BadMacUse.java:139:79:139:90 | input : byte[] | BadMacUse.java:152:42:152:51 | ciphertext | Incorrect MAC usage: Encryption plaintext also used for MAC. Flow shows plaintext to final use through intermediate mac or encryption operation here $@ | BadMacUse.java:92:31:92:35 | bytes | bytes |
 edges
 | BadMacUse.java:63:82:63:97 | plaintext : byte[] | BadMacUse.java:71:42:71:50 | plaintext : byte[] | provenance |  |
 | BadMacUse.java:71:42:71:50 | plaintext : byte[] | BadMacUse.java:71:42:71:50 | plaintext : byte[] | provenance | Config |
 | BadMacUse.java:71:42:71:50 | plaintext : byte[] | BadMacUse.java:76:44:76:52 | plaintext | provenance |  |
+| BadMacUse.java:84:42:84:53 | bytes : byte[] | BadMacUse.java:92:31:92:35 | bytes : byte[] | provenance |  |
+| BadMacUse.java:84:42:84:53 | bytes : byte[] [[]] : Object | BadMacUse.java:92:31:92:35 | bytes : byte[] [[]] : Object | provenance |  |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | BadMacUse.java:146:48:146:57 | ciphertext : byte[] | provenance | Config |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] [[]] : Object | BadMacUse.java:146:48:146:57 | ciphertext : byte[] | provenance | Config |
+| BadMacUse.java:99:39:99:55 | ciphertext : byte[] [[]] : Object | BadMacUse.java:100:39:100:48 | ciphertext : byte[] [[]] : Object | provenance |  |
+| BadMacUse.java:100:39:100:48 | ciphertext : byte[] [[]] : Object | BadMacUse.java:84:42:84:53 | bytes : byte[] [[]] : Object | provenance |  |
+| BadMacUse.java:107:39:107:54 | plaintext : byte[] | BadMacUse.java:108:39:108:47 | plaintext : byte[] | provenance |  |
+| BadMacUse.java:108:39:108:47 | plaintext : byte[] | BadMacUse.java:84:42:84:53 | bytes : byte[] | provenance |  |
+| BadMacUse.java:114:92:114:107 | plaintext : byte[] | BadMacUse.java:118:52:118:60 | plaintext : byte[] | provenance |  |
+| BadMacUse.java:118:52:118:60 | plaintext : byte[] | BadMacUse.java:84:42:84:53 | bytes : byte[] | provenance |  |
+| BadMacUse.java:139:79:139:90 | input : byte[] | BadMacUse.java:142:48:142:52 | input : byte[] | provenance |  |
+| BadMacUse.java:142:29:142:82 | copyOfRange(...) : byte[] [[]] : Object | BadMacUse.java:146:48:146:57 | ciphertext : byte[] [[]] : Object | provenance |  |
+| BadMacUse.java:142:48:142:52 | input : byte[] | BadMacUse.java:142:29:142:82 | copyOfRange(...) : byte[] [[]] : Object | provenance | MaD:1 |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] | BadMacUse.java:152:42:152:51 | ciphertext | provenance |  |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] [[]] : Object | BadMacUse.java:99:39:99:55 | ciphertext : byte[] [[]] : Object | provenance |  |
+models
+| 1 | Summary: java.util; Arrays; false; copyOfRange; ; ; Argument[0].ArrayElement; ReturnValue.ArrayElement; value; manual |
 nodes
 | BadMacUse.java:63:82:63:97 | plaintext : byte[] | semmle.label | plaintext : byte[] |
 | BadMacUse.java:71:42:71:50 | plaintext : byte[] | semmle.label | plaintext : byte[] |
 | BadMacUse.java:71:42:71:50 | plaintext : byte[] | semmle.label | plaintext : byte[] |
 | BadMacUse.java:76:44:76:52 | plaintext | semmle.label | plaintext |
+| BadMacUse.java:84:42:84:53 | bytes : byte[] | semmle.label | bytes : byte[] |
+| BadMacUse.java:84:42:84:53 | bytes : byte[] [[]] : Object | semmle.label | bytes : byte[] [[]] : Object |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] | semmle.label | bytes : byte[] |
+| BadMacUse.java:92:31:92:35 | bytes : byte[] [[]] : Object | semmle.label | bytes : byte[] [[]] : Object |
+| BadMacUse.java:99:39:99:55 | ciphertext : byte[] [[]] : Object | semmle.label | ciphertext : byte[] [[]] : Object |
+| BadMacUse.java:100:39:100:48 | ciphertext : byte[] [[]] : Object | semmle.label | ciphertext : byte[] [[]] : Object |
+| BadMacUse.java:107:39:107:54 | plaintext : byte[] | semmle.label | plaintext : byte[] |
+| BadMacUse.java:108:39:108:47 | plaintext : byte[] | semmle.label | plaintext : byte[] |
+| BadMacUse.java:114:92:114:107 | plaintext : byte[] | semmle.label | plaintext : byte[] |
+| BadMacUse.java:118:52:118:60 | plaintext : byte[] | semmle.label | plaintext : byte[] |
+| BadMacUse.java:139:79:139:90 | input : byte[] | semmle.label | input : byte[] |
+| BadMacUse.java:142:29:142:82 | copyOfRange(...) : byte[] [[]] : Object | semmle.label | copyOfRange(...) : byte[] [[]] : Object |
+| BadMacUse.java:142:48:142:52 | input : byte[] | semmle.label | input : byte[] |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] | semmle.label | ciphertext : byte[] |
+| BadMacUse.java:146:48:146:57 | ciphertext : byte[] [[]] : Object | semmle.label | ciphertext : byte[] [[]] : Object |
+| BadMacUse.java:152:42:152:51 | ciphertext | semmle.label | ciphertext |
 subpaths
 testFailures
 | BadMacUse.java:50:56:50:65 | // $Source | Missing result: Source |
+| BadMacUse.java:139:79:139:90 | input : byte[] | Unexpected result: Source |
+| BadMacUse.java:146:95:146:104 | // $Source | Missing result: Source |
+| BadMacUse.java:152:42:152:51 | ciphertext | Unexpected result: Alert |
--- a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacUse.java
+++ b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacUse.java
@@ -53,7 +53,7 @@ class BadMacUse {
        SecretKey macKey = new SecretKeySpec(macKeyBytes, "HmacSHA256");
        Mac mac = Mac.getInstance("HmacSHA256");
        mac.init(macKey);
-        byte[] computedMac = mac.doFinal(plaintext); // $Alert[java/quantum/examples/bad-mac-order-decrypt-to-mac]
+        byte[] computedMac = mac.doFinal(plaintext); // $Alert[java/quantum/examples/bad-mac-order-decrypt-to-mac] 

        if (!MessageDigest.isEqual(receivedMac, computedMac)) {
            throw new SecurityException("MAC verification failed");
@@ -129,4 +129,30 @@ class BadMacUse {
        System.arraycopy(computedMac, 0, output, ciphertext.length, computedMac.length);
        return output;
    }
+
+
+    /**
+     * Correct inputs to a decrypt and MAC operation, but the ordering is unsafe. 
+     * The function decrypts THEN computes the MAC on the plaintext.
+     * It should have the MAC computed on the ciphertext first.
+     */
+    public void decryptThenMac(byte[] encryptionKeyBytes, byte[] macKeyBytes, byte[] input) throws Exception {
+        // Split input into ciphertext and MAC
+        int macLength = 32; // HMAC-SHA256 output length
+        byte[] ciphertext = Arrays.copyOfRange(input, 0, input.length - macLength);
+        byte[] receivedMac = Arrays.copyOfRange(input, input.length - macLength, input.length);
+
+        // Decrypt first (unsafe)
+        byte[] plaintext = decryptUsingWrapper(ciphertext, encryptionKeyBytes, new byte[16]); // $Source
+
+        // Now verify MAC (too late)
+        SecretKey macKey = new SecretKeySpec(macKeyBytes, "HmacSHA256");
+        Mac mac = Mac.getInstance("HmacSHA256");
+        mac.init(macKey);
+        byte[] computedMac = mac.doFinal(ciphertext); // $Alert[java/quantum/examples/bad-mac-order-decrypt-then-mac], False positive for Plaintext reuse
+
+        if (!MessageDigest.isEqual(receivedMac, computedMac)) {
+            throw new SecurityException("MAC verification failed");
+        }
+    }
 }