Add modelling for JCA key gen cipher algorithm

This commit is contained in:
Nicolas Will
2025-04-30 16:28:31 +02:00
parent 1958c192ec
commit 7f24a2557d
8 changed files with 234 additions and 71 deletions

View File

@@ -2,7 +2,6 @@ import java
import semmle.code.java.dataflow.DataFlow
import semmle.code.java.dataflow.TaintTracking
import semmle.code.java.controlflow.Dominance
import codeql.util.Option
module JCAModel {
import Language
@@ -354,9 +353,11 @@ module JCAModel {
else result instanceof KeyOpAlg::TUnknownKeyOperationAlgorithmType
}
override string getKeySize() {
override string getKeySizeFixed() {
none() // TODO: implement to handle variants such as AES-128
}
override Crypto::ConsumerInputDataFlowNode getKeySizeConsumer() { none() }
}
bindingset[input]
@@ -394,8 +395,6 @@ module JCAModel {
override Crypto::HashAlgorithmInstance getOAEPEncodingHashAlgorithm() { result = this }
override Crypto::HashAlgorithmInstance getMGF1HashAlgorithm() { none() } // TODO
override string getKeySize() { none() }
}
/**
@@ -446,8 +445,6 @@ module JCAModel {
predicate isIntermediate();
}
module MethodCallOption = Option<MethodCall>;
/**
* An generic analysis module for analyzing the `getInstance` to `initialize` to `doOperation` pattern in the JCA.
*
@@ -568,6 +565,14 @@ module JCAModel {
GetInstanceToInitToUseFlow::flowPath(src, sink)
}
GetInstance getInstantiationFromInit(
Init init, GetInstanceToInitToUseFlow::PathNode src, GetInstanceToInitToUseFlow::PathNode sink
) {
src.getNode().asExpr() = result and
sink.getNode().asExpr() = init.(MethodCall).getQualifier() and
GetInstanceToInitToUseFlow::flowPath(src, sink)
}
Init getInitFromUse(
Use use, GetInstanceToInitToUseFlow::PathNode src, GetInstanceToInitToUseFlow::PathNode sink
) {
@@ -829,6 +834,9 @@ module JCAModel {
}
}
module MessageDigestFlowAnalysisImpl =
GetInstanceInitUseFlowAnalysis<MessageDigestGetInstanceCall, DUMMY_UNUSED_METHODCALL, DigestCall>;
class MessageDigestGetInstanceAlgorithmValueConsumer extends HashAlgorithmValueConsumer {
MessageDigestGetInstanceCall call;
@@ -849,17 +857,18 @@ module JCAModel {
}
Expr getAlgorithmArg() { result = this.getArgument(0) }
DigestHashOperation getDigestCall() {
DigestGetInstanceToDigestFlow::flow(DataFlow::exprNode(this),
DataFlow::exprNode(result.(DigestCall).getQualifier()))
}
}
class DigestCall extends MethodCall {
DigestCall() { this.getCallee().hasQualifiedName("java.security", "MessageDigest", "digest") }
DigestCall() {
this.getCallee().hasQualifiedName("java.security", "MessageDigest", ["update", "digest"])
}
Expr getDigestArtifactOutput() { result = this }
Expr getInputArg() { result = this.getArgument(0) }
predicate isIntermediate() { this.getMethod().getName() = "update" }
}
// flow config from MessageDigest.getInstance to MessageDigest.digest
@@ -873,23 +882,22 @@ module JCAModel {
module DigestGetInstanceToDigestFlow = DataFlow::Global<DigestGetInstanceToDigestConfig>;
class DigestArtifact extends Crypto::DigestArtifactInstance {
DigestArtifact() { this = any(DigestCall call).getDigestArtifactOutput() }
override DataFlow::Node getOutputNode() { result.asExpr() = this }
}
class DigestHashOperation extends Crypto::HashOperationInstance instanceof DigestCall {
override Crypto::DigestArtifactInstance getDigestArtifact() {
result = this.(DigestCall).getDigestArtifactOutput()
DigestHashOperation() { not super.isIntermediate() }
override Crypto::ArtifactOutputDataFlowNode getOutputArtifact() {
result.asExpr() = super.getDigestArtifactOutput()
}
override Crypto::AlgorithmValueConsumer getAnAlgorithmValueConsumer() {
exists(MessageDigestGetInstanceCall getInstanceCall |
getInstanceCall.getDigestCall() = this and
getInstanceCall =
result.(MessageDigestGetInstanceAlgorithmValueConsumer).getInstantiationCall()
)
MessageDigestFlowAnalysisImpl::getInstantiationFromUse(this, _, _) =
result.(MessageDigestGetInstanceAlgorithmValueConsumer).getInstantiationCall()
}
override Crypto::ConsumerInputDataFlowNode getInputConsumer() {
result.asExpr() = super.getInputArg() or
result.asExpr() =
MessageDigestFlowAnalysisImpl::getAnIntermediateUseFromFinalUse(this, _, _).getInputArg()
}
}
@@ -997,6 +1005,7 @@ module JCAModel {
or
// However, for general elliptic curves, getInstance("EC") is used
// and java.security.spec.ECGenParameterSpec("<CURVE NAME>") is what sets the specific curve.
// If init is not specified, the default (P-)
// The result of ECGenParameterSpec is passed to KeyPairGenerator.initialize
// If the curve is not specified, the default is used.
// We would trace the use of this inside a KeyPairGenerator.initialize
@@ -1096,6 +1105,30 @@ module JCAModel {
override string getKeySizeFixed() { none() }
}
class KeyGeneratorCipherAlgorithm extends CipherStringLiteralAlgorithmInstance {
KeyGeneratorCipherAlgorithm() { consumer instanceof KeyGenerationAlgorithmValueConsumer }
override Crypto::ConsumerInputDataFlowNode getKeySizeConsumer() {
exists(KeyGeneratorGetInstanceCall getInstance, KeyGeneratorInitCall init |
getInstance =
this.getConsumer().(KeyGenerationAlgorithmValueConsumer).getInstantiationCall() and
getInstance = KeyGeneratorFlowAnalysisImpl::getInstantiationFromInit(init, _, _) and
init.getKeySizeArg() = result.asExpr()
)
}
predicate isOnlyConsumedByKeyGen() {
forall(Crypto::AlgorithmValueConsumer c |
c = this.getConsumer() and
c instanceof KeyGenerationAlgorithmValueConsumer
)
}
override predicate shouldHaveModeOfOperation() { this.isOnlyConsumedByKeyGen() }
override predicate shouldHavePaddingScheme() { this.isOnlyConsumedByKeyGen() }
}
/*
* Key Derivation Functions (KDFs)
*/

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() }
@@ -107,7 +107,7 @@ class ConstantDataSource extends Crypto::GenericConstantSourceInstance instanceo
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()
}
@@ -203,7 +212,7 @@ module ArtifactUniversalFlowConfig implements DataFlow::ConfigSig {
}
}
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

@@ -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,5 +1,5 @@
/**
* @name "PQC Test"
* @name "Key operation slice table demo query"
*/
import experimental.Quantum.Language

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()