Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
c5cf0ff
added java cryptographic check queries
unprovable Oct 1, 2025
f38ab45
removed all @security.severity ratings to keep the main impartial
unprovable Oct 1, 2025
bba541c
Merge remote-tracking branch 'upstream/java-crypto-check' into santan…
bdrodes Oct 8, 2025
cf88e3f
Crypto: Standardize naming where use of "family" and "type" have been…
bdrodes Oct 8, 2025
1b1b333
Crypto: Modify suggested queries per misc. side conversations on stan…
bdrodes Oct 8, 2025
143be8c
Crypto: Remove redundant queries.
bdrodes Oct 8, 2025
bd34b6c
Crypto: Removing JCA model of random, need to reassess this as this i…
bdrodes Oct 8, 2025
83ff70b
Crypto: Adding tests for insecure iv or nonce. Updating generic liter…
bdrodes Oct 8, 2025
8e10e19
Crypto: Adding query for unknown IV initialization.
bdrodes Oct 8, 2025
75b5a9f
Crypto: Update general regression test results to account for removal…
bdrodes Oct 8, 2025
11e8139
Crypto: Updated default flows to use taint tracking (this is needed t…
bdrodes Oct 8, 2025
7a57496
Crypto: Missing test update.
bdrodes Oct 8, 2025
f524de4
Crypto: Updating insecure iv/nonce to consider if an operation is kno…
bdrodes Oct 8, 2025
fdba3ac
Crypto: Fix QL-for-QL alert and auto-format
nicolaswill Oct 9, 2025
c6cc4ff
Crypto: Minor fixes to WeakBlockModes, WeakHash to consider SHA3 ok, …
bdrodes Oct 9, 2025
3dedda4
Merge branch 'santander-java-crypto-check' of https://github.com/bdro…
bdrodes Oct 9, 2025
deb4373
Crypto: Minor fixes to WeakSymmetricCipher, change to a singular name…
bdrodes Oct 9, 2025
fba8087
Crypto: Example query reorg - moving queries of this PR into 'example…
bdrodes Oct 9, 2025
758759a
Crypto: Reused nonce query updates and test updates to address false …
bdrodes Oct 10, 2025
3667365
Crypto: Weak asymmetric key gen size fixes and test.
bdrodes Oct 10, 2025
ffd191d
Crypto: missing new endpoint to get the creating operation for a key …
bdrodes Oct 10, 2025
d68f3cf
Crypto: InsecureIVorNonceSource now ignored null to avoid being too n…
bdrodes Oct 10, 2025
e76ced1
Crypto: Updating weak asymmetric key gen to include key exchange.
bdrodes Oct 10, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ class KnownOpenSslEllipticCurveConstantAlgorithmInstance extends OpenSslAlgorith
result = this.(Call).getTarget().getName()
}

override Crypto::EllipticCurveFamilyType getEllipticCurveFamilyType() {
override Crypto::EllipticCurveType getEllipticCurveType() {
if
Crypto::ellipticCurveNameToKnownKeySizeAndFamilyMapping(this.getParsedEllipticCurveName(), _,
_)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ class KnownOpenSslHashConstantAlgorithmInstance extends OpenSslAlgorithmInstance

override OpenSslAlgorithmValueConsumer getAvc() { result = getterCall }

override Crypto::THashType getHashFamily() {
override Crypto::THashType getHashType() {
knownOpenSslConstantToHashFamilyType(this, result)
or
not knownOpenSslConstantToHashFamilyType(this, _) and result = Crypto::OtherHashType()
Expand Down
33 changes: 11 additions & 22 deletions java/ql/lib/experimental/quantum/JCA.qll
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,8 @@ module JCAModel {
predicate signature_names(string name) {
name.toUpperCase().splitAt("WITH", 1).matches(["RSA%", "ECDSA%", "DSA%"])
or
name.toUpperCase().matches(["RSASSA-PSS", "ED25519", "ED448", "EDDSA", "ML-DSA%", "HSS/LMS"])
name.toUpperCase()
.matches(["RSASSA-PSS", "ED25519", "ED448", "EDDSA", "ML-DSA%", "HSS/LMS", "DSA"])
}

bindingset[name]
Expand Down Expand Up @@ -257,6 +258,8 @@ module JCAModel {
name.toUpperCase().matches("ML-DSA%") and type = KeyOpAlg::TSignature(KeyOpAlg::DSA())
or
name.toUpperCase() = "HSS/LMS" and type = KeyOpAlg::TSignature(KeyOpAlg::HSS_LMS())
or
name.toUpperCase() = "DSA" and type = KeyOpAlg::TSignature(KeyOpAlg::DSA())
}

bindingset[name]
Expand Down Expand Up @@ -426,7 +429,7 @@ module JCAModel {

override string getRawHashAlgorithmName() { result = super.getPadding() }

override Crypto::THashType getHashFamily() { result = hash_name_to_type_known(hashName, _) }
override Crypto::THashType getHashType() { result = hash_name_to_type_known(hashName, _) }

override int getFixedDigestLength() { exists(hash_name_to_type_known(hashName, result)) }
}
Expand Down Expand Up @@ -859,7 +862,7 @@ module JCAModel {

override string getRawHashAlgorithmName() { result = super.getValue() }

override Crypto::THashType getHashFamily() {
override Crypto::THashType getHashType() {
result = hash_name_to_type_known(this.getRawHashAlgorithmName(), _)
}

Expand Down Expand Up @@ -1019,7 +1022,8 @@ module JCAModel {
}

class KeyGenerationAlgorithmValueConsumer extends CipherAlgorithmValueConsumer,
KeyAgreementAlgorithmValueConsumer, EllipticCurveAlgorithmValueConsumer instanceof Expr
KeyAgreementAlgorithmValueConsumer, EllipticCurveAlgorithmValueConsumer,
SignatureAlgorithmValueConsumer instanceof Expr
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is instanceof Expr necessary here?

{
KeyGeneratorGetInstanceCall instantiationCall;

Expand Down Expand Up @@ -1095,21 +1099,6 @@ module JCAModel {
}
}

/**
* An instance of `java.security.SecureRandom.nextBytes(byte[])` call.
* This is already generally modeled for Java in CodeQL, but
* we model it again as part of the crypto API model to have a cohesive model.
*/
class JavaSecuritySecureRandom extends Crypto::RandomNumberGenerationInstance instanceof Call {
JavaSecuritySecureRandom() {
this.getCallee().hasQualifiedName("java.security", "SecureRandom", "nextBytes")
}

override Crypto::DataFlowNode getOutputNode() { result.asExpr() = this.(Call).getArgument(0) }

override string getGeneratorName() { result = this.(Call).getCallee().getName() }
}

class KeyGeneratorGenerateCall extends Crypto::KeyGenerationOperationInstance instanceof MethodCall
{
Crypto::KeyArtifactType type;
Expand Down Expand Up @@ -1302,7 +1291,7 @@ module JCAModel {

override string getRawHashAlgorithmName() { result = this.(StringLiteral).getValue() }

override Crypto::THashType getHashFamily() { result = hash_name_to_type_known(hashName, _) }
override Crypto::THashType getHashType() { result = hash_name_to_type_known(hashName, _) }

override int getFixedDigestLength() { exists(hash_name_to_type_known(hashName, result)) }
}
Expand Down Expand Up @@ -1770,7 +1759,7 @@ module JCAModel {

override string getRawHashAlgorithmName() { result = this.(StringLiteral).getValue() }

override Crypto::THashType getHashFamily() { result = hashType }
override Crypto::THashType getHashType() { result = hashType }

override int getFixedDigestLength() { result = digestLength }
}
Expand Down Expand Up @@ -1905,7 +1894,7 @@ module JCAModel {

override string getRawEllipticCurveName() { result = super.getValue() }

override Crypto::EllipticCurveFamilyType getEllipticCurveFamilyType() {
override Crypto::EllipticCurveType getEllipticCurveType() {
if
Crypto::ellipticCurveNameToKnownKeySizeAndFamilyMapping(this.getRawEllipticCurveName(), _, _)
then
Expand Down
21 changes: 18 additions & 3 deletions java/ql/lib/experimental/quantum/Language.qll
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,9 @@ private class GenericRemoteDataSource extends Crypto::GenericRemoteDataSource {
override string getAdditionalDescription() { result = this.toString() }
}

private class ConstantDataSource extends Crypto::GenericConstantSourceInstance instanceof Literal {
ConstantDataSource() {
private class ConstantDataSourceLiteral extends Crypto::GenericConstantSourceInstance instanceof Literal
{
ConstantDataSourceLiteral() {
// TODO: this is an API specific workaround for JCA, as 'EC' is a constant that may be used
// where typical algorithms are specified, but EC specifically means set up a
// default curve container, that will later be specified explicitly (or if not a default)
Expand All @@ -112,6 +113,20 @@ private class ConstantDataSource extends Crypto::GenericConstantSourceInstance i
override string getAdditionalDescription() { result = this.toString() }
}

private class ConstantDataSourceArrayInitializer extends Crypto::GenericConstantSourceInstance instanceof ArrayInit
{
ConstantDataSourceArrayInitializer() { this.getAnInit() instanceof Literal }

override DataFlow::Node getOutputNode() { result.asExpr() = this }

override predicate flowsTo(Crypto::FlowAwareElement other) {
// TODO: separate config to avoid blowing up data-flow analysis
GenericDataSourceFlow::flow(this.getOutputNode(), other.getInputNode())
}

override string getAdditionalDescription() { result = this.toString() }
}

/**
* An instance of random number generation, modeled as the expression
* tied to an output node (i.e., the result of the source of randomness)
Expand Down Expand Up @@ -215,7 +230,7 @@ module ArtifactFlowConfig implements DataFlow::ConfigSig {

module GenericDataSourceFlow = TaintTracking::Global<GenericDataSourceFlowConfig>;

module ArtifactFlow = DataFlow::Global<ArtifactFlowConfig>;
module ArtifactFlow = TaintTracking::Global<ArtifactFlowConfig>;

// Import library-specific modeling
import JCA

This file was deleted.

17 changes: 0 additions & 17 deletions java/ql/src/experimental/quantum/Analysis/ReusedNonce.ql

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import experimental.quantum.Language
* NOTE: TODO: need to handle call by refernece for now. Need to re-evaluate (see notes below)
* Such functions may be 'wrappers' for some derived value.
*/
private module WrapperConfig implements DataFlow::ConfigSig {
private module ArtifactGeneratingWrapperConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
source.asExpr() instanceof Call and
// not handling references yet, I think we want to flat say references are only ok
Expand All @@ -28,25 +28,41 @@ private module WrapperConfig implements DataFlow::ConfigSig {
predicate isSink(DataFlow::Node sink) { sink.asExpr() = any(Crypto::ArtifactNode i).asElement() }
}

module WrapperFlow = DataFlow::Global<WrapperConfig>;
module ArtifactGeneratingWrapperFlow = TaintTracking::Global<ArtifactGeneratingWrapperConfig>;

/**
* Using a set approach to determine if reuse of an artifact exists.
* This predicate produces a set of 'wrappers' that flow to the artifact node.
* This set can be compared with the set to another artifact node to determine if they are the same.
*/
private DataFlow::Node getWrapperSet(Crypto::NonceArtifactNode a) {
WrapperFlow::flow(result, DataFlow::exprNode(a.asElement()))
private DataFlow::Node getGeneratingWrapperSet(Crypto::NonceArtifactNode a) {
ArtifactGeneratingWrapperFlow::flow(result, DataFlow::exprNode(a.asElement()))
or
result.asExpr() = a.getSourceElement()
}

private predicate ancestorOfArtifact(
Crypto::ArtifactNode a, Callable enclosingCallable, ControlFlow::Node midOrTarget
) {
a.asElement().(Expr).getEnclosingCallable() = enclosingCallable and
(
midOrTarget.asExpr() = a.asElement() or
midOrTarget.asExpr().(Call).getCallee().calls*(a.asElement().(Expr).getEnclosingCallable())
)
}

/**
* Two different artifact nodes are considered reuse if any of the following conditions are met:
* 1. The source for artifact `a` and artifact `b` are the same and the source is a literal.
* 2. The source for artifact `a` and artifact `b` are not the same and the source is a literal of the same value.
* 3. For all 'wrappers' that return the source of artifact `a`, and that wrapper also exists for artifact `b`.
* 4. For all 'wrappers' that return the source of artifact `b`, and that wrapper also exists for artifact `a`.
* 3. For all 'wrappers' that return the source of artifact `a`, and each wrapper also exists for artifact `b`.
* 4. For all 'wrappers' that return the source of artifact `b`, and each wrapper also exists for artifact `a`.
*
* The above conditions determine that the use of the IV is from the same source, but the use may
* be on separate code paths that do not occur sequentially. We must therefore also find a common callable ancestor
* for both uses, and in that ancestor, there must be control flow from the call or use of one to the call or use of the other.
* Note that if no shared ancestor callable exists, it means the flow is more nuanced and ignore the shared ancestor
* use flow.
*/
predicate isArtifactReuse(Crypto::ArtifactNode a, Crypto::ArtifactNode b) {
a != b and
Expand All @@ -55,12 +71,32 @@ predicate isArtifactReuse(Crypto::ArtifactNode a, Crypto::ArtifactNode b) {
or
a.getSourceElement().(Literal).getValue() = b.getSourceElement().(Literal).getValue()
or
forex(DataFlow::Node e | e = getWrapperSet(a) |
exists(DataFlow::Node e2 | e2 = getWrapperSet(b) | e = e2)
forex(DataFlow::Node e | e = getGeneratingWrapperSet(a) |
exists(DataFlow::Node e2 | e2 = getGeneratingWrapperSet(b) | e = e2)
)
or
forex(DataFlow::Node e | e = getWrapperSet(b) |
exists(DataFlow::Node e2 | e2 = getWrapperSet(a) | e = e2)
forex(DataFlow::Node e | e = getGeneratingWrapperSet(b) |
exists(DataFlow::Node e2 | e2 = getGeneratingWrapperSet(a) | e = e2)
)
) and
// If there is a common parent, there is control flow between the two uses in the parent
// TODO: this logic needs to be examined/revisited to ensure it is correct
(
exists(Callable commonParent |
ancestorOfArtifact(a, commonParent, _) and
ancestorOfArtifact(b, commonParent, _)
)
implies
exists(Callable commonParent, ControlFlow::Node aMid, ControlFlow::Node bMid |
ancestorOfArtifact(a, commonParent, aMid) and
ancestorOfArtifact(b, commonParent, bMid) and
a instanceof Crypto::NonceArtifactNode and
b instanceof Crypto::NonceArtifactNode and
(
aMid.getASuccessor*() = bMid
or
bMid.getASuccessor*() = aMid
)
)
)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
/**
* @name Insecure nonce/iv (static value or weak random source)
* @id java/quantum/insecure-iv-or-nonce
* @description A nonce/iv is generated from a source that is not secure. This can lead to
* vulnerabilities such as replay attacks or key recovery. Insecure generation
* is any static nonce, or any known insecure source for a nonce/iv if
* the value is used for an encryption operation (decryption operations are ignored
* as the nonce/iv would be provided alongside the ciphertext).
* @kind problem
* @problem.severity error
* @precision high
* @tags quantum
* experimental
*/

import experimental.quantum.Language

from Crypto::NonceArtifactNode nonce, Crypto::NodeBase src, Crypto::NodeBase op, string msg
where
nonce.getSourceNode() = src and
// NOTE: null nonces should be handled seaparately, often used for default values prior to initialization
// failure to initialize should, in practice, lead to a NullPointerException, which is a separate concern
// however there may be APIs where NULL uses a default nonce or action.
not src.asElement() instanceof NullLiteral and
(
// Case 1: Any constant nonce/iv is bad, regardless of how it is used
src.asElement() instanceof Crypto::GenericConstantSourceInstance and
op = nonce and // binding op by not using it
msg = "Nonce or IV uses constant source $@"
or
// Case 2: The nonce has a non-random source and there is no known operation for the nonce
// assume it is used for encryption
not src.asElement() instanceof SecureRandomnessInstance and
not src.asElement() instanceof Crypto::GenericConstantSourceInstance and
not exists(Crypto::CipherOperationNode o | o.getANonce() = nonce) and
op = nonce and // binding op, but not using it
msg =
"Nonce or IV uses insecure source $@ with no observed nonce usage (assuming could be for encryption)."
or
// Case 3: The nonce has a non-random source and is used in an encryption operation
not src.asElement() instanceof SecureRandomnessInstance and
not src.asElement() instanceof Crypto::GenericConstantSourceInstance and
op.(Crypto::CipherOperationNode).getANonce() = nonce and
(
op.(Crypto::CipherOperationNode).getKeyOperationSubtype() instanceof Crypto::TEncryptMode
or
op.(Crypto::CipherOperationNode).getKeyOperationSubtype() instanceof Crypto::TWrapMode
) and
msg = "Nonce or IV uses insecure source $@ at encryption operation $@"
)
select nonce, msg, src, src.toString(), op, op.toString()
25 changes: 25 additions & 0 deletions java/ql/src/experimental/quantum/Examples/NonAESGCMCipher.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
/**
* @name Cipher not AES-GCM mode
* @id java/quantum/non-aes-gcm
* @description An AES cipher is in use without GCM
* @kind problem
* @problem.severity error
* @precision high
* @tags quantum
* experimental
*/

import experimental.quantum.Language

class NonAESGCMAlgorithmNode extends Crypto::KeyOperationAlgorithmNode {
NonAESGCMAlgorithmNode() {
this.getAlgorithmType() = Crypto::KeyOpAlg::TSymmetricCipher(Crypto::KeyOpAlg::AES()) and
this.getModeOfOperation().getModeType() != Crypto::KeyOpAlg::GCM()
}
}

from Crypto::KeyOperationNode op, Crypto::KeyOperationOutputNode codeNode
where
op.getAKnownAlgorithm() instanceof NonAESGCMAlgorithmNode and
codeNode = op.getAnOutputArtifact()
select op, "Non-AES-GCM instance."
Loading
Loading