Merge pull request #10 from nicolaswill/brodes/key_agreement

Initial progress on key agreement.
This commit is contained in:
Nicolas Will
2025-04-30 16:31:42 +02:00
committed by GitHub
30 changed files with 2147 additions and 1199 deletions

View File

@@ -112,7 +112,7 @@ module ArtifactUniversalFlowConfig implements DataFlow::ConfigSig {
module ArtifactUniversalFlow = DataFlow::Global<ArtifactUniversalFlowConfig>;
abstract class CipherOutputArtifact extends Crypto::CipherOutputArtifactInstance {
abstract class CipherOutputArtifact extends Crypto::KeyOperationOutputArtifactInstance {
override predicate flowsTo(Crypto::FlowAwareElement other) {
ArtifactUniversalFlow::flow(this.getOutputNode(), other.getInputNode())
}

File diff suppressed because it is too large Load Diff

View File

@@ -38,7 +38,7 @@ module CryptoInput implements InputSig<Language::Location> {
predicate artifactOutputFlowsToGenericInput(
DataFlow::Node artifactOutput, DataFlow::Node otherInput
) {
ArtifactUniversalFlow::flow(artifactOutput, otherInput)
ArtifactFlow::flow(artifactOutput, otherInput)
}
}
@@ -60,7 +60,7 @@ class GenericUnreferencedParameterSource extends Crypto::GenericUnreferencedPara
}
override predicate flowsTo(Crypto::FlowAwareElement other) {
GenericDataSourceUniversalFlow::flow(this.getOutputNode(), other.getInputNode())
GenericDataSourceFlow::flow(this.getOutputNode(), other.getInputNode())
}
override DataFlow::Node getOutputNode() { result.asParameter() = this }
@@ -76,7 +76,7 @@ class GenericLocalDataSource extends Crypto::GenericLocalDataSource {
override DataFlow::Node getOutputNode() { result.asExpr() = this }
override predicate flowsTo(Crypto::FlowAwareElement other) {
GenericDataSourceUniversalFlow::flow(this.getOutputNode(), other.getInputNode())
GenericDataSourceFlow::flow(this.getOutputNode(), other.getInputNode())
}
override string getAdditionalDescription() { result = this.toString() }
@@ -88,7 +88,7 @@ class GenericRemoteDataSource extends Crypto::GenericRemoteDataSource {
override DataFlow::Node getOutputNode() { result.asExpr() = this }
override predicate flowsTo(Crypto::FlowAwareElement other) {
GenericDataSourceUniversalFlow::flow(this.getOutputNode(), other.getInputNode())
GenericDataSourceFlow::flow(this.getOutputNode(), other.getInputNode())
}
override string getAdditionalDescription() { result = this.toString() }
@@ -100,14 +100,14 @@ class ConstantDataSource extends Crypto::GenericConstantSourceInstance instanceo
// 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)
// curve is used.
this = any(Literal l | l.getValue() != "EC")
this.getValue() != "EC"
}
override DataFlow::Node getOutputNode() { result.asExpr() = this }
override predicate flowsTo(Crypto::FlowAwareElement other) {
// TODO: separate config to avoid blowing up data-flow analysis
GenericDataSourceUniversalFlow::flow(this.getOutputNode(), other.getInputNode())
GenericDataSourceFlow::flow(this.getOutputNode(), other.getInputNode())
}
override string getAdditionalDescription() { result = this.toString() }
@@ -122,15 +122,24 @@ abstract class RandomnessInstance extends Crypto::RandomNumberGenerationInstance
}
class SecureRandomnessInstance extends RandomnessInstance {
RandomDataSource source;
SecureRandomnessInstance() {
exists(RandomDataSource s | this = s.getOutput() |
s.getSourceOfRandomness() instanceof SecureRandomNumberGenerator
)
this = source.getOutput() and
source.getSourceOfRandomness() instanceof SecureRandomNumberGenerator
}
override string getGeneratorName() { result = source.getSourceOfRandomness().getQualifiedName() }
}
class InsecureRandomnessInstance extends RandomnessInstance {
InsecureRandomnessInstance() { exists(InsecureRandomnessSource node | this = node.asExpr()) }
RandomDataSource source;
InsecureRandomnessInstance() {
any(InsecureRandomnessSource src).asExpr() = this and source.getOutput() = this
}
override string getGeneratorName() { result = source.getSourceOfRandomness().getQualifiedName() }
}
/**
@@ -142,12 +151,12 @@ abstract class AdditionalFlowInputStep extends DataFlow::Node {
final DataFlow::Node getInput() { result = this }
}
module ArtifactUniversalFlow = DataFlow::Global<ArtifactUniversalFlowConfig>;
module ArtifactFlow = DataFlow::Global<ArtifactFlowConfig>;
/**
* Generic data source to node input configuration
*/
module GenericDataSourceUniversalFlowConfig implements DataFlow::ConfigSig {
module GenericDataSourceFlowConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
source = any(Crypto::GenericSourceInstance i).getOutputNode()
}
@@ -175,7 +184,7 @@ module GenericDataSourceUniversalFlowConfig implements DataFlow::ConfigSig {
}
}
module ArtifactUniversalFlowConfig implements DataFlow::ConfigSig {
module ArtifactFlowConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
source = any(Crypto::ArtifactInstance artifact).getOutputNode()
}
@@ -194,10 +203,16 @@ module ArtifactUniversalFlowConfig implements DataFlow::ConfigSig {
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 GenericDataSourceUniversalFlow = TaintTracking::Global<GenericDataSourceUniversalFlowConfig>;
module GenericDataSourceFlow = TaintTracking::Global<GenericDataSourceFlowConfig>;
// Import library-specific modeling
import JCA

View File

@@ -0,0 +1,20 @@
/**
* @name Insecure nonce at a cipher operation
* @id java/insecure-nonce
* @kind problem
* @problem.severity error
* @precision high
* @description A nonce is generated from a source that is not secure. This can lead to
* vulnerabilities such as replay attacks or key recovery.
*/
import experimental.Quantum.Language
predicate isInsecureNonceSource(Crypto::NonceArtifactNode n, Crypto::NodeBase src) {
src = n.getSourceNode() and
not src.asElement() instanceof SecureRandomnessInstance
}
from Crypto::KeyOperationNode op, Crypto::NodeBase src
where isInsecureNonceSource(op.getANonce(), src)
select op, "Operation uses insecure nonce source $@", src, src.toString()

View File

@@ -7,18 +7,17 @@
import experimental.Quantum.Language
from
Crypto::NonceArtifactNode n, Crypto::CipherOperationNode op, Crypto::FlowAwareElement src,
string msg
Crypto::NonceArtifactNode n, Crypto::KeyOperationNode op, Crypto::FlowAwareElement src, string msg
where
op.getANonce() = n and
// Only encryption mode is relevant for insecure nonces, consder any 'unknown' subtype
// as possibly encryption.
(
op.getCipherOperationSubtype() instanceof Crypto::EncryptionSubtype
op.getKeyOperationSubtype() instanceof Crypto::EncryptionSubtype
or
op.getCipherOperationSubtype() instanceof Crypto::WrapSubtype
op.getKeyOperationSubtype() instanceof Crypto::WrapSubtype
or
op.getCipherOperationSubtype() instanceof Crypto::UnwrapSubtype
op.getKeyOperationSubtype() instanceof Crypto::UnwrapSubtype
) and
(
// Known sources cases that are not secure

View File

@@ -0,0 +1,70 @@
import java
import semmle.code.java.dataflow.DataFlow
import experimental.Quantum.Language
/**
* Flow from any function that appears to return a value
* to an artifact node.
* 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 {
predicate isSource(DataFlow::Node source) {
exists(Call c |
c = source.asExpr()
// not handling references yet, I think we want to flat say references are only ok
// if I know the source, otherwise, it has to be through an additional flow step, which
// we filter as a source, i.e., references are only allowed as sources only,
// no inferrece? Not sure if that would work
//or
// source.(DataFlow::PostUpdateNode).getPreUpdateNode().asExpr() = c.getAnArgument()
) and
// Filter out sources that are known additional flow steps, as these are likely not the
// kind of wrapper source we are looking for.
not exists(AdditionalFlowInputStep s | s.getOutput() = source)
}
// Flow through additional flow steps
predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
node1.(AdditionalFlowInputStep).getOutput() = node2
}
predicate isSink(DataFlow::Node sink) { sink.asExpr() = any(Crypto::ArtifactNode i).asElement() }
}
module WrapperFlow = DataFlow::Global<WrapperConfig>;
/**
* 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()))
or
result.asExpr() = a.getSourceElement()
}
/**
* 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`.
*/
predicate isArtifactReuse(Crypto::ArtifactNode a, Crypto::ArtifactNode b) {
a != b and
(
a.getSourceElement() = b.getSourceElement() and a.getSourceElement() instanceof Literal
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)
)
or
forex(DataFlow::Node e | e = getWrapperSet(b) |
exists(DataFlow::Node e2 | e2 = getWrapperSet(a) | e = e2)
)
)
}

View File

@@ -0,0 +1,15 @@
/**
* @name Detects known weak KDf iteration counts (less than 100k and the count is statically known)
* @id java/crypto_inventory_filters/known_weak_kdf_iteration_count
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::KeyDerivationOperationNode op, Literal l
where
op.getIterationCount().asElement() = l and
l.getValue().toInt() < 100000
select op, "Key derivation operation configures iteration count below 100k: $@", l,
l.getValue().toString()

View File

@@ -0,0 +1,12 @@
/**
* @name Detects reuse of the same nonce in multiple operations
* @id java/crypto_inventory_filter/nonce_reuse
* @kind problem
*/
import java
import ArtifactReuse
from Crypto::NonceArtifactNode nonce1, Crypto::NonceArtifactNode nonce2
where isArtifactReuse(nonce1, nonce2)
select nonce1, "Reuse with nonce $@", nonce2, nonce2.toString()

View File

@@ -0,0 +1,19 @@
/**
* @name Detects unknown KDf iteration counts
* @id java/crypto_inventory_filters/unknown_kdf_iteration_count
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::KeyDerivationOperationNode op, Element e, string msg
where
e = op.getIterationCount().asElement() and
not e instanceof Literal and
msg = "Key derivation operation with unknown iteration: $@"
or
not exists(op.getIterationCount()) and
e = op.asElement() and
msg = "Key derivation operation with no iteration configuration."
select op, msg, e, e.toString()

View File

@@ -0,0 +1,12 @@
/**
* @name Detects known asymmetric algorithms
* @id java/crypto_inventory_slices/known_asymmetric_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::AlgorithmNode a
where Crypto::isKnownAsymmetricAlgorithm(a)
select a, "Instance of asymmetric algorithm " + a.getAlgorithmName()

View File

@@ -0,0 +1,12 @@
/**
* @name Detects known asymmetric cipher algorithms
* @id java/crypto_inventory_slices/known_symmetric_cipher_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::KeyOperationAlgorithmNode a
where a.getAlgorithmType() instanceof Crypto::KeyOpAlg::AsymmetricCipherAlgorithm
select a, "Instance of asymmetric cipher algorithm " + a.getAlgorithmName()

View File

@@ -0,0 +1,12 @@
/**
* @name Detects operations where the algorithm applied is a known asymmetric algorithms
* @id java/crypto_inventory_slices/known_asymmetric_operation_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::OperationNode op, Crypto::AlgorithmNode a
where a = op.getAKnownAlgorithm() and Crypto::isKnownAsymmetricAlgorithm(a)
select op, "Operation using asymmetric algorithm $@", a, a.getAlgorithmName()

View File

@@ -0,0 +1,15 @@
/**
* @name Detects known cipher algorithms
* @id java/crypto_inventory_slices/known_cipher_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
// TODO: should there be a cipher algorithm node?
from Crypto::KeyOperationAlgorithmNode a
where
a.getAlgorithmType() instanceof Crypto::KeyOpAlg::AsymmetricCipherAlgorithm or
a.getAlgorithmType() instanceof Crypto::KeyOpAlg::SymmetricCipherAlgorithm
select a, "Instance of cipher algorithm " + a.getAlgorithmName()

View File

@@ -0,0 +1,11 @@
/**
* @name Detects known elliptic curve algorithms
* @id java/crypto_inventory_slices/known_elliptic_curve_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::EllipticCurveNode a
select a, "Instance of elliptic curve algorithm " + a.getAlgorithmName()

View File

@@ -0,0 +1,11 @@
/**
* @name Detects algorithms that are known hashing algorithms
* @id java/crypto_inventory_slices/known_hashing_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::HashAlgorithmNode a
select a, "Instance of hashing algorithm " + a.getAlgorithmName()

View File

@@ -0,0 +1,11 @@
/**
* @name Detects uses of hashing operations (operations exlicitly for hashing only, irrespective of the algorithm used)
* @id java/crypto_inventory_slices/known_hashing_operation
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::HashOperationNode op
select op, "Known hashing operation"

View File

@@ -0,0 +1,12 @@
/**
* @name Detects operations where the algorithm applied is a known hashing algorithm
* @id java/crypto_inventory_slices/operation_with_known_hashing_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::OperationNode op, Crypto::HashAlgorithmNode a
where a = op.getAKnownAlgorithm()
select op, "Operation using hashing algorithm $@", a, a.getAlgorithmName()

View File

@@ -0,0 +1,11 @@
/**
* @name Detects known key derivation algorithms
* @id java/crypto_inventory_slices/known_key_derivation_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::KeyDerivationAlgorithmNode alg
select alg, "Known key derivation algorithm " + alg.getAlgorithmName()

View File

@@ -0,0 +1,11 @@
/**
* @name Detects uses of key derivation operations (operations exlicitly for key derivation only, irrespective of the algorithm used)
* @id java/crypto_inventory_slices/known_key_derivation_operation
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::KeyDerivationOperationNode op
select op, "Known key derivation operation"

View File

@@ -0,0 +1,12 @@
/**
* @name Detects operations where the algorithm applied is a known key derivation algorithm
* @id java/crypto_inventory_slices/operation_with_known_key_derivation_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
from Crypto::OperationNode op, Crypto::KeyDerivationAlgorithmNode a
where a = op.getAKnownAlgorithm()
select op, "Operation using key derivation algorithm $@", a, a.getAlgorithmName()

View File

@@ -0,0 +1,16 @@
/**
* @name Detects functions that take in crypto configuration parameters but calls are not detected in source.
* @id java/crypto_inventory_slices/likely_crypto_api_function
* @kind problem
*/
import java
import experimental.Quantum.Language
from Callable f, Parameter p, Crypto::OperationNode op
where
op.asElement().(Expr).getEnclosingCallable() = f and
op.getAnAlgorithmOrGenericSource().asElement() = p
select f,
"Likely crypto API function: Operation $@ configured by parameter $@ with no known configuring call",
op, op.toString(), p, p.toString()

View File

@@ -0,0 +1,22 @@
/**
* @name Detects operations where the algorithm applied is unknown
* @id java/crypto_inventory_slices/unknown_operation_algorithm
* @kind problem
*/
import java
import experimental.Quantum.Language
//TODO: can we have an unknown node concept?
from Crypto::OperationNode op, Element e, string msg
where
not exists(op.getAnAlgorithmOrGenericSource()) and
e = op.asElement() and
msg = "Operation with unconfigured algorithm (no known sources)."
or
exists(Crypto::GenericSourceNode n |
n = op.getAnAlgorithmOrGenericSource() and
e = n.asElement()
) and
msg = "Operation with unknown algorithm source: $@"
select op, msg, e, e.toString()

View File

@@ -1,37 +0,0 @@
/**
* @name Possible Nonce Reuse: Produces false positives if reuse occurs in a source that is a re-entry point.
* @id java/possible-nonce-reuse
* @kind problem
*/
import experimental.Quantum.Language
import semmle.code.java.dataflow.DataFlow
from
Crypto::CipherOperationNode op1, Crypto::CipherOperationNode op2,
Crypto::NonceArtifactNode nonce1, Crypto::NonceArtifactNode nonce2, Crypto::FlowAwareElement src1,
Crypto::FlowAwareElement src2
where
// NOTE: not looking at value of the nonce, if we knew value, it would be insecure (hard coded)
// Instead trying to find nonce sources that trace to multiple operations.
// Only looking for encryption operations, presumably if reuse for decryption either wouldn't be observable
// (the encryption happened else where) or we are able to see the encryption and decryption operation and
// reuse for encryption is the concern)
(
op1.getCipherOperationSubtype() instanceof Crypto::EncryptionSubtype or
op1.getCipherOperationSubtype() instanceof Crypto::WrapSubtype or
op1.getCipherOperationSubtype() instanceof Crypto::UnknownCipherOperationSubtype
) and
(
op2.getCipherOperationSubtype() instanceof Crypto::EncryptionSubtype or
op2.getCipherOperationSubtype() instanceof Crypto::WrapSubtype or
op2.getCipherOperationSubtype() instanceof Crypto::UnknownCipherOperationSubtype
) and
nonce1 = op1.getANonce() and
nonce2 = op2.getANonce() and
op1 != op2 and
nonce1.getSourceElement() = src1 and
nonce2.getSourceElement() = src2 and
src1 = src2
// TODO: need to clarify that a reuse in a non-finalize is ok, need to check if 'finalize' through a modeled predicate
select op1, "Operation has a possible reused nonce with source $@", src1, src1.toString()

View File

@@ -0,0 +1,16 @@
/**
* @name "PQC Test"
*/
import experimental.Quantum.Language
class AESGCMAlgorithmNode extends Crypto::KeyOperationAlgorithmNode {
AESGCMAlgorithmNode() {
this.getAlgorithmType() = Crypto::KeyOpAlg::TSymmetricCipher(Crypto::KeyOpAlg::AES()) and
this.getModeOfOperation().getModeType() = Crypto::GCM()
}
}
from Crypto::KeyOperationNode op, Crypto::NonceArtifactNode nonce
where op.getAKnownAlgorithm() instanceof AESGCMAlgorithmNode and nonce = op.getANonce()
select op, nonce.getSourceNode()

View File

@@ -1,18 +1,18 @@
/**
* @name "PQC Test"
* @name "Key operation slice table demo query"
*/
import experimental.Quantum.Language
from
Crypto::CipherOperationNode op, Crypto::CipherAlgorithmNode a,
Crypto::KeyOperationNode op, Crypto::KeyOperationAlgorithmNode a,
Crypto::ModeOfOperationAlgorithmNode m, Crypto::PaddingAlgorithmNode p,
Crypto::NonceArtifactNode nonce, Crypto::KeyArtifactNode k
where
a = op.getAKnownCipherAlgorithm() and
a = op.getAKnownAlgorithm() and
m = a.getModeOfOperation() and
p = a.getPaddingAlgorithm() and
nonce = op.getANonce() and
k = op.getAKey()
select op, op.getCipherOperationSubtype(), a, a.getRawAlgorithmName(), m, m.getRawAlgorithmName(),
p, p.getRawAlgorithmName(), nonce, k, k.getSourceElement()
select op, op.getKeyOperationSubtype(), a, a.getRawAlgorithmName(), m, m.getRawAlgorithmName(), p,
p.getRawAlgorithmName(), nonce, k

View File

@@ -4,11 +4,11 @@
import experimental.Quantum.Language
from Crypto::CipherOperationNode op, Crypto::CipherAlgorithmNode a, Crypto::KeyArtifactNode k
from Crypto::KeyOperationNode op, Crypto::CipherAlgorithmNode a, Crypto::KeyArtifactNode k
where
a = op.getAKnownCipherAlgorithm() and
k = op.getAKey()
select op, op.getCipherOperationSubtype(), a, a.getRawAlgorithmName(), k, k.getSourceNode()
select op, op.getKeyOperationSubtype(), a, a.getRawAlgorithmName(), k, k.getSourceNode()
/*
* from Crypto::CipherOperationNode op
* where op.getLocation().getFile().getBaseName() = "AsymmetricEncryptionMacHybridCryptosystem.java"

View File

@@ -1,9 +1,9 @@
/**
* @name TestHashOperations
* @name "Hash operation slice table demo query"
*/
import experimental.Quantum.Language
from Crypto::HashOperationNode op, Crypto::HashAlgorithmNode alg
where alg = op.getAKnownHashAlgorithm()
where alg = op.getAKnownAlgorithm()
select op, op.getDigest(), alg, alg.getRawAlgorithmName()

View File

@@ -1,6 +1,7 @@
#!/usr/bin/env python3
import os
import re
import sys
import argparse
import subprocess
@@ -86,6 +87,7 @@ def main():
parser.add_argument("-c", "--codeql", required=True, help="Path to CodeQL CLI executable.")
parser.add_argument("-d", "--database", required=True, help="Path to the CodeQL database.")
parser.add_argument("-q", "--query", required=True, help="Path to the .ql query file.")
parser.add_argument("--queryid", required=True, help="Query ID for the analysis.")
parser.add_argument("-o", "--output", required=True, help="Output directory for analysis results.")
args = parser.parse_args()
@@ -94,7 +96,13 @@ def main():
run_codeql_analysis(args.codeql, args.database, args.query, args.output)
# Locate DGML file
dgml_file = os.path.join(args.output, "java", "print-cbom-graph.dgml")
ALLOWED_QUERY_ID = re.compile(r'^[a-zA-Z0-9_\-]+$')
if not ALLOWED_QUERY_ID.match(args.queryid):
print("Invalid query_id provided: '%s'. Allowed characters: letters, digits, '_', and '-'.", args.queryid)
sys.exit(1)
dgml_file = os.path.join(args.output, "java", '{}.dgml'.format(args.queryid))
dot_file = dgml_file.replace(".dgml", ".dot")
if os.path.exists(dgml_file):

File diff suppressed because it is too large Load Diff