diff --git 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 index 58b6b5766f2f..9c967eb3d989 100644 --- 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 diff --git a/java/ql/src/experimental/quantum/Examples/BadMacOrder.qll b/java/ql/src/experimental/quantum/Examples/BadMacOrder.qll index 645a092d57ca..6d944661621b 100644 --- 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; + +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; + +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; +module ArgToEncryptOrMacFlow = TaintTracking::Global; /** * 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::Option; + class FlowState = Option::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; + +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; diff --git a/java/ql/src/experimental/quantum/Examples/BadMacOrderDecryptThenMac.ql b/java/ql/src/experimental/quantum/Examples/BadMacOrderDecryptThenMac.ql new file mode 100644 index 000000000000..21b0be29ed50 --- /dev/null +++ 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." diff --git a/java/ql/src/experimental/quantum/Examples/BadMacOrderMacOnEncryptPlaintext.ql b/java/ql/src/experimental/quantum/Examples/BadMacOrderMacOnEncryptPlaintext.ql index b3ff84b091ac..7644167c589a 100644 --- 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 $@", diff --git a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.expected b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.expected new file mode 100644 index 000000000000..ba74f3dffce5 --- /dev/null +++ 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 | diff --git a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.qlref b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptThenMac.qlref new file mode 100644 index 000000000000..811a6cbac130 --- /dev/null +++ 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 \ No newline at end of file diff --git a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptToMac.expected b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderDecryptToMac.expected index 2a3c1d533dfb..f73f0f25e0aa 100644 --- 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 | diff --git a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderMacOnEncryptPlaintext.expected b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacOrderMacOnEncryptPlaintext.expected index 70733bbf8d35..ea4273613611 100644 --- 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 | diff --git a/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacUse.java b/java/ql/test/experimental/query-tests/quantum/examples/BadMacUse/BadMacUse.java index 597c2a106d82..5c442d4bca76 100644 --- 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 @@ public void BadDecryptThenMacOnPlaintextVerify(byte[] encryptionKeyBytes, byte[] 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 @@ public byte[] falsePositiveDecryptToMac(byte[] encryptionKeyBytes, byte[] macKey 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"); + } + } }