From 395d54bf867803acddc8012c4c44bf8b56531165 Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Thu, 23 Jan 2025 12:46:09 +0100 Subject: [PATCH 01/28] Create Base.qll --- cpp/ql/lib/experimental/Quantum/Base.qll | 165 +++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 cpp/ql/lib/experimental/Quantum/Base.qll diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/cpp/ql/lib/experimental/Quantum/Base.qll new file mode 100644 index 000000000000..bfdd509174e5 --- /dev/null +++ b/cpp/ql/lib/experimental/Quantum/Base.qll @@ -0,0 +1,165 @@ +/** + * A language-independent library for reasoning about cryptography. + */ + +import codeql.util.Location +import codeql.util.Option + +signature module InputSig { + class KnownUnknownLocation extends Location; + + class LocatableElement { + Location getLocation(); + } +} + +module CryptographyBase Input> { + final class LocatableElement = Input::LocatableElement; + + newtype TNode = + TNodeUnknown() or + TNodeAsset() or + TNodeValue() // currently unused + + class KnownNode = TNodeAsset or TNodeValue; + + abstract class NodeBase extends TNode { + /** + * Returns a string representation of this node, usually the name of the operation/algorithm/property. + */ + abstract string toString(); + + /** + * Returns the location of this node in the code. + */ + abstract Location getLocation(); + + /** + * Returns the child of this node with the given edge name. + * + * This predicate is used by derived classes to construct the graph of cryptographic operations. + */ + NodeBase getChild(string edgeName) { none() } + + /** + * Returns the parent of this node. + */ + final NodeBase getAParent() { result.getChild(_) = this } + } + + /** + * A node representing an unknown value. + * + * If a property should have a value but that value is unknown, `UnknownNode` to represent that value. + */ + final class UnknownNode extends NodeBase, TNodeUnknown { + override string toString() { result = "unknown" } + + override Location getLocation() { result instanceof Input::KnownUnknownLocation } + } + + /** + * A node with a known location in the code. + */ + abstract class LocatableNode extends NodeBase, TNodeAsset { + abstract LocatableElement toElement(); + + override Location getLocation() { result = this.toElement().getLocation() } + } + + /** + * A node representing a known asset, i.e., an algorithm, operation, or property. + */ + class Asset = LocatableNode; + + /** + * A cryptographic operation, such as hashing or encryption. + */ + abstract class Operation extends Asset { + /** + * Gets the algorithm associated with this operation. + */ + private NodeBase getAlgorithmOrUnknown() { + if exists(this.getAlgorithm()) + then result = this.getAlgorithm() + else result instanceof UnknownNode + } + + abstract Algorithm getAlgorithm(); + + /** + * Gets the name of this operation, e.g., "hash" or "encrypt". + */ + abstract string getOperationName(); + + final override string toString() { result = this.getOperationName() } + + override NodeBase getChild(string edgeName) { + edgeName = "algorithm" and + this.getAlgorithmOrUnknown() = result + } + } + + abstract class Algorithm extends Asset { + /** + * Gets the name of this algorithm, e.g., "AES" or "SHA". + */ + abstract string getAlgorithmName(); + + final override string toString() { result = this.getAlgorithmName() } + } + + /** + * A hashing operation that processes data to generate a hash value. + * This operation takes an input message of arbitrary content and length and produces a fixed-size + * hash value as the output using a specified hashing algorithm. + */ + abstract class HashOperation extends Operation { + abstract override HashAlgorithm getAlgorithm(); + + override string getOperationName() { result = "hash" } + } + + /** + * A hashing algorithm that transforms variable-length input into a fixed-size hash value. + */ + abstract class HashAlgorithm extends Algorithm { } + + /** + * An operation that derives one or more keys from an input value. + */ + abstract class KeyDerivationOperation extends Operation { + override string getOperationName() { result = "key derivation" } + } + + /** + * An algorithm that derives one or more keys from an input value. + */ + abstract class KeyDerivationAlgorithm extends Algorithm { + abstract override string getAlgorithmName(); + } + + /** + * HKDF Extract+Expand key derivation function. + */ + abstract class HKDFAlgorithm extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "HKDF" } + + private NodeBase getHashAlgorithmOrUnknown() { + if exists(this.getHashAlgorithm()) + then result = this.getHashAlgorithm() + else result instanceof UnknownNode + } + + abstract HashAlgorithm getHashAlgorithm(); + + /** + * digest:HashAlgorithm + */ + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "digest" and result = this.getHashAlgorithmOrUnknown() + } + } +} From 1a7d8cb99db194624238ab0d2880bd6984c96904 Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Fri, 24 Jan 2025 17:33:03 +0100 Subject: [PATCH 02/28] WIP --- cpp/ql/lib/experimental/Quantum/Base.qll | 80 ++++------- .../lib/experimental/Quantum/BaseBackup.qll | 125 ++++++++++++++++++ cpp/ql/lib/experimental/Quantum/Language.qll | 10 ++ cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 100 ++++++++++++++ cpp/ql/src/experimental/Quantum/Test.ql | 17 +++ cpp/ql/src/experimental/Quantum/Test2.ql | 8 ++ 6 files changed, 288 insertions(+), 52 deletions(-) create mode 100644 cpp/ql/lib/experimental/Quantum/BaseBackup.qll create mode 100644 cpp/ql/lib/experimental/Quantum/Language.qll create mode 100644 cpp/ql/lib/experimental/Quantum/OpenSSL.qll create mode 100644 cpp/ql/src/experimental/Quantum/Test.ql create mode 100644 cpp/ql/src/experimental/Quantum/Test2.ql diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/cpp/ql/lib/experimental/Quantum/Base.qll index bfdd509174e5..8a910eb44143 100644 --- a/cpp/ql/lib/experimental/Quantum/Base.qll +++ b/cpp/ql/lib/experimental/Quantum/Base.qll @@ -6,8 +6,6 @@ import codeql.util.Location import codeql.util.Option signature module InputSig { - class KnownUnknownLocation extends Location; - class LocatableElement { Location getLocation(); } @@ -16,14 +14,7 @@ signature module InputSig { module CryptographyBase Input> { final class LocatableElement = Input::LocatableElement; - newtype TNode = - TNodeUnknown() or - TNodeAsset() or - TNodeValue() // currently unused - - class KnownNode = TNodeAsset or TNodeValue; - - abstract class NodeBase extends TNode { + abstract class NodeBase instanceof LocatableElement { /** * Returns a string representation of this node, usually the name of the operation/algorithm/property. */ @@ -32,14 +23,19 @@ module CryptographyBase Input> { /** * Returns the location of this node in the code. */ - abstract Location getLocation(); + Location getLocation() { result = super.getLocation() } /** * Returns the child of this node with the given edge name. * * This predicate is used by derived classes to construct the graph of cryptographic operations. */ - NodeBase getChild(string edgeName) { none() } + NodeBase getChild(string edgeName) { edgeName = "origin" and result = this.getOrigin() } + + /** + * Gets the origin of this node, e.g., a string literal in source describing it. + */ + NodeBase getOrigin() { none() } /** * Returns the parent of this node. @@ -47,30 +43,7 @@ module CryptographyBase Input> { final NodeBase getAParent() { result.getChild(_) = this } } - /** - * A node representing an unknown value. - * - * If a property should have a value but that value is unknown, `UnknownNode` to represent that value. - */ - final class UnknownNode extends NodeBase, TNodeUnknown { - override string toString() { result = "unknown" } - - override Location getLocation() { result instanceof Input::KnownUnknownLocation } - } - - /** - * A node with a known location in the code. - */ - abstract class LocatableNode extends NodeBase, TNodeAsset { - abstract LocatableElement toElement(); - - override Location getLocation() { result = this.toElement().getLocation() } - } - - /** - * A node representing a known asset, i.e., an algorithm, operation, or property. - */ - class Asset = LocatableNode; + class Asset = NodeBase; /** * A cryptographic operation, such as hashing or encryption. @@ -79,12 +52,6 @@ module CryptographyBase Input> { /** * Gets the algorithm associated with this operation. */ - private NodeBase getAlgorithmOrUnknown() { - if exists(this.getAlgorithm()) - then result = this.getAlgorithm() - else result instanceof UnknownNode - } - abstract Algorithm getAlgorithm(); /** @@ -95,8 +62,10 @@ module CryptographyBase Input> { final override string toString() { result = this.getOperationName() } override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or edgeName = "algorithm" and - this.getAlgorithmOrUnknown() = result + if exists(this.getAlgorithm()) then result = this.getAlgorithm() else result = this } } @@ -125,6 +94,10 @@ module CryptographyBase Input> { */ abstract class HashAlgorithm extends Algorithm { } + abstract class SHA1 extends HashAlgorithm { + override string getAlgorithmName() { result = "SHA1" } + } + /** * An operation that derives one or more keys from an input value. */ @@ -142,24 +115,27 @@ module CryptographyBase Input> { /** * HKDF Extract+Expand key derivation function. */ - abstract class HKDFAlgorithm extends KeyDerivationAlgorithm { + abstract class HKDF extends KeyDerivationAlgorithm { final override string getAlgorithmName() { result = "HKDF" } - private NodeBase getHashAlgorithmOrUnknown() { - if exists(this.getHashAlgorithm()) - then result = this.getHashAlgorithm() - else result instanceof UnknownNode + abstract HashAlgorithm getHashAlgorithm(); + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "digest" and result = this.getHashAlgorithm() } + } + + abstract class PKCS12KDF extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "PKCS12KDF" } abstract HashAlgorithm getHashAlgorithm(); - /** - * digest:HashAlgorithm - */ override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or - edgeName = "digest" and result = this.getHashAlgorithmOrUnknown() + edgeName = "digest" and result = this.getHashAlgorithm() } } } diff --git a/cpp/ql/lib/experimental/Quantum/BaseBackup.qll b/cpp/ql/lib/experimental/Quantum/BaseBackup.qll new file mode 100644 index 000000000000..821c89eb8f57 --- /dev/null +++ b/cpp/ql/lib/experimental/Quantum/BaseBackup.qll @@ -0,0 +1,125 @@ +/** + * A language-independent library for reasoning about cryptography. + */ + +import codeql.util.Location +import codeql.util.Option + +signature module InputSig { + class KnownUnknownLocation extends Location; + + class LocatableElement { + Location getLocation(); + } +} + +// An operation = a specific loc in code +// An algorithm +// Properties +// Node -> Operation -> Algorithm -> Symmetric -> SpecificSymmetricAlgo +// -[Language-Specific]-> LibrarySymmetricAlgo -> Properties +// For example (nsted newtypes): +/* + * newtype for each algo, and each one of those would have params for their properties + * implementation: optional/range for example + * + * + * + * /** + * Constructs an `Option` type that is a disjoint union of the given type and an + * additional singleton element. + */ + +module CryptographyBase Input> { + newtype TNode = + TNodeUnknown() or + TNodeAlgorithm() or + TNodeOperation() + + /* + * A cryptographic asset in code, i.e., an algorithm, operation, property, or known unknown. + */ + + abstract class Node extends TNode { + // this would then extend LanguageNode + abstract Location getLocation(); + + abstract string toString(); + + abstract Node getChild(int childIndex); + + final Node getAChild() { result = this.getChild(_) } + + final Node getAParent() { result.getAChild() = this } + } + + final class KnownUnknown extends Node, TNodeUnknown { + override string toString() { result = "unknown" } + + override Node getChild(int childIndex) { none() } + + override Location getLocation() { result instanceof Input::KnownUnknownLocation } + } + + abstract class Operation extends Node, TNodeOperation { + /** + * Gets the algorithm associated with this operation. + */ + abstract Node getAlgorithm(); + + /** + * Gets the name of this operation, e.g., "hash" or "encrypt". + */ + abstract string getOperationName(); + + final override Node getChild(int childIndex) { childIndex = 0 and result = this.getAlgorithm() } + + final override string toString() { result = this.getOperationName() } + } + + abstract class Algorithm extends Node, TNodeAlgorithm { + /** + * Gets the name of this algorithm, e.g., "AES" or "SHA". + */ + abstract string getAlgorithmName(); + } + + /** + * A hashing operation that processes data to generate a hash value. + * This operation takes an input message of arbitrary content and length and produces a fixed-size + * hash value as the output using a specified hashing algorithm. + */ + abstract class HashOperation extends Operation { + abstract override HashAlgorithm getAlgorithm(); + + override string getOperationName() { result = "hash" } + } + + /** + * A hashing algorithm that transforms variable-length input into a fixed-size hash value. + */ + abstract class HashAlgorithm extends Algorithm { } + + /** + * An operation that derives one or more keys from an input value. + */ + abstract class KeyDerivationOperation extends Operation { + override string getOperationName() { result = "key derivation" } + } + + /** + * An algorithm that derives one or more keys from an input value. + */ + abstract class KeyDerivationAlgorithm extends Algorithm { + abstract override string getAlgorithmName(); + } + + /** + * HKDF Extract+Expand key derivation function. + */ + abstract class HKDFAlgorithm extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "HKDF" } + + abstract Node getDigestAlgorithm(); + } +} diff --git a/cpp/ql/lib/experimental/Quantum/Language.qll b/cpp/ql/lib/experimental/Quantum/Language.qll new file mode 100644 index 000000000000..108993fb134c --- /dev/null +++ b/cpp/ql/lib/experimental/Quantum/Language.qll @@ -0,0 +1,10 @@ +private import Base +private import cpp as Lang + +module CryptoInput implements InputSig { + class LocatableElement = Lang::Locatable; +} + +module Crypto = CryptographyBase; + +import OpenSSL diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll new file mode 100644 index 000000000000..b489a6630a0e --- /dev/null +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -0,0 +1,100 @@ +import cpp +import semmle.code.cpp.dataflow.new.DataFlow + +module OpenSSLModel { + import Language + + abstract class KeyDerivationOperation extends Crypto::KeyDerivationOperation { } + + class SHA1Algo extends Crypto::SHA1 instanceof MacroAccess { + SHA1Algo() { this.getMacro().getName() = "SN_sha1" } + } + + module AlgorithmToEVPKeyDeriveConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { source.asExpr() instanceof KeyDerivationAlgorithm } + + predicate isSink(DataFlow::Node sink) { + exists(EVP_KDF_derive kdo | sink.asExpr() = kdo.getAlgorithmArg()) + } + } + + module AlgorithmToEVPKeyDeriveFlow = DataFlow::Global; + + predicate algorithm_to_EVP_KDF_derive(Crypto::Algorithm algo, EVP_KDF_derive derive) { + algo.(Expr).getEnclosingFunction() = derive.(Expr).getEnclosingFunction() + } + + class EVP_KDF_derive extends KeyDerivationOperation instanceof FunctionCall { + EVP_KDF_derive() { this.getTarget().getName() = "EVP_KDF_derive" } + + override Crypto::Algorithm getAlgorithm() { algorithm_to_EVP_KDF_derive(result, this) } + + Expr getAlgorithmArg() { result = this.(FunctionCall).getArgument(3) } + } + + abstract class KeyDerivationAlgorithm extends Crypto::KeyDerivationAlgorithm { } + + class EVP_KDF_fetch_Call extends FunctionCall { + EVP_KDF_fetch_Call() { this.getTarget().getName() = "EVP_KDF_fetch" } + + Expr getAlgorithmArg() { result = this.getArgument(1) } + } + + predicate kdf_names(string algo) { algo = ["HKDF", "PKCS12KDF"] } + + class KDFAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLiteral { + KDFAlgorithmStringLiteral() { kdf_names(this.getValue().toUpperCase()) } + + override string toString() { result = this.(StringLiteral).toString() } + + string getValue() { result = this.(StringLiteral).getValue() } + } + + private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node src) { src.asExpr() instanceof KDFAlgorithmStringLiteral } + + predicate isSink(DataFlow::Node sink) { + exists(EVP_KDF_fetch_Call call | sink.asExpr() = call.getAlgorithmArg()) + } + } + + module AlgorithmStringToFetchFlow = DataFlow::Global; + + predicate algorithmStringToKDFFetchArgFlow(string name, KDFAlgorithmStringLiteral origin, Expr arg) { + exists(EVP_KDF_fetch_Call sinkCall | + origin.getValue().toUpperCase() = name and + arg = sinkCall.getAlgorithmArg() and + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) + ) + } + + class HKDF extends KeyDerivationAlgorithm, Crypto::HKDF instanceof Expr { + KDFAlgorithmStringLiteral origin; + + HKDF() { algorithmStringToKDFFetchArgFlow("HKDF", origin, this) } + + override Crypto::HashAlgorithm getHashAlgorithm() { none() } + + override Crypto::NodeBase getOrigin() { result = origin } + } + + class TestKeyDerivationOperationHacky extends KeyDerivationOperation instanceof FunctionCall { + HKDF hkdf; + + TestKeyDerivationOperationHacky() { + this.getEnclosingFunction() = hkdf.(Expr).getEnclosingFunction() + } + + override Crypto::KeyDerivationAlgorithm getAlgorithm() { result = hkdf } + } + + class PKCS12KDF extends KeyDerivationAlgorithm, Crypto::PKCS12KDF instanceof Expr { + KDFAlgorithmStringLiteral origin; + + PKCS12KDF() { algorithmStringToKDFFetchArgFlow("PKCS12KDF", origin, this) } + + override Crypto::HashAlgorithm getHashAlgorithm() { none() } + + override Crypto::NodeBase getOrigin() { result = origin } + } +} diff --git a/cpp/ql/src/experimental/Quantum/Test.ql b/cpp/ql/src/experimental/Quantum/Test.ql new file mode 100644 index 000000000000..a9ad5021a295 --- /dev/null +++ b/cpp/ql/src/experimental/Quantum/Test.ql @@ -0,0 +1,17 @@ +/** + * @name "PQC Test" + * @kind graph + */ + +import experimental.Quantum.Language + +query predicate nodes(Crypto::NodeBase node) { any() } + +query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { + target = source.getChild(value) and + key = "semmle.label" +} + +query predicate graphProperties(string key, string value) { + key = "semmle.graphKind" and value = "tree" +} diff --git a/cpp/ql/src/experimental/Quantum/Test2.ql b/cpp/ql/src/experimental/Quantum/Test2.ql new file mode 100644 index 000000000000..f5971da96443 --- /dev/null +++ b/cpp/ql/src/experimental/Quantum/Test2.ql @@ -0,0 +1,8 @@ +/** + * @name "PQC Test" + */ + +import experimental.Quantum.Language + +from Crypto::KeyDerivationAlgorithm n +select n From 78362341fff9adb73deaf5a3a3f85f1da66481b0 Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Fri, 24 Jan 2025 22:32:32 +0100 Subject: [PATCH 03/28] WIP: hash types example and documentation --- cpp/ql/lib/experimental/Quantum/Base.qll | 38 ++++++++++++++++++--- cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 4 ++- 2 files changed, 37 insertions(+), 5 deletions(-) diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/cpp/ql/lib/experimental/Quantum/Base.qll index 8a910eb44143..22e810f4aff4 100644 --- a/cpp/ql/lib/experimental/Quantum/Base.qll +++ b/cpp/ql/lib/experimental/Quantum/Base.qll @@ -64,7 +64,7 @@ module CryptographyBase Input> { override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or - edgeName = "algorithm" and + edgeName = "uses" and if exists(this.getAlgorithm()) then result = this.getAlgorithm() else result = this } } @@ -89,13 +89,43 @@ module CryptographyBase Input> { override string getOperationName() { result = "hash" } } + // Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces + // + // Example: HKDF and PKCS12KDF are both key derivation algorithms. + // However, PKCS12KDF also has a property: the iteration count. + // + // If we have HKDF and PKCS12KDF under TKeyDerivationType, + // someone modelling a library might try to make a generic identification of both of those algorithms. + // + // They will therefore not use the specialized type for PKCS12KDF, + // meaning "from PKCS12KDF algo select algo" will have no results. + // + newtype THashType = + // We're saying by this that all of these have an identical interface / properties / edges + MD5() or + SHA1() or + SHA256() or + SHA512() + + class HashAlgorithmType extends THashType { + string toString() { hashTypeToNameMapping(this, result) } + } + + predicate hashTypeToNameMapping(THashType type, string name) { + type instanceof SHA1 and name = "SHA-1" + or + type instanceof SHA256 and name = "SHA-256" + or + type instanceof SHA512 and name = "SHA-512" + } + /** * A hashing algorithm that transforms variable-length input into a fixed-size hash value. */ - abstract class HashAlgorithm extends Algorithm { } + abstract class HashAlgorithm extends Algorithm { + abstract HashAlgorithmType getHashType(); - abstract class SHA1 extends HashAlgorithm { - override string getAlgorithmName() { result = "SHA1" } + override string getAlgorithmName() { hashTypeToNameMapping(this.getHashType(), result) } } /** diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll index b489a6630a0e..17de5ddab604 100644 --- a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -6,8 +6,10 @@ module OpenSSLModel { abstract class KeyDerivationOperation extends Crypto::KeyDerivationOperation { } - class SHA1Algo extends Crypto::SHA1 instanceof MacroAccess { + class SHA1Algo extends Crypto::HashAlgorithm instanceof MacroAccess { SHA1Algo() { this.getMacro().getName() = "SN_sha1" } + + override Crypto::HashAlgorithmType getHashType() { result instanceof Crypto::SHA1 } } module AlgorithmToEVPKeyDeriveConfig implements DataFlow::ConfigSig { From e027b0e9a0e56f21226d832bcd87751a8c0ee47f Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Tue, 28 Jan 2025 02:02:06 +0100 Subject: [PATCH 04/28] WIP: add properties --- cpp/ql/lib/experimental/Quantum/Base.qll | 95 +++++++++++++++----- cpp/ql/lib/experimental/Quantum/Language.qll | 2 + cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 12 ++- cpp/ql/src/experimental/Quantum/Test.ql | 28 +++++- cpp/ql/src/experimental/Quantum/Test2.ql | 4 +- 5 files changed, 114 insertions(+), 27 deletions(-) diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/cpp/ql/lib/experimental/Quantum/Base.qll index 22e810f4aff4..b3f4d619f4d8 100644 --- a/cpp/ql/lib/experimental/Quantum/Base.qll +++ b/cpp/ql/lib/experimental/Quantum/Base.qll @@ -9,11 +9,19 @@ signature module InputSig { class LocatableElement { Location getLocation(); } + + class UnknownLocation instanceof Location; } module CryptographyBase Input> { final class LocatableElement = Input::LocatableElement; + final class UnknownLocation = Input::UnknownLocation; + + final class UnknownPropertyValue extends string { + UnknownPropertyValue() { this = "" } + } + abstract class NodeBase instanceof LocatableElement { /** * Returns a string representation of this node, usually the name of the operation/algorithm/property. @@ -25,17 +33,26 @@ module CryptographyBase Input> { */ Location getLocation() { result = super.getLocation() } + /** + * Gets the origin of this node, e.g., a string literal in source describing it. + */ + LocatableElement getOrigin(string value) { none() } + /** * Returns the child of this node with the given edge name. * * This predicate is used by derived classes to construct the graph of cryptographic operations. */ - NodeBase getChild(string edgeName) { edgeName = "origin" and result = this.getOrigin() } + NodeBase getChild(string edgeName) { none() } /** - * Gets the origin of this node, e.g., a string literal in source describing it. + * Defines properties of this node by name and either a value or location or both. + * + * This predicate is used by derived classes to construct the graph of cryptographic operations. */ - NodeBase getOrigin() { none() } + predicate properties(string key, string value, Location location) { + key = "origin" and location = this.getOrigin(value).getLocation() + } /** * Returns the parent of this node. @@ -86,7 +103,7 @@ module CryptographyBase Input> { abstract class HashOperation extends Operation { abstract override HashAlgorithm getAlgorithm(); - override string getOperationName() { result = "hash" } + override string getOperationName() { result = "HASH" } } // Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces @@ -105,34 +122,40 @@ module CryptographyBase Input> { MD5() or SHA1() or SHA256() or - SHA512() - - class HashAlgorithmType extends THashType { - string toString() { hashTypeToNameMapping(this, result) } - } - - predicate hashTypeToNameMapping(THashType type, string name) { - type instanceof SHA1 and name = "SHA-1" - or - type instanceof SHA256 and name = "SHA-256" - or - type instanceof SHA512 and name = "SHA-512" - } + SHA512() or + OtherHashType() /** * A hashing algorithm that transforms variable-length input into a fixed-size hash value. */ abstract class HashAlgorithm extends Algorithm { - abstract HashAlgorithmType getHashType(); + final predicate hashTypeToNameMapping(THashType type, string name) { + type instanceof MD5 and name = "MD5" + or + type instanceof SHA1 and name = "SHA-1" + or + type instanceof SHA256 and name = "SHA-256" + or + type instanceof SHA512 and name = "SHA-512" + or + type instanceof OtherHashType and name = this.getRawAlgorithmName() + } + + abstract THashType getHashType(); + + override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } - override string getAlgorithmName() { hashTypeToNameMapping(this.getHashType(), result) } + /** + * Gets the raw name of this hash algorithm from source. + */ + abstract string getRawAlgorithmName(); } /** * An operation that derives one or more keys from an input value. */ abstract class KeyDerivationOperation extends Operation { - override string getOperationName() { result = "key derivation" } + override string getOperationName() { result = "KEY_DERIVATION" } } /** @@ -143,7 +166,7 @@ module CryptographyBase Input> { } /** - * HKDF Extract+Expand key derivation function. + * HKDF key derivation function */ abstract class HKDF extends KeyDerivationAlgorithm { final override string getAlgorithmName() { result = "HKDF" } @@ -157,6 +180,9 @@ module CryptographyBase Input> { } } + /** + * PKCS #12 key derivation function + */ abstract class PKCS12KDF extends KeyDerivationAlgorithm { final override string getAlgorithmName() { result = "PKCS12KDF" } @@ -168,4 +194,31 @@ module CryptographyBase Input> { edgeName = "digest" and result = this.getHashAlgorithm() } } + + /** + * Elliptic curve algorithm + */ + abstract class EllipticCurve extends Algorithm { + abstract string getVersion(Location location); + + abstract string getKeySize(Location location); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + key = "version" and + if exists(this.getVersion(location)) + then value = this.getVersion(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + or + key = "key_size" and + if exists(this.getKeySize(location)) + then value = this.getKeySize(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + } + } } diff --git a/cpp/ql/lib/experimental/Quantum/Language.qll b/cpp/ql/lib/experimental/Quantum/Language.qll index 108993fb134c..c9398c9e3245 100644 --- a/cpp/ql/lib/experimental/Quantum/Language.qll +++ b/cpp/ql/lib/experimental/Quantum/Language.qll @@ -3,6 +3,8 @@ private import cpp as Lang module CryptoInput implements InputSig { class LocatableElement = Lang::Locatable; + + class UnknownLocation = Lang::UnknownDefaultLocation; } module Crypto = CryptographyBase; diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll index 17de5ddab604..852fedf646a8 100644 --- a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -9,7 +9,9 @@ module OpenSSLModel { class SHA1Algo extends Crypto::HashAlgorithm instanceof MacroAccess { SHA1Algo() { this.getMacro().getName() = "SN_sha1" } - override Crypto::HashAlgorithmType getHashType() { result instanceof Crypto::SHA1 } + override string getRawAlgorithmName() { result = "SN_sha1" } + + override Crypto::THashType getHashType() { result instanceof Crypto::SHA1 } } module AlgorithmToEVPKeyDeriveConfig implements DataFlow::ConfigSig { @@ -77,7 +79,9 @@ module OpenSSLModel { override Crypto::HashAlgorithm getHashAlgorithm() { none() } - override Crypto::NodeBase getOrigin() { result = origin } + override Crypto::LocatableElement getOrigin(string name) { + result = origin and name = origin.toString() + } } class TestKeyDerivationOperationHacky extends KeyDerivationOperation instanceof FunctionCall { @@ -97,6 +101,8 @@ module OpenSSLModel { override Crypto::HashAlgorithm getHashAlgorithm() { none() } - override Crypto::NodeBase getOrigin() { result = origin } + override Crypto::NodeBase getOrigin(string name) { + result = origin and name = origin.toString() + } } } diff --git a/cpp/ql/src/experimental/Quantum/Test.ql b/cpp/ql/src/experimental/Quantum/Test.ql index a9ad5021a295..87341a6b612c 100644 --- a/cpp/ql/src/experimental/Quantum/Test.ql +++ b/cpp/ql/src/experimental/Quantum/Test.ql @@ -5,7 +5,33 @@ import experimental.Quantum.Language -query predicate nodes(Crypto::NodeBase node) { any() } +string getValueAndLocationPairs(Crypto::NodeBase node, string key) { + exists(string value, Location location | + node.properties(key, value, location) and + result = "(" + value + "," + location.toString() + ")" + ) +} + +string properties(Crypto::NodeBase node) { + forex(string key | node.properties(key, _, _) | + result = key + ":" + strictconcat(getValueAndLocationPairs(node, key), ",") + ) +} + +string getLabel(Crypto::NodeBase node) { + result = + "[" + node.toString() + "]" + + any(string prop | + if exists(properties(node)) then prop = " " + properties(node) else prop = "" + | + prop + ) +} + +query predicate nodes(Crypto::NodeBase node, string key, string value) { + key = "semmle.label" and + value = getLabel(node) +} query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { target = source.getChild(value) and diff --git a/cpp/ql/src/experimental/Quantum/Test2.ql b/cpp/ql/src/experimental/Quantum/Test2.ql index f5971da96443..3f48f156a430 100644 --- a/cpp/ql/src/experimental/Quantum/Test2.ql +++ b/cpp/ql/src/experimental/Quantum/Test2.ql @@ -4,5 +4,5 @@ import experimental.Quantum.Language -from Crypto::KeyDerivationAlgorithm n -select n +from Crypto::NodeBase node +select node From 0cd3df9d2685d9aef55b2305c2ef2d478d3e1223 Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Wed, 29 Jan 2025 10:27:46 -0500 Subject: [PATCH 05/28] Concepts for elliptic cureve and misc. updates. --- cpp/ql/lib/experimental/Quantum/Base.qll | 50 +++- python/ql/lib/experimental/Quantum/Base.qll | 250 ++++++++++++++++++ .../ql/lib/experimental/Quantum/Language.qll | 12 + .../experimental/Quantum/PycaCryptography.qll | 55 ++++ python/ql/lib/semmle/python/Files.qll | 37 +++ 5 files changed, 392 insertions(+), 12 deletions(-) create mode 100644 python/ql/lib/experimental/Quantum/Base.qll create mode 100644 python/ql/lib/experimental/Quantum/Language.qll create mode 100644 python/ql/lib/experimental/Quantum/PycaCryptography.qll diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/cpp/ql/lib/experimental/Quantum/Base.qll index b3f4d619f4d8..9be24ca6efaa 100644 --- a/cpp/ql/lib/experimental/Quantum/Base.qll +++ b/cpp/ql/lib/experimental/Quantum/Base.qll @@ -92,6 +92,11 @@ module CryptographyBase Input> { */ abstract string getAlgorithmName(); + /** + * Gets the raw name of this algorithm from source (no parsing or formatting) + */ + abstract string getRawAlgorithmName(); + final override string toString() { result = this.getAlgorithmName() } } @@ -145,10 +150,6 @@ module CryptographyBase Input> { override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } - /** - * Gets the raw name of this hash algorithm from source. - */ - abstract string getRawAlgorithmName(); } /** @@ -195,30 +196,55 @@ module CryptographyBase Input> { } } + newtype TEllipticCurveFamilyType = + // We're saying by this that all of these have an identical interface / properties / edges + NIST() or + SEC() or + NUMS() or + PRIME() or + BRAINPOOL() or + CURVE25519() or + CURVE448() or + C2() or + SM2() or + ES() or + OtherEllipticCurveFamilyType() + + /** * Elliptic curve algorithm */ abstract class EllipticCurve extends Algorithm { - abstract string getVersion(Location location); + abstract string getKeySize(Location location); + abstract TEllipticCurveFamilyType getCurveFamilyType(); + override predicate properties(string key, string value, Location location) { super.properties(key, value, location) or - key = "version" and - if exists(this.getVersion(location)) - then value = this.getVersion(location) - else ( - value instanceof UnknownPropertyValue and location instanceof UnknownLocation - ) - or key = "key_size" and if exists(this.getKeySize(location)) then value = this.getKeySize(location) else ( value instanceof UnknownPropertyValue and location instanceof UnknownLocation ) + // other properties, like field type are possible, but not modeled until considered necessary } + + override string getAlgorithmName() { result = this.getRawAlgorithmName().toUpperCase()} + + /** + * Mandating that for Elliptic Curves specifically, users are responsible + * for providing as the 'raw' name, the official name of the algorithm. + * Casing doesn't matter, we will enforce further naming restrictions on + * `getAlgorithmName` by default. + * Rationale: elliptic curve names can have a lot of variation in their components + * (e.g., "secp256r1" vs "P-256"), trying to produce generalized set of properties + * is possible to capture all cases, but such modeling is likely not necessary. + * if all properties need to be captured, we can reassess how names are generated. + */ + override abstract string getRawAlgorithmName(); } } diff --git a/python/ql/lib/experimental/Quantum/Base.qll b/python/ql/lib/experimental/Quantum/Base.qll new file mode 100644 index 000000000000..9be24ca6efaa --- /dev/null +++ b/python/ql/lib/experimental/Quantum/Base.qll @@ -0,0 +1,250 @@ +/** + * A language-independent library for reasoning about cryptography. + */ + +import codeql.util.Location +import codeql.util.Option + +signature module InputSig { + class LocatableElement { + Location getLocation(); + } + + class UnknownLocation instanceof Location; +} + +module CryptographyBase Input> { + final class LocatableElement = Input::LocatableElement; + + final class UnknownLocation = Input::UnknownLocation; + + final class UnknownPropertyValue extends string { + UnknownPropertyValue() { this = "" } + } + + abstract class NodeBase instanceof LocatableElement { + /** + * Returns a string representation of this node, usually the name of the operation/algorithm/property. + */ + abstract string toString(); + + /** + * Returns the location of this node in the code. + */ + Location getLocation() { result = super.getLocation() } + + /** + * Gets the origin of this node, e.g., a string literal in source describing it. + */ + LocatableElement getOrigin(string value) { none() } + + /** + * Returns the child of this node with the given edge name. + * + * This predicate is used by derived classes to construct the graph of cryptographic operations. + */ + NodeBase getChild(string edgeName) { none() } + + /** + * Defines properties of this node by name and either a value or location or both. + * + * This predicate is used by derived classes to construct the graph of cryptographic operations. + */ + predicate properties(string key, string value, Location location) { + key = "origin" and location = this.getOrigin(value).getLocation() + } + + /** + * Returns the parent of this node. + */ + final NodeBase getAParent() { result.getChild(_) = this } + } + + class Asset = NodeBase; + + /** + * A cryptographic operation, such as hashing or encryption. + */ + abstract class Operation extends Asset { + /** + * Gets the algorithm associated with this operation. + */ + abstract Algorithm getAlgorithm(); + + /** + * Gets the name of this operation, e.g., "hash" or "encrypt". + */ + abstract string getOperationName(); + + final override string toString() { result = this.getOperationName() } + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "uses" and + if exists(this.getAlgorithm()) then result = this.getAlgorithm() else result = this + } + } + + abstract class Algorithm extends Asset { + /** + * Gets the name of this algorithm, e.g., "AES" or "SHA". + */ + abstract string getAlgorithmName(); + + /** + * Gets the raw name of this algorithm from source (no parsing or formatting) + */ + abstract string getRawAlgorithmName(); + + final override string toString() { result = this.getAlgorithmName() } + } + + /** + * A hashing operation that processes data to generate a hash value. + * This operation takes an input message of arbitrary content and length and produces a fixed-size + * hash value as the output using a specified hashing algorithm. + */ + abstract class HashOperation extends Operation { + abstract override HashAlgorithm getAlgorithm(); + + override string getOperationName() { result = "HASH" } + } + + // Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces + // + // Example: HKDF and PKCS12KDF are both key derivation algorithms. + // However, PKCS12KDF also has a property: the iteration count. + // + // If we have HKDF and PKCS12KDF under TKeyDerivationType, + // someone modelling a library might try to make a generic identification of both of those algorithms. + // + // They will therefore not use the specialized type for PKCS12KDF, + // meaning "from PKCS12KDF algo select algo" will have no results. + // + newtype THashType = + // We're saying by this that all of these have an identical interface / properties / edges + MD5() or + SHA1() or + SHA256() or + SHA512() or + OtherHashType() + + /** + * A hashing algorithm that transforms variable-length input into a fixed-size hash value. + */ + abstract class HashAlgorithm extends Algorithm { + final predicate hashTypeToNameMapping(THashType type, string name) { + type instanceof MD5 and name = "MD5" + or + type instanceof SHA1 and name = "SHA-1" + or + type instanceof SHA256 and name = "SHA-256" + or + type instanceof SHA512 and name = "SHA-512" + or + type instanceof OtherHashType and name = this.getRawAlgorithmName() + } + + abstract THashType getHashType(); + + override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } + + } + + /** + * An operation that derives one or more keys from an input value. + */ + abstract class KeyDerivationOperation extends Operation { + override string getOperationName() { result = "KEY_DERIVATION" } + } + + /** + * An algorithm that derives one or more keys from an input value. + */ + abstract class KeyDerivationAlgorithm extends Algorithm { + abstract override string getAlgorithmName(); + } + + /** + * HKDF key derivation function + */ + abstract class HKDF extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "HKDF" } + + abstract HashAlgorithm getHashAlgorithm(); + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "digest" and result = this.getHashAlgorithm() + } + } + + /** + * PKCS #12 key derivation function + */ + abstract class PKCS12KDF extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "PKCS12KDF" } + + abstract HashAlgorithm getHashAlgorithm(); + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "digest" and result = this.getHashAlgorithm() + } + } + + newtype TEllipticCurveFamilyType = + // We're saying by this that all of these have an identical interface / properties / edges + NIST() or + SEC() or + NUMS() or + PRIME() or + BRAINPOOL() or + CURVE25519() or + CURVE448() or + C2() or + SM2() or + ES() or + OtherEllipticCurveFamilyType() + + + /** + * Elliptic curve algorithm + */ + abstract class EllipticCurve extends Algorithm { + + + abstract string getKeySize(Location location); + + abstract TEllipticCurveFamilyType getCurveFamilyType(); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + key = "key_size" and + if exists(this.getKeySize(location)) + then value = this.getKeySize(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + // other properties, like field type are possible, but not modeled until considered necessary + } + + override string getAlgorithmName() { result = this.getRawAlgorithmName().toUpperCase()} + + /** + * Mandating that for Elliptic Curves specifically, users are responsible + * for providing as the 'raw' name, the official name of the algorithm. + * Casing doesn't matter, we will enforce further naming restrictions on + * `getAlgorithmName` by default. + * Rationale: elliptic curve names can have a lot of variation in their components + * (e.g., "secp256r1" vs "P-256"), trying to produce generalized set of properties + * is possible to capture all cases, but such modeling is likely not necessary. + * if all properties need to be captured, we can reassess how names are generated. + */ + override abstract string getRawAlgorithmName(); + } +} diff --git a/python/ql/lib/experimental/Quantum/Language.qll b/python/ql/lib/experimental/Quantum/Language.qll new file mode 100644 index 000000000000..9abf3e7fa7e4 --- /dev/null +++ b/python/ql/lib/experimental/Quantum/Language.qll @@ -0,0 +1,12 @@ +private import Base +private import python as Lang + +module CryptoInput implements InputSig { + class LocatableElement = Lang::Expr; + + class UnknownLocation = Lang::UnknownDefaultLocation; +} + +module Crypto = CryptographyBase; + +import PycaCryptography diff --git a/python/ql/lib/experimental/Quantum/PycaCryptography.qll b/python/ql/lib/experimental/Quantum/PycaCryptography.qll new file mode 100644 index 000000000000..802ad23cf9d9 --- /dev/null +++ b/python/ql/lib/experimental/Quantum/PycaCryptography.qll @@ -0,0 +1,55 @@ +import python +import semmle.python.ApiGraphs + +module PycaCryptographyModule { + import Language + + /** + * Gets a predefined curve class constructor call from + * `cryptography.hazmat.primitives.asymmetric.ec` + * https://cryptography.io/en/latest/hazmat/primitives/asymmetric/ec/#elliptic-curves + */ + DataFlow::Node predefinedCurveClass(string rawName, string curveName, Crypto::TEllipticCurveFamilyType family, int keySize) { + // getACall since the typical case is to construct the curve with initialization values, + // not to pass the mode uninitialized + result = + API::moduleImport("cryptography") + .getMember("hazmat") + .getMember("primitives") + .getMember("asymmetric") + .getMember("ec") + .getMember(rawName) + .getACall() + and + curveName = rawName.toUpperCase() + and + curveName.matches("SEC%") and family instanceof Crypto::SEC + and + curveName.matches("BRAINPOOL%") and family instanceof Crypto::BRAINPOOL + and + // Enumerating all key sizes known in the API + // TODO: should we dynamically extract them through a regex? + keySize in [160, 163, 192, 224, 233, 256, 283, 320, 384, 409, 512, 571] + and + curveName.matches("%" + keySize + "%") + } + + + class EllipticCurve extends Crypto::EllipticCurve instanceof Expr{ + int keySize; + string rawName; + string curveName; + Crypto::TEllipticCurveFamilyType family; + EllipticCurve() { + this = predefinedCurveClass(rawName, curveName, family, keySize).asExpr() + } + + override string getRawAlgorithmName() { result = rawName } + override string getAlgorithmName() { result = curveName } + Crypto::TEllipticCurveFamilyType getFamily() { result = family } + + override string getKeySize(Location location) { + location = this and + result = keySize.toString() } + } +} diff --git a/python/ql/lib/semmle/python/Files.qll b/python/ql/lib/semmle/python/Files.qll index 2da0dd61f885..67f21ad0b249 100644 --- a/python/ql/lib/semmle/python/Files.qll +++ b/python/ql/lib/semmle/python/Files.qll @@ -368,3 +368,40 @@ class EncodingError extends SyntaxError { override string toString() { result = "Encoding Error" } } + + + +/** + * A dummy location which is used when something doesn't have a location in + * the source code but needs to have a `Location` associated with it. There + * may be several distinct kinds of unknown locations. For example: one for + * expressions, one for statements and one for other program elements. + */ +class UnknownLocation extends Location { + UnknownLocation() { this.getFile().getAbsolutePath() = "" } +} + +/** + * A dummy location which is used when something doesn't have a location in + * the source code but needs to have a `Location` associated with it. + */ +class UnknownDefaultLocation extends UnknownLocation { + UnknownDefaultLocation() { locations_default(this, _, 0, 0, 0, 0) } +} + +/** + * A dummy location which is used when an expression doesn't have a + * location in the source code but needs to have a `Location` associated + * with it. + */ +class UnknownExprLocation extends UnknownLocation { + UnknownExprLocation() { locations_default(this, _, 0, 0, 0, 0) } +} + +/** + * A dummy location which is used when a statement doesn't have a location + * in the source code but needs to have a `Location` associated with it. + */ +class UnknownStmtLocation extends UnknownLocation { + UnknownStmtLocation() { locations_default(this, _, 0, 0, 0, 0) } +} From 9af18bc1002e4b32b18a8f56d2fbf9c2ffa7405f Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Wed, 29 Jan 2025 19:45:04 +0100 Subject: [PATCH 06/28] WIP: add dgml/dot output/remove test code --- cpp/ql/lib/experimental/Quantum/Base.qll | 4 +- .../lib/experimental/Quantum/BaseBackup.qll | 125 ------------------ cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 10 -- cpp/ql/src/experimental/Quantum/CBOMGraph.ql | 47 +++++++ cpp/ql/src/experimental/Quantum/Test.ql | 43 ------ cpp/ql/src/experimental/Quantum/cbom.sh | 8 ++ .../src/experimental/Quantum/generate_cbom.py | 104 +++++++++++++++ 7 files changed, 162 insertions(+), 179 deletions(-) delete mode 100644 cpp/ql/lib/experimental/Quantum/BaseBackup.qll create mode 100644 cpp/ql/src/experimental/Quantum/CBOMGraph.ql delete mode 100644 cpp/ql/src/experimental/Quantum/Test.ql create mode 100755 cpp/ql/src/experimental/Quantum/cbom.sh create mode 100644 cpp/ql/src/experimental/Quantum/generate_cbom.py diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/cpp/ql/lib/experimental/Quantum/Base.qll index b3f4d619f4d8..cb0f53f468e7 100644 --- a/cpp/ql/lib/experimental/Quantum/Base.qll +++ b/cpp/ql/lib/experimental/Quantum/Base.qll @@ -51,7 +51,9 @@ module CryptographyBase Input> { * This predicate is used by derived classes to construct the graph of cryptographic operations. */ predicate properties(string key, string value, Location location) { - key = "origin" and location = this.getOrigin(value).getLocation() + key = "origin" and + location = this.getOrigin(value).getLocation() and + not location = this.getLocation() } /** diff --git a/cpp/ql/lib/experimental/Quantum/BaseBackup.qll b/cpp/ql/lib/experimental/Quantum/BaseBackup.qll deleted file mode 100644 index 821c89eb8f57..000000000000 --- a/cpp/ql/lib/experimental/Quantum/BaseBackup.qll +++ /dev/null @@ -1,125 +0,0 @@ -/** - * A language-independent library for reasoning about cryptography. - */ - -import codeql.util.Location -import codeql.util.Option - -signature module InputSig { - class KnownUnknownLocation extends Location; - - class LocatableElement { - Location getLocation(); - } -} - -// An operation = a specific loc in code -// An algorithm -// Properties -// Node -> Operation -> Algorithm -> Symmetric -> SpecificSymmetricAlgo -// -[Language-Specific]-> LibrarySymmetricAlgo -> Properties -// For example (nsted newtypes): -/* - * newtype for each algo, and each one of those would have params for their properties - * implementation: optional/range for example - * - * - * - * /** - * Constructs an `Option` type that is a disjoint union of the given type and an - * additional singleton element. - */ - -module CryptographyBase Input> { - newtype TNode = - TNodeUnknown() or - TNodeAlgorithm() or - TNodeOperation() - - /* - * A cryptographic asset in code, i.e., an algorithm, operation, property, or known unknown. - */ - - abstract class Node extends TNode { - // this would then extend LanguageNode - abstract Location getLocation(); - - abstract string toString(); - - abstract Node getChild(int childIndex); - - final Node getAChild() { result = this.getChild(_) } - - final Node getAParent() { result.getAChild() = this } - } - - final class KnownUnknown extends Node, TNodeUnknown { - override string toString() { result = "unknown" } - - override Node getChild(int childIndex) { none() } - - override Location getLocation() { result instanceof Input::KnownUnknownLocation } - } - - abstract class Operation extends Node, TNodeOperation { - /** - * Gets the algorithm associated with this operation. - */ - abstract Node getAlgorithm(); - - /** - * Gets the name of this operation, e.g., "hash" or "encrypt". - */ - abstract string getOperationName(); - - final override Node getChild(int childIndex) { childIndex = 0 and result = this.getAlgorithm() } - - final override string toString() { result = this.getOperationName() } - } - - abstract class Algorithm extends Node, TNodeAlgorithm { - /** - * Gets the name of this algorithm, e.g., "AES" or "SHA". - */ - abstract string getAlgorithmName(); - } - - /** - * A hashing operation that processes data to generate a hash value. - * This operation takes an input message of arbitrary content and length and produces a fixed-size - * hash value as the output using a specified hashing algorithm. - */ - abstract class HashOperation extends Operation { - abstract override HashAlgorithm getAlgorithm(); - - override string getOperationName() { result = "hash" } - } - - /** - * A hashing algorithm that transforms variable-length input into a fixed-size hash value. - */ - abstract class HashAlgorithm extends Algorithm { } - - /** - * An operation that derives one or more keys from an input value. - */ - abstract class KeyDerivationOperation extends Operation { - override string getOperationName() { result = "key derivation" } - } - - /** - * An algorithm that derives one or more keys from an input value. - */ - abstract class KeyDerivationAlgorithm extends Algorithm { - abstract override string getAlgorithmName(); - } - - /** - * HKDF Extract+Expand key derivation function. - */ - abstract class HKDFAlgorithm extends KeyDerivationAlgorithm { - final override string getAlgorithmName() { result = "HKDF" } - - abstract Node getDigestAlgorithm(); - } -} diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll index 852fedf646a8..18feda6c8c6c 100644 --- a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -84,16 +84,6 @@ module OpenSSLModel { } } - class TestKeyDerivationOperationHacky extends KeyDerivationOperation instanceof FunctionCall { - HKDF hkdf; - - TestKeyDerivationOperationHacky() { - this.getEnclosingFunction() = hkdf.(Expr).getEnclosingFunction() - } - - override Crypto::KeyDerivationAlgorithm getAlgorithm() { result = hkdf } - } - class PKCS12KDF extends KeyDerivationAlgorithm, Crypto::PKCS12KDF instanceof Expr { KDFAlgorithmStringLiteral origin; diff --git a/cpp/ql/src/experimental/Quantum/CBOMGraph.ql b/cpp/ql/src/experimental/Quantum/CBOMGraph.ql new file mode 100644 index 000000000000..1df6611aab9a --- /dev/null +++ b/cpp/ql/src/experimental/Quantum/CBOMGraph.ql @@ -0,0 +1,47 @@ +/** + * @name "Outputs a graph representation of the cryptographic bill of materials." + * @kind graph + * @id cbomgraph + */ + +import experimental.Quantum.Language + +string getPropertyString(Crypto::NodeBase node, string key) { + result = + strictconcat(any(string value, Location location, string parsed | + node.properties(key, value, location) and + parsed = "(" + value + "," + location.toString() + ")" + | + parsed + ), "," + ) +} + +string getLabel(Crypto::NodeBase node) { result = node.toString() } + +query predicate nodes(Crypto::NodeBase node, string key, string value) { + key = "semmle.label" and + value = getLabel(node) + or + // CodeQL's DGML output does not include a location + key = "Location" and + value = node.getLocation().toString() + or + // Known unknown edges should be reported as properties rather than edges + node = node.getChild(key) and + value = "" + or + // Report properties + value = getPropertyString(node, key) +} + +query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { + key = "semmle.label" and + target = source.getChild(value) and + // Known unknowns are reported as properties rather than edges + not source = target +} + +query predicate graphProperties(string key, string value) { + key = "semmle.graphKind" and value = "graph" +} diff --git a/cpp/ql/src/experimental/Quantum/Test.ql b/cpp/ql/src/experimental/Quantum/Test.ql deleted file mode 100644 index 87341a6b612c..000000000000 --- a/cpp/ql/src/experimental/Quantum/Test.ql +++ /dev/null @@ -1,43 +0,0 @@ -/** - * @name "PQC Test" - * @kind graph - */ - -import experimental.Quantum.Language - -string getValueAndLocationPairs(Crypto::NodeBase node, string key) { - exists(string value, Location location | - node.properties(key, value, location) and - result = "(" + value + "," + location.toString() + ")" - ) -} - -string properties(Crypto::NodeBase node) { - forex(string key | node.properties(key, _, _) | - result = key + ":" + strictconcat(getValueAndLocationPairs(node, key), ",") - ) -} - -string getLabel(Crypto::NodeBase node) { - result = - "[" + node.toString() + "]" + - any(string prop | - if exists(properties(node)) then prop = " " + properties(node) else prop = "" - | - prop - ) -} - -query predicate nodes(Crypto::NodeBase node, string key, string value) { - key = "semmle.label" and - value = getLabel(node) -} - -query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { - target = source.getChild(value) and - key = "semmle.label" -} - -query predicate graphProperties(string key, string value) { - key = "semmle.graphKind" and value = "tree" -} diff --git a/cpp/ql/src/experimental/Quantum/cbom.sh b/cpp/ql/src/experimental/Quantum/cbom.sh new file mode 100755 index 000000000000..df1c58b1efb8 --- /dev/null +++ b/cpp/ql/src/experimental/Quantum/cbom.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +CODEQL_PATH="/Users/nicolaswill/Library/Application Support/Code/User/globalStorage/github.vscode-codeql/distribution5/codeql/codeql" +DATABASE_PATH="/Users/nicolaswill/openssl_codeql/openssl/openssl_db" +QUERY_FILE="CBOMGraph.ql" +OUTPUT_DIR="graph_output" + +python3 generate_cbom.py -c "$CODEQL_PATH" -d "$DATABASE_PATH" -q "$QUERY_FILE" -o "$OUTPUT_DIR" diff --git a/cpp/ql/src/experimental/Quantum/generate_cbom.py b/cpp/ql/src/experimental/Quantum/generate_cbom.py new file mode 100644 index 000000000000..10ec895dc629 --- /dev/null +++ b/cpp/ql/src/experimental/Quantum/generate_cbom.py @@ -0,0 +1,104 @@ +#!/usr/bin/env python3 + +import os +import sys +import argparse +import subprocess +import xml.etree.ElementTree as ET + +def run_codeql_analysis(codeql_path, database_path, query_path, output_dir): + """Runs the CodeQL analysis and generates a DGML file.""" + os.makedirs(output_dir, exist_ok=True) + command = [ + codeql_path, "database", "analyze", database_path, query_path, + "--rerun", "--format=dgml", "--output", output_dir + ] + + print(f"Running CodeQL analysis: {' '.join(command)}") + result = subprocess.run(command, capture_output=True, text=True) + + if result.returncode == 0: + print("Analysis completed successfully.") + else: + print("Analysis failed.") + print(result.stderr) + sys.exit(1) + + return result.returncode + + +def convert_dgml_to_dot(dgml_file, dot_file): + """Converts the DGML file to DOT format using the exact original implementation.""" + print(f"Processing DGML file: {dgml_file}") + + # Read source DGML + with open(dgml_file, "r", encoding="utf-8") as f: + xml_content = f.read() + + root = ET.fromstring(xml_content) + + # Form dot element sequence + body_l = ["digraph cbom {", + "node [shape=box];", + "rankdir=LR;" + ] + + # Process nodes + for node in root.find("{http://schemas.microsoft.com/vs/2009/dgml}Nodes"): + att = node.attrib + node_id = att['Id'] + label_parts = [] + for key, value in att.items(): + if key == 'Id': + continue + elif key == 'Label': + label_parts.append(value) + else: + label_parts.append(f"{key}={value}") + label = "\\n".join(label_parts) + prop_l = [f'label="{label}"'] + node_s = f'nd_{node_id} [{", ".join(prop_l)}];' + body_l.append(node_s) + + # Process edges + for edge in root.find("{http://schemas.microsoft.com/vs/2009/dgml}Links"): + att = edge.attrib + edge_s = 'nd_{} -> nd_{} [label="{}"];'.format( + att["Source"], att["Target"], att.get("Label", "")) + body_l.append(edge_s) + + body_l.append("}") + + # Write DOT output + with open(dot_file, "w", encoding="utf-8") as f: + f.write("\n".join(body_l)) + + print(f"DGML file successfully converted to DOT format: {dot_file}") + + +def main(): + parser = argparse.ArgumentParser(description="Run CodeQL analysis and convert DGML to DOT.") + 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("-o", "--output", required=True, help="Output directory for analysis results.") + + args = parser.parse_args() + + # Run CodeQL analysis + run_codeql_analysis(args.codeql, args.database, args.query, args.output) + + # Locate DGML file + dgml_file = os.path.join(args.output, "cbomgraph.dgml") + dot_file = dgml_file.replace(".dgml", ".dot") + + if os.path.exists(dgml_file): + # Convert DGML to DOT + convert_dgml_to_dot(dgml_file, dot_file) + else: + print(f"No DGML file found in {args.output}.") + sys.exit(1) + + +if __name__ == "__main__": + main() From 69a63855cc07c7a5d4b0b48f2e4b3f51b274ed3a Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Wed, 29 Jan 2025 21:55:57 +0100 Subject: [PATCH 07/28] Update CBOMGraph.ql --- cpp/ql/src/experimental/Quantum/CBOMGraph.ql | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpp/ql/src/experimental/Quantum/CBOMGraph.ql b/cpp/ql/src/experimental/Quantum/CBOMGraph.ql index 1df6611aab9a..edcc40aca6a4 100644 --- a/cpp/ql/src/experimental/Quantum/CBOMGraph.ql +++ b/cpp/ql/src/experimental/Quantum/CBOMGraph.ql @@ -1,5 +1,6 @@ /** - * @name "Outputs a graph representation of the cryptographic bill of materials." + * @name "Print CBOM Graph" + * @description "Outputs a graph representation of the cryptographic bill of materials." * @kind graph * @id cbomgraph */ From 5f355c7f555748cb47b9cbaab862a0a05daf211c Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Tue, 4 Feb 2025 11:55:09 -0500 Subject: [PATCH 08/28] Add first sample JCA encryption model --- java/ql/lib/experimental/Quantum/Base.qll | 235 ++++++++++++++++++ java/ql/lib/experimental/Quantum/JCA.qll | 105 ++++++++ java/ql/lib/experimental/Quantum/Language.qll | 30 +++ java/ql/src/experimental/Quantum/Test.ql | 13 + 4 files changed, 383 insertions(+) create mode 100644 java/ql/lib/experimental/Quantum/Base.qll create mode 100644 java/ql/lib/experimental/Quantum/JCA.qll create mode 100644 java/ql/lib/experimental/Quantum/Language.qll create mode 100644 java/ql/src/experimental/Quantum/Test.ql diff --git a/java/ql/lib/experimental/Quantum/Base.qll b/java/ql/lib/experimental/Quantum/Base.qll new file mode 100644 index 000000000000..bbcd60ee891a --- /dev/null +++ b/java/ql/lib/experimental/Quantum/Base.qll @@ -0,0 +1,235 @@ +/** + * A language-independent library for reasoning about cryptography. + */ + + import codeql.util.Location + import codeql.util.Option + + signature module InputSig { + class LocatableElement { + Location getLocation(); + } + + class UnknownLocation instanceof Location; + } + + module CryptographyBase Input> { + final class LocatableElement = Input::LocatableElement; + + final class UnknownLocation = Input::UnknownLocation; + + final class UnknownPropertyValue extends string { + UnknownPropertyValue() { this = "" } + } + + abstract class NodeBase instanceof LocatableElement { + /** + * Returns a string representation of this node, usually the name of the operation/algorithm/property. + */ + abstract string toString(); + + /** + * Returns the location of this node in the code. + */ + Location getLocation() { result = super.getLocation() } + + /** + * Gets the origin of this node, e.g., a string literal in source describing it. + */ + LocatableElement getOrigin(string value) { none() } + + /** + * Returns the child of this node with the given edge name. + * + * This predicate is used by derived classes to construct the graph of cryptographic operations. + */ + NodeBase getChild(string edgeName) { none() } + + /** + * Defines properties of this node by name and either a value or location or both. + * + * This predicate is used by derived classes to construct the graph of cryptographic operations. + */ + predicate properties(string key, string value, Location location) { + key = "origin" and location = this.getOrigin(value).getLocation() + } + + /** + * Returns the parent of this node. + */ + final NodeBase getAParent() { result.getChild(_) = this } + } + + class Asset = NodeBase; + + /** + * A cryptographic operation, such as hashing or encryption. + */ + abstract class Operation extends Asset { + /** + * Gets the algorithm associated with this operation. + */ + abstract Algorithm getAlgorithm(); + + /** + * Gets the name of this operation, e.g., "hash" or "encrypt". + */ + abstract string getOperationName(); + + final override string toString() { result = this.getOperationName() } + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "uses" and + if exists(this.getAlgorithm()) then result = this.getAlgorithm() else result = this + } + } + + abstract class Algorithm extends Asset { + /** + * Gets the name of this algorithm, e.g., "AES" or "SHA". + */ + abstract string getAlgorithmName(); + + final override string toString() { result = this.getAlgorithmName() } + } + + /** + * A hashing operation that processes data to generate a hash value. + * This operation takes an input message of arbitrary content and length and produces a fixed-size + * hash value as the output using a specified hashing algorithm. + */ + abstract class HashOperation extends Operation { + abstract override HashAlgorithm getAlgorithm(); + + override string getOperationName() { result = "HASH" } + } + + // Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces + // + // Example: HKDF and PKCS12KDF are both key derivation algorithms. + // However, PKCS12KDF also has a property: the iteration count. + // + // If we have HKDF and PKCS12KDF under TKeyDerivationType, + // someone modelling a library might try to make a generic identification of both of those algorithms. + // + // They will therefore not use the specialized type for PKCS12KDF, + // meaning "from PKCS12KDF algo select algo" will have no results. + // + newtype THashType = + // We're saying by this that all of these have an identical interface / properties / edges + MD5() or + SHA1() or + SHA256() or + SHA512() or + OtherHashType() + + /** + * A hashing algorithm that transforms variable-length input into a fixed-size hash value. + */ + abstract class HashAlgorithm extends Algorithm { + final predicate hashTypeToNameMapping(THashType type, string name) { + type instanceof MD5 and name = "MD5" + or + type instanceof SHA1 and name = "SHA-1" + or + type instanceof SHA256 and name = "SHA-256" + or + type instanceof SHA512 and name = "SHA-512" + or + type instanceof OtherHashType and name = this.getRawAlgorithmName() + } + + abstract THashType getHashType(); + + override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } + + /** + * Gets the raw name of this hash algorithm from source. + */ + abstract string getRawAlgorithmName(); + } + + /** + * An operation that derives one or more keys from an input value. + */ + abstract class KeyDerivationOperation extends Operation { + override string getOperationName() { result = "KEY_DERIVATION" } + } + + /** + * An algorithm that derives one or more keys from an input value. + */ + abstract class KeyDerivationAlgorithm extends Algorithm { + abstract override string getAlgorithmName(); + } + + /** + * HKDF key derivation function + */ + abstract class HKDF extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "HKDF" } + + abstract HashAlgorithm getHashAlgorithm(); + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "digest" and result = this.getHashAlgorithm() + } + } + + /** + * PKCS #12 key derivation function + */ + abstract class PKCS12KDF extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "PKCS12KDF" } + + abstract HashAlgorithm getHashAlgorithm(); + + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + edgeName = "digest" and result = this.getHashAlgorithm() + } + } + + /** + * Elliptic curve algorithm + */ + abstract class EllipticCurve extends Algorithm { + abstract string getVersion(Location location); + + abstract string getKeySize(Location location); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + key = "version" and + if exists(this.getVersion(location)) + then value = this.getVersion(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + or + key = "key_size" and + if exists(this.getKeySize(location)) + then value = this.getKeySize(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + } + } + + /** + * An encryption operation that processes plaintext to generate a ciphertext. + * This operation takes an input message (plaintext) of arbitrary content and length and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). + */ + abstract class EncryptionOperation extends Operation { + abstract override Algorithm getAlgorithm(); + + override string getOperationName() { result = "ENCRYPTION" } + } + } + \ No newline at end of file diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll new file mode 100644 index 000000000000..bef648d290a1 --- /dev/null +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -0,0 +1,105 @@ +import java +import semmle.code.java.dataflow.DataFlow + +module JCAModel { + import Language + + abstract class EncryptionOperation extends Crypto::EncryptionOperation { } + + //TODO PBEWith can have suffixes. how to do? enumerate? or match a pattern? +predicate cipher_names(string algo) { algo = ["AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", "DES", "DESede", "DESedeWrap", "ECIES", "PBEWith", "RC2", "RC4", "RC5", "RSA"] } +//TODO solve the fact that x is an int of various values. same as above... enumerate? +predicate cipher_modes(string mode) {mode = ["NONE", "CBC", "CCM", "CFB", "CFBx", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB", "OFBx", "PCBC"]} +//todo same as above, OAEPWith has asuffix type +predicate cipher_padding(string padding) {padding = ["NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", "SSL3Padding"]} + + /** + * Symmetric algorithms + */ + abstract class SymmetricAlgorithm extends Crypto::Algorithm { + + + //TODO figure out how to get this from the Cipher interface, is it explicit? + //abstract string getKeySize(Location location); + + // override predicate properties(string key, string value, Location location) { + // super.properties(key, value, location) + // or + // key = "key_size" and + // if exists(this.getKeySize(location)) + // then value = this.getKeySize(location) + // else ( + // value instanceof Crypto::UnknownPropertyValue and location instanceof UnknownLocation + // ) + // // other properties, like field type are possible, but not modeled until considered necessary + // } + + abstract override string getAlgorithmName(); +} + +////cipher specifics ---------------------------------------- + +class CipherInstance extends Call { + CipherInstance() { this.getCallee().hasQualifiedName("javax.crypto","Cipher", "getInstance") } + + Expr getAlgorithmArg() { result = this.getArgument(0) } + } + +class CipherAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLiteral { + CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/"))} + + override string toString() { result = this.(StringLiteral).toString() } + + string getValue() { result = this.(StringLiteral).getValue() } + } + + class CipherAlgorithmModeStringLiteral extends Crypto::NodeBase instanceof StringLiteral { + CipherAlgorithmModeStringLiteral() { cipher_modes(this.getValue().splitAt("/"))} + + override string toString() { result = this.(StringLiteral).toString() } + + string getValue() { result = this.(StringLiteral).getValue() } + } + + class CipherAlgorithmPaddingStringLiteral extends Crypto::NodeBase instanceof StringLiteral { + CipherAlgorithmPaddingStringLiteral() { cipher_padding(this.getValue().splitAt("/"))} + + override string toString() { result = this.(StringLiteral).toString() } + + string getValue() { result = this.(StringLiteral).getValue() } + } + + private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherAlgorithmStringLiteral } + + predicate isSink(DataFlow::Node sink) { + exists(CipherInstance call | sink.asExpr() = call.getAlgorithmArg()) + } + } + + module AlgorithmStringToFetchFlow = DataFlow::Global; + + predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, Expr arg) { + exists(CipherInstance sinkCall | + origin.getValue().toUpperCase() = name and + arg = sinkCall.getAlgorithmArg() and + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) + ) + } + + class AES extends SymmetricAlgorithm instanceof Expr { + CipherAlgorithmStringLiteral origin; + + AES() { algorithmStringToCipherInstanceArgFlow("AES", origin, this) } + + override Crypto::LocatableElement getOrigin(string name) { + result = origin and name = origin.toString() + } + + override string getAlgorithmName(){ result = "AES"} + } + + + + +} \ No newline at end of file diff --git a/java/ql/lib/experimental/Quantum/Language.qll b/java/ql/lib/experimental/Quantum/Language.qll new file mode 100644 index 000000000000..246f2b86367c --- /dev/null +++ b/java/ql/lib/experimental/Quantum/Language.qll @@ -0,0 +1,30 @@ +private import Base +private import java as Lang + +/** + * A dummy location which is used when something doesn't have a location in + * the source code but needs to have a `Location` associated with it. There + * may be several distinct kinds of unknown locations. For example: one for + * expressions, one for statements and one for other program elements. + */ +class UnknownLocation extends Location { + UnknownLocation() { this.getFile().getAbsolutePath() = "" } +} + +/** + * A dummy location which is used when something doesn't have a location in + * the source code but needs to have a `Location` associated with it. + */ +class UnknownDefaultLocation extends UnknownLocation { + UnknownDefaultLocation() { locations_default(this, _, 0, 0, 0, 0) } +} + +module CryptoInput implements InputSig { + class LocatableElement = Lang::Element; + + class UnknownLocation = UnknownDefaultLocation; +} + +module Crypto = CryptographyBase; + +import JCA diff --git a/java/ql/src/experimental/Quantum/Test.ql b/java/ql/src/experimental/Quantum/Test.ql new file mode 100644 index 000000000000..672ad14e5dfa --- /dev/null +++ b/java/ql/src/experimental/Quantum/Test.ql @@ -0,0 +1,13 @@ +/** + * @name "PQC Test" + */ + + import experimental.Quantum.Language + //import java + + from Crypto::NodeBase node + select node + +// from Class t +// where t.hasQualifiedName("javax.crypto", "CipherSpi") +// select t, t.getADescendant*() \ No newline at end of file From 86e51dad8a4d2ead6638f1d5cfb0f54309bf81fa Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Wed, 5 Feb 2025 13:39:48 -0500 Subject: [PATCH 09/28] Improve JCA aes alg model, add test --- java/ql/lib/experimental/Quantum/JCA.qll | 58 ++++++++++++++++++------ java/ql/src/experimental/Quantum/Test.ql | 9 +--- 2 files changed, 45 insertions(+), 22 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index bef648d290a1..fae5c4f806e9 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -13,6 +13,18 @@ predicate cipher_modes(string mode) {mode = ["NONE", "CBC", "CCM", "CFB", "CFBx" //todo same as above, OAEPWith has asuffix type predicate cipher_padding(string padding) {padding = ["NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", "SSL3Padding"]} + +abstract class BlockCiper extends Crypto::Algorithm { + CipherAlgorithmStringLiteral alg; + CipherAlgorithmMode mode; + CipherAlgorithmPadding padding; + + + CipherAlgorithmStringLiteral getAlg() {result = alg } + CipherAlgorithmMode getMode() {result = mode } + + CipherAlgorithmPadding getPadding() {result =padding} +} /** * Symmetric algorithms */ @@ -45,6 +57,9 @@ class CipherInstance extends Call { Expr getAlgorithmArg() { result = this.getArgument(0) } } + /** + * this may be specified either in the ALG/MODE/PADDING or just ALG format + */ class CipherAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLiteral { CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/"))} @@ -53,20 +68,28 @@ class CipherAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLit string getValue() { result = this.(StringLiteral).getValue() } } - class CipherAlgorithmModeStringLiteral extends Crypto::NodeBase instanceof StringLiteral { - CipherAlgorithmModeStringLiteral() { cipher_modes(this.getValue().splitAt("/"))} +abstract class CipherAlgorithmMode extends Crypto::NodeBase { + string getValue() {result = ""} +} + + class CipherAlgorithmModeStringLiteral extends CipherAlgorithmMode instanceof StringLiteral { + CipherAlgorithmModeStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/"))} override string toString() { result = this.(StringLiteral).toString() } - string getValue() { result = this.(StringLiteral).getValue() } + override string getValue() { result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*",1) } } - class CipherAlgorithmPaddingStringLiteral extends Crypto::NodeBase instanceof StringLiteral { - CipherAlgorithmPaddingStringLiteral() { cipher_padding(this.getValue().splitAt("/"))} + abstract class CipherAlgorithmPadding extends Crypto::NodeBase { + string getValue() {result = ""} + } + + class CipherAlgorithmPaddingStringLiteral extends CipherAlgorithmPadding instanceof StringLiteral { + CipherAlgorithmPaddingStringLiteral() { cipher_padding(this.(StringLiteral).getValue().splitAt("/"))} override string toString() { result = this.(StringLiteral).toString() } - string getValue() { result = this.(StringLiteral).getValue() } + override string getValue() { result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)",1) } } private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { @@ -79,27 +102,32 @@ class CipherAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLit module AlgorithmStringToFetchFlow = DataFlow::Global; - predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, Expr arg) { + predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, CipherAlgorithmModeStringLiteral mode, CipherAlgorithmPaddingStringLiteral padding, Expr arg) { exists(CipherInstance sinkCall | - origin.getValue().toUpperCase() = name and + origin.getValue().splitAt("/") = name and + origin = mode and + origin = padding and arg = sinkCall.getAlgorithmArg() and AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) ) } - class AES extends SymmetricAlgorithm instanceof Expr { - CipherAlgorithmStringLiteral origin; + /** + * A class to represent when AES is used AND it has literal mode and padding provided + * this does not capture the use without + */ + class AESLiteral extends SymmetricAlgorithm, BlockCiper instanceof Expr { - AES() { algorithmStringToCipherInstanceArgFlow("AES", origin, this) } + + AESLiteral() { algorithmStringToCipherInstanceArgFlow("AES", alg, mode, padding, this) +} override Crypto::LocatableElement getOrigin(string name) { - result = origin and name = origin.toString() + result = alg and name = alg.toString() } - override string getAlgorithmName(){ result = "AES"} + override string getAlgorithmName(){ result = this.getAlgorithmName()} } - - } \ No newline at end of file diff --git a/java/ql/src/experimental/Quantum/Test.ql b/java/ql/src/experimental/Quantum/Test.ql index 672ad14e5dfa..f35336a846f2 100644 --- a/java/ql/src/experimental/Quantum/Test.ql +++ b/java/ql/src/experimental/Quantum/Test.ql @@ -3,11 +3,6 @@ */ import experimental.Quantum.Language - //import java - from Crypto::NodeBase node - select node - -// from Class t -// where t.hasQualifiedName("javax.crypto", "CipherSpi") -// select t, t.getADescendant*() \ No newline at end of file +from JCAModel::AESLiteral l +select l, l.getAlg(), l.getMode().getValue(), l.getPadding().getValue() \ No newline at end of file From efcf7eab0cad504376e19ea96145007df3d929a5 Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Wed, 5 Feb 2025 17:24:25 -0500 Subject: [PATCH 10/28] Add broken crypto query --- java/ql/lib/experimental/Quantum/JCA.qll | 2 +- .../src/experimental/Quantum/BrokenCrypto.ql | 77 +++++++++++++++++++ 2 files changed, 78 insertions(+), 1 deletion(-) create mode 100644 java/ql/src/experimental/Quantum/BrokenCrypto.ql diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index fae5c4f806e9..8a613b66d022 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -126,7 +126,7 @@ abstract class CipherAlgorithmMode extends Crypto::NodeBase { result = alg and name = alg.toString() } - override string getAlgorithmName(){ result = this.getAlgorithmName()} + override string getAlgorithmName(){ result = alg.getValue()} } diff --git a/java/ql/src/experimental/Quantum/BrokenCrypto.ql b/java/ql/src/experimental/Quantum/BrokenCrypto.ql new file mode 100644 index 000000000000..020ac1b8925a --- /dev/null +++ b/java/ql/src/experimental/Quantum/BrokenCrypto.ql @@ -0,0 +1,77 @@ +/** +* @name Use of a broken or risky cryptographic algorithm +* @description Using broken or weak cryptographic algorithms can allow an attacker to compromise security. +* @kind problem +* @problem.severity warning +* @security-severity 7.5 +* @precision high +* @id java/weak-cryptographic-algorithm-new-model +* @tags security +* external/cwe/cwe-327 +* external/cwe/cwe-328 +*/ + + + +//THIS QUERY IS A REPLICA OF: https://github.com/github/codeql/blob/main/java/ql/src/Security/CWE/CWE-327/BrokenCryptoAlgorithm.ql +//but uses the **NEW MODELLING** +import experimental.Quantum.Language + + +/** + * Gets the name of an algorithm that is known to be insecure. + */ +string getAnInsecureAlgorithmName() { + result = + [ + "DES", "RC2", "RC4", "RC5", + // ARCFOUR is a variant of RC4 + "ARCFOUR", + // Encryption mode ECB like AES/ECB/NoPadding is vulnerable to replay and other attacks + "ECB", + // CBC mode of operation with PKCS#5 or PKCS#7 padding is vulnerable to padding oracle attacks + "AES/CBC/PKCS[57]Padding" + ] + } + + private string rankedInsecureAlgorithm(int i) { + result = rank[i](string s | s = getAnInsecureAlgorithmName()) + } + + private string insecureAlgorithmString(int i) { + i = 1 and result = rankedInsecureAlgorithm(i) + or + result = rankedInsecureAlgorithm(i) + "|" + insecureAlgorithmString(i - 1) + } + + /** + * Gets the regular expression used for matching strings that look like they + * contain an algorithm that is known to be insecure. + */ + string getInsecureAlgorithmRegex() { + result = algorithmRegex(insecureAlgorithmString(max(int i | exists(rankedInsecureAlgorithm(i))))) + } + + bindingset[algorithmString] +private string algorithmRegex(string algorithmString) { + // Algorithms usually appear in names surrounded by characters that are not + // alphabetical characters in the same case. This handles the upper and lower + // case cases. + result = + "((^|.*[^A-Z])(" + algorithmString + ")([^A-Z].*|$))" + + // or... + "|" + + // For lowercase, we want to be careful to avoid being confused by camelCase + // hence we require two preceding uppercase letters to be sure of a case switch, + // or a preceding non-alphabetic character + "((^|.*[A-Z]{2}|.*[^a-zA-Z])(" + algorithmString.toLowerCase() + ")([^a-z].*|$))" +} + +from Crypto::Algorithm alg +where alg.getAlgorithmName().regexpMatch(getInsecureAlgorithmRegex()) and +// Exclude RSA/ECB/.* ciphers. +not alg.getAlgorithmName().regexpMatch("RSA/ECB.*") and +// Exclude German and French sentences. +not alg.getAlgorithmName().regexpMatch(".*\\p{IsLowercase} des \\p{IsLetter}.*") +select alg, "Cryptographic algorithm $@ is weak and should not be used.", alg, +alg.getAlgorithmName() From 3dc28c2d17d95c9bdbf2e7127d365e3673770363 Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Thu, 6 Feb 2025 21:54:18 +0100 Subject: [PATCH 11/28] Move language-agnostic model to shared library --- cpp/ql/lib/experimental/Quantum/Language.qll | 2 +- cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 4 ++ cpp/ql/lib/qlpack.yml | 1 + .../scripts/cryptography}/cbom.sh | 2 +- .../scripts/cryptography}/generate_cbom.py | 0 .../codeql/cryptography/Model.qll | 44 +++++++++---------- shared/cryptography/qlpack.yml | 7 +++ 7 files changed, 34 insertions(+), 26 deletions(-) rename {cpp/ql/src/experimental/Quantum => misc/scripts/cryptography}/cbom.sh (79%) rename {cpp/ql/src/experimental/Quantum => misc/scripts/cryptography}/generate_cbom.py (100%) rename cpp/ql/lib/experimental/Quantum/Base.qll => shared/cryptography/codeql/cryptography/Model.qll (93%) create mode 100644 shared/cryptography/qlpack.yml diff --git a/cpp/ql/lib/experimental/Quantum/Language.qll b/cpp/ql/lib/experimental/Quantum/Language.qll index c9398c9e3245..8f400858f07c 100644 --- a/cpp/ql/lib/experimental/Quantum/Language.qll +++ b/cpp/ql/lib/experimental/Quantum/Language.qll @@ -1,4 +1,4 @@ -private import Base +private import codeql.cryptography.Model private import cpp as Lang module CryptoInput implements InputSig { diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll index 18feda6c8c6c..bf38e5c0ab5d 100644 --- a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -77,6 +77,8 @@ module OpenSSLModel { HKDF() { algorithmStringToKDFFetchArgFlow("HKDF", origin, this) } + override string getRawAlgorithmName() { result = origin.getValue() } + override Crypto::HashAlgorithm getHashAlgorithm() { none() } override Crypto::LocatableElement getOrigin(string name) { @@ -89,6 +91,8 @@ module OpenSSLModel { PKCS12KDF() { algorithmStringToKDFFetchArgFlow("PKCS12KDF", origin, this) } + override string getRawAlgorithmName() { result = origin.getValue() } + override Crypto::HashAlgorithm getHashAlgorithm() { none() } override Crypto::NodeBase getOrigin(string name) { diff --git a/cpp/ql/lib/qlpack.yml b/cpp/ql/lib/qlpack.yml index 6ffc77714d47..489de9f6cef4 100644 --- a/cpp/ql/lib/qlpack.yml +++ b/cpp/ql/lib/qlpack.yml @@ -6,6 +6,7 @@ extractor: cpp library: true upgrades: upgrades dependencies: + codeql/cryptography: ${workspace} codeql/dataflow: ${workspace} codeql/mad: ${workspace} codeql/rangeanalysis: ${workspace} diff --git a/cpp/ql/src/experimental/Quantum/cbom.sh b/misc/scripts/cryptography/cbom.sh similarity index 79% rename from cpp/ql/src/experimental/Quantum/cbom.sh rename to misc/scripts/cryptography/cbom.sh index df1c58b1efb8..9cbef951bbf4 100755 --- a/cpp/ql/src/experimental/Quantum/cbom.sh +++ b/misc/scripts/cryptography/cbom.sh @@ -2,7 +2,7 @@ CODEQL_PATH="/Users/nicolaswill/Library/Application Support/Code/User/globalStorage/github.vscode-codeql/distribution5/codeql/codeql" DATABASE_PATH="/Users/nicolaswill/openssl_codeql/openssl/openssl_db" -QUERY_FILE="CBOMGraph.ql" +QUERY_FILE="/Users/nicolaswill/pqc/codeql/cpp/ql/src/experimental/Quantum/CBOMGraph.ql" OUTPUT_DIR="graph_output" python3 generate_cbom.py -c "$CODEQL_PATH" -d "$DATABASE_PATH" -q "$QUERY_FILE" -o "$OUTPUT_DIR" diff --git a/cpp/ql/src/experimental/Quantum/generate_cbom.py b/misc/scripts/cryptography/generate_cbom.py similarity index 100% rename from cpp/ql/src/experimental/Quantum/generate_cbom.py rename to misc/scripts/cryptography/generate_cbom.py diff --git a/cpp/ql/lib/experimental/Quantum/Base.qll b/shared/cryptography/codeql/cryptography/Model.qll similarity index 93% rename from cpp/ql/lib/experimental/Quantum/Base.qll rename to shared/cryptography/codeql/cryptography/Model.qll index 68b3bc08cf70..eba25db60d24 100644 --- a/cpp/ql/lib/experimental/Quantum/Base.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -94,7 +94,7 @@ module CryptographyBase Input> { */ abstract string getAlgorithmName(); - /** + /** * Gets the raw name of this algorithm from source (no parsing or formatting) */ abstract string getRawAlgorithmName(); @@ -151,7 +151,6 @@ module CryptographyBase Input> { abstract THashType getHashType(); override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } - } /** @@ -199,26 +198,23 @@ module CryptographyBase Input> { } newtype TEllipticCurveFamilyType = - // We're saying by this that all of these have an identical interface / properties / edges - NIST() or - SEC() or - NUMS() or - PRIME() or - BRAINPOOL() or - CURVE25519() or - CURVE448() or - C2() or - SM2() or - ES() or - OtherEllipticCurveFamilyType() - + // We're saying by this that all of these have an identical interface / properties / edges + NIST() or + SEC() or + NUMS() or + PRIME() or + BRAINPOOL() or + CURVE25519() or + CURVE448() or + C2() or + SM2() or + ES() or + OtherEllipticCurveFamilyType() /** * Elliptic curve algorithm */ abstract class EllipticCurve extends Algorithm { - - abstract string getKeySize(Location location); abstract TEllipticCurveFamilyType getCurveFamilyType(); @@ -235,18 +231,18 @@ module CryptographyBase Input> { // other properties, like field type are possible, but not modeled until considered necessary } - override string getAlgorithmName() { result = this.getRawAlgorithmName().toUpperCase()} + override string getAlgorithmName() { result = this.getRawAlgorithmName().toUpperCase() } /** * Mandating that for Elliptic Curves specifically, users are responsible - * for providing as the 'raw' name, the official name of the algorithm. - * Casing doesn't matter, we will enforce further naming restrictions on - * `getAlgorithmName` by default. + * for providing as the 'raw' name, the official name of the algorithm. + * Casing doesn't matter, we will enforce further naming restrictions on + * `getAlgorithmName` by default. * Rationale: elliptic curve names can have a lot of variation in their components * (e.g., "secp256r1" vs "P-256"), trying to produce generalized set of properties - * is possible to capture all cases, but such modeling is likely not necessary. - * if all properties need to be captured, we can reassess how names are generated. + * is possible to capture all cases, but such modeling is likely not necessary. + * if all properties need to be captured, we can reassess how names are generated. */ - override abstract string getRawAlgorithmName(); + abstract override string getRawAlgorithmName(); } } diff --git a/shared/cryptography/qlpack.yml b/shared/cryptography/qlpack.yml new file mode 100644 index 000000000000..768c64a0704e --- /dev/null +++ b/shared/cryptography/qlpack.yml @@ -0,0 +1,7 @@ +name: codeql/cryptography +version: 0.0.0-dev +groups: shared +library: true +dependencies: + codeql/util: ${workspace} +warnOnImplicitThis: true \ No newline at end of file From 60d931af9f98ffda9185ed17bc17e9ad870887ab Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Fri, 7 Feb 2025 15:46:13 -0500 Subject: [PATCH 12/28] Update progress on JCA --- java/ql/lib/experimental/Quantum/Base.qll | 94 +++++++++++++++++++- java/ql/lib/experimental/Quantum/JCA.qll | 100 ++++++++++------------ 2 files changed, 136 insertions(+), 58 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/Base.qll b/java/ql/lib/experimental/Quantum/Base.qll index bbcd60ee891a..a14f3b6836ad 100644 --- a/java/ql/lib/experimental/Quantum/Base.qll +++ b/java/ql/lib/experimental/Quantum/Base.qll @@ -11,6 +11,8 @@ } class UnknownLocation instanceof Location; + + } module CryptographyBase Input> { @@ -91,6 +93,11 @@ * Gets the name of this algorithm, e.g., "AES" or "SHA". */ abstract string getAlgorithmName(); + + /** + * Gets the raw name of this algorithm from source (no parsing or formatting) + */ + abstract string getRawAlgorithmName(); final override string toString() { result = this.getAlgorithmName() } } @@ -148,7 +155,7 @@ /** * Gets the raw name of this hash algorithm from source. */ - abstract string getRawAlgorithmName(); + override abstract string getRawAlgorithmName(); } /** @@ -231,5 +238,90 @@ override string getOperationName() { result = "ENCRYPTION" } } + +// newtype TBlockCipherFamilyType = +// // We're saying by this that all of these have an identical interface / properties / edges +// CBC() or ECB() + + +// abstract class BlockCiper extends Algorithm { + +// abstract string getKeySize(Location location); + +// abstract TBlockCipherFamilyType getBlockCipherFamilyType(); + +// override predicate properties(string key, string value, Location location) { +// super.properties(key, value, location) +// or +// key = "key_size" and +// if exists(this.getKeySize(location)) +// then value = this.getKeySize(location) +// else ( +// value instanceof UnknownPropertyValue and location instanceof UnknownLocation +// ) +// // other properties, like field type are possible, but not modeled until considered necessary +// } + +// override string getAlgorithmName() { result = this.getRawAlgorithmName().toUpperCase()} + +// override abstract string getRawAlgorithmName(); +// } + +newtype TModeOperation = +ECB() or OtherMode() + +abstract class ModeOfOperation extends Algorithm { + string getValue() {result = ""} + + final private predicate modeToNameMapping(TModeOperation type, string name) { + type instanceof ECB and name = "ECB" + or + type instanceof OtherMode and name = this.getRawAlgorithmName() + } + + abstract TModeOperation getModeType(); + + override string getAlgorithmName() { this.modeToNameMapping(this.getModeType(), result) } + +} + +newtype TCipherStructure = +Block() or Stream() + + newtype TSymmetricCipherFamilyType = +// We're saying by this that all of these have an identical interface / properties / edges +AES() + + /** + * Symmetric algorithms + */ + abstract class SymmetricAlgorithm extends Algorithm { + + + abstract TSymmetricCipherFamilyType getSymmetricCipherFamilyType(); + + abstract string getKeySize(Location location); + + abstract TCipherStructure getCipherType(); + + + //mode, padding scheme, keysize, block/stream, auth'd + //nodes = mode, padding scheme + //properties = keysize, block/stream, auth'd + //leave authd to lang specific + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + key = "key_size" and + if exists(this.getKeySize(location)) + then value = this.getKeySize(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + //add more keys to index props + } + + abstract ModeOfOperation getModeOfOperation(); +} } \ No newline at end of file diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 8a613b66d022..389235964b5f 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -14,41 +14,6 @@ predicate cipher_modes(string mode) {mode = ["NONE", "CBC", "CCM", "CFB", "CFBx" predicate cipher_padding(string padding) {padding = ["NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", "SSL3Padding"]} -abstract class BlockCiper extends Crypto::Algorithm { - CipherAlgorithmStringLiteral alg; - CipherAlgorithmMode mode; - CipherAlgorithmPadding padding; - - - CipherAlgorithmStringLiteral getAlg() {result = alg } - CipherAlgorithmMode getMode() {result = mode } - - CipherAlgorithmPadding getPadding() {result =padding} -} - /** - * Symmetric algorithms - */ - abstract class SymmetricAlgorithm extends Crypto::Algorithm { - - - //TODO figure out how to get this from the Cipher interface, is it explicit? - //abstract string getKeySize(Location location); - - // override predicate properties(string key, string value, Location location) { - // super.properties(key, value, location) - // or - // key = "key_size" and - // if exists(this.getKeySize(location)) - // then value = this.getKeySize(location) - // else ( - // value instanceof Crypto::UnknownPropertyValue and location instanceof UnknownLocation - // ) - // // other properties, like field type are possible, but not modeled until considered necessary - // } - - abstract override string getAlgorithmName(); -} - ////cipher specifics ---------------------------------------- class CipherInstance extends Call { @@ -60,24 +25,26 @@ class CipherInstance extends Call { /** * this may be specified either in the ALG/MODE/PADDING or just ALG format */ -class CipherAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLiteral { +class CipherAlgorithmStringLiteral extends StringLiteral { CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/"))} - - override string toString() { result = this.(StringLiteral).toString() } - - string getValue() { result = this.(StringLiteral).getValue() } } -abstract class CipherAlgorithmMode extends Crypto::NodeBase { - string getValue() {result = ""} -} - class CipherAlgorithmModeStringLiteral extends CipherAlgorithmMode instanceof StringLiteral { - CipherAlgorithmModeStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/"))} + class ModeOfOperationStringLiteral extends Crypto::ModeOfOperation instanceof StringLiteral { + ModeOfOperationStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/"))} - override string toString() { result = this.(StringLiteral).toString() } + override string getRawAlgorithmName() { result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*",1) } override string getValue() { result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*",1) } + + + predicate modeToNameMapping(Crypto::TModeOperation type, string name) { + name = "ECB" and type instanceof Crypto::ECB + } + + override Crypto::TModeOperation getModeType(){ + modeToNameMapping(result, this.getRawAlgorithmName()) + } } abstract class CipherAlgorithmPadding extends Crypto::NodeBase { @@ -102,32 +69,51 @@ abstract class CipherAlgorithmMode extends Crypto::NodeBase { module AlgorithmStringToFetchFlow = DataFlow::Global; - predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, CipherAlgorithmModeStringLiteral mode, CipherAlgorithmPaddingStringLiteral padding, Expr arg) { + predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, Expr arg) { exists(CipherInstance sinkCall | origin.getValue().splitAt("/") = name and - origin = mode and - origin = padding and arg = sinkCall.getAlgorithmArg() and AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) ) } + + predicate modeStringToCipherInstanceArgFlow(string name, ModeOfOperationStringLiteral mode, Expr arg) { + exists(CipherInstance sinkCall | + mode.getRawAlgorithmName() = name and + arg = sinkCall.getAlgorithmArg() and + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(mode), DataFlow::exprNode(arg)) + ) + } + /** * A class to represent when AES is used AND it has literal mode and padding provided * this does not capture the use without */ - class AESLiteral extends SymmetricAlgorithm, BlockCiper instanceof Expr { +// class AESLiteral extends Crypto::SymmetricAlgorithm instanceof Expr { +// CipherAlgorithmStringLiteral alg; +// AESLiteral() { algorithmStringToCipherInstanceArgFlow("AES", alg, this) +// } +// override Crypto::ModeOfOperation getModeOfOperation(){ modeStringToCipherInstanceArgFlow(result.getAlgorithmName(), result, this)} - AESLiteral() { algorithmStringToCipherInstanceArgFlow("AES", alg, mode, padding, this) -} +// override Crypto::LocatableElement getOrigin(string name) { +// result = alg and name = alg.toString() +// } - override Crypto::LocatableElement getOrigin(string name) { - result = alg and name = alg.toString() - } +// override string getAlgorithmName(){ result = "AES" } - override string getAlgorithmName(){ result = alg.getValue()} - } +// override string getRawAlgorithmName(){ result = alg.getValue()} + +// override Crypto::TSymmetricCipherFamilyType getSymmetricCipherFamilyType() { result instanceof Crypto::AES} + +// //temp hacks for testing +// override string getKeySize(Location location){ +// result = "" +// } + +// override Crypto::TCipherStructure getCipherType(){ none()} +// } } \ No newline at end of file From 6005437001c27e022d6f9d29c738f5fdb05ad481 Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Mon, 10 Feb 2025 11:26:48 -0500 Subject: [PATCH 13/28] Update JCA model with flow to call as AESuse and format JCA model --- java/ql/lib/experimental/Quantum/JCA.qll | 132 ++++++++++++++--------- 1 file changed, 82 insertions(+), 50 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 389235964b5f..f75cfe7fd083 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -7,17 +7,35 @@ module JCAModel { abstract class EncryptionOperation extends Crypto::EncryptionOperation { } //TODO PBEWith can have suffixes. how to do? enumerate? or match a pattern? -predicate cipher_names(string algo) { algo = ["AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", "DES", "DESede", "DESedeWrap", "ECIES", "PBEWith", "RC2", "RC4", "RC5", "RSA"] } -//TODO solve the fact that x is an int of various values. same as above... enumerate? -predicate cipher_modes(string mode) {mode = ["NONE", "CBC", "CCM", "CFB", "CFBx", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB", "OFBx", "PCBC"]} -//todo same as above, OAEPWith has asuffix type -predicate cipher_padding(string padding) {padding = ["NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", "SSL3Padding"]} + predicate cipher_names(string algo) { + algo = + [ + "AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", + "DES", "DESede", "DESedeWrap", "ECIES", "PBEWith", "RC2", "RC4", "RC5", "RSA" + ] + } + //TODO solve the fact that x is an int of various values. same as above... enumerate? + predicate cipher_modes(string mode) { + mode = + [ + "NONE", "CBC", "CCM", "CFB", "CFBx", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB", "OFBx", + "PCBC" + ] + } -////cipher specifics ---------------------------------------- + //todo same as above, OAEPWith has asuffix type + predicate cipher_padding(string padding) { + padding = + [ + "NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", + "SSL3Padding" + ] + } -class CipherInstance extends Call { - CipherInstance() { this.getCallee().hasQualifiedName("javax.crypto","Cipher", "getInstance") } + ////cipher specifics ---------------------------------------- + class CipherInstance extends Call { + CipherInstance() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "getInstance") } Expr getAlgorithmArg() { result = this.getArgument(0) } } @@ -25,38 +43,44 @@ class CipherInstance extends Call { /** * this may be specified either in the ALG/MODE/PADDING or just ALG format */ -class CipherAlgorithmStringLiteral extends StringLiteral { - CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/"))} + class CipherAlgorithmStringLiteral extends StringLiteral { + CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/")) } } - class ModeOfOperationStringLiteral extends Crypto::ModeOfOperation instanceof StringLiteral { - ModeOfOperationStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/"))} + ModeOfOperationStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/")) } - override string getRawAlgorithmName() { result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*",1) } + override string getRawAlgorithmName() { + result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*", 1) + } - override string getValue() { result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*",1) } + override string getValue() { + result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*", 1) + } + predicate modeToNameMapping(Crypto::TModeOperation type, string name) { + name = "ECB" and type instanceof Crypto::ECB + } - predicate modeToNameMapping(Crypto::TModeOperation type, string name) { - name = "ECB" and type instanceof Crypto::ECB - } - - override Crypto::TModeOperation getModeType(){ + override Crypto::TModeOperation getModeType() { modeToNameMapping(result, this.getRawAlgorithmName()) } } abstract class CipherAlgorithmPadding extends Crypto::NodeBase { - string getValue() {result = ""} + string getValue() { result = "" } } class CipherAlgorithmPaddingStringLiteral extends CipherAlgorithmPadding instanceof StringLiteral { - CipherAlgorithmPaddingStringLiteral() { cipher_padding(this.(StringLiteral).getValue().splitAt("/"))} + CipherAlgorithmPaddingStringLiteral() { + cipher_padding(this.(StringLiteral).getValue().splitAt("/")) + } override string toString() { result = this.(StringLiteral).toString() } - override string getValue() { result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)",1) } + override string getValue() { + result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)", 1) + } } private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { @@ -69,51 +93,59 @@ class CipherAlgorithmStringLiteral extends StringLiteral { module AlgorithmStringToFetchFlow = DataFlow::Global; - predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, Expr arg) { + predicate algorithmStringToCipherInstanceArgFlow( + string name, CipherAlgorithmStringLiteral origin, Expr arg + ) { exists(CipherInstance sinkCall | origin.getValue().splitAt("/") = name and - arg = sinkCall.getAlgorithmArg() and - AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) + arg = sinkCall and + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), + DataFlow::exprNode(sinkCall.getAlgorithmArg())) ) } - - predicate modeStringToCipherInstanceArgFlow(string name, ModeOfOperationStringLiteral mode, Expr arg) { + predicate modeStringToCipherInstanceArgFlow( + string name, ModeOfOperationStringLiteral mode, Expr arg + ) { exists(CipherInstance sinkCall | mode.getRawAlgorithmName() = name and - arg = sinkCall.getAlgorithmArg() and - AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(mode), DataFlow::exprNode(arg)) + arg = sinkCall and + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(mode), + DataFlow::exprNode(sinkCall.getAlgorithmArg())) ) } /** - * A class to represent when AES is used AND it has literal mode and padding provided - * this does not capture the use without + * A class to represent when AES is used + * AND currently it has literal mode and padding provided + * + * this currently does not capture the use without a literal + * though should be extended to */ -// class AESLiteral extends Crypto::SymmetricAlgorithm instanceof Expr { -// CipherAlgorithmStringLiteral alg; -// AESLiteral() { algorithmStringToCipherInstanceArgFlow("AES", alg, this) -// } + class AESAlgo extends Crypto::SymmetricAlgorithm instanceof Expr { + CipherAlgorithmStringLiteral alg; -// override Crypto::ModeOfOperation getModeOfOperation(){ modeStringToCipherInstanceArgFlow(result.getAlgorithmName(), result, this)} + AESAlgo() { algorithmStringToCipherInstanceArgFlow("AES", alg, this) } -// override Crypto::LocatableElement getOrigin(string name) { -// result = alg and name = alg.toString() -// } + override Crypto::ModeOfOperation getModeOfOperation() { + modeStringToCipherInstanceArgFlow(result.getAlgorithmName(), result, this) + } -// override string getAlgorithmName(){ result = "AES" } + override Crypto::LocatableElement getOrigin(string name) { + result = alg and name = alg.toString() + } -// override string getRawAlgorithmName(){ result = alg.getValue()} + override string getAlgorithmName() { result = "AES" } -// override Crypto::TSymmetricCipherFamilyType getSymmetricCipherFamilyType() { result instanceof Crypto::AES} + override string getRawAlgorithmName() { result = alg.getValue() } -// //temp hacks for testing -// override string getKeySize(Location location){ -// result = "" -// } + override Crypto::TSymmetricCipherFamilyType getSymmetricCipherFamilyType() { + result instanceof Crypto::AES + } -// override Crypto::TCipherStructure getCipherType(){ none()} -// } + //temp hacks for testing + override string getKeySize(Location location) { result = "" } - -} \ No newline at end of file + override Crypto::TCipherStructure getCipherType() { none() } + } +} From 59208bdb85adb0b5fb14c7b2d9bf94d393ff11ea Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Mon, 10 Feb 2025 12:22:22 -0500 Subject: [PATCH 14/28] Update JCA model to use shared lib --- java/ql/lib/experimental/Quantum/Base.qll | 327 ------------------ java/ql/lib/experimental/Quantum/Language.qll | 2 +- java/ql/lib/qlpack.yml | 1 + .../codeql/cryptography/Model.qll | 65 ++++ 4 files changed, 67 insertions(+), 328 deletions(-) delete mode 100644 java/ql/lib/experimental/Quantum/Base.qll diff --git a/java/ql/lib/experimental/Quantum/Base.qll b/java/ql/lib/experimental/Quantum/Base.qll deleted file mode 100644 index a14f3b6836ad..000000000000 --- a/java/ql/lib/experimental/Quantum/Base.qll +++ /dev/null @@ -1,327 +0,0 @@ -/** - * A language-independent library for reasoning about cryptography. - */ - - import codeql.util.Location - import codeql.util.Option - - signature module InputSig { - class LocatableElement { - Location getLocation(); - } - - class UnknownLocation instanceof Location; - - - } - - module CryptographyBase Input> { - final class LocatableElement = Input::LocatableElement; - - final class UnknownLocation = Input::UnknownLocation; - - final class UnknownPropertyValue extends string { - UnknownPropertyValue() { this = "" } - } - - abstract class NodeBase instanceof LocatableElement { - /** - * Returns a string representation of this node, usually the name of the operation/algorithm/property. - */ - abstract string toString(); - - /** - * Returns the location of this node in the code. - */ - Location getLocation() { result = super.getLocation() } - - /** - * Gets the origin of this node, e.g., a string literal in source describing it. - */ - LocatableElement getOrigin(string value) { none() } - - /** - * Returns the child of this node with the given edge name. - * - * This predicate is used by derived classes to construct the graph of cryptographic operations. - */ - NodeBase getChild(string edgeName) { none() } - - /** - * Defines properties of this node by name and either a value or location or both. - * - * This predicate is used by derived classes to construct the graph of cryptographic operations. - */ - predicate properties(string key, string value, Location location) { - key = "origin" and location = this.getOrigin(value).getLocation() - } - - /** - * Returns the parent of this node. - */ - final NodeBase getAParent() { result.getChild(_) = this } - } - - class Asset = NodeBase; - - /** - * A cryptographic operation, such as hashing or encryption. - */ - abstract class Operation extends Asset { - /** - * Gets the algorithm associated with this operation. - */ - abstract Algorithm getAlgorithm(); - - /** - * Gets the name of this operation, e.g., "hash" or "encrypt". - */ - abstract string getOperationName(); - - final override string toString() { result = this.getOperationName() } - - override NodeBase getChild(string edgeName) { - result = super.getChild(edgeName) - or - edgeName = "uses" and - if exists(this.getAlgorithm()) then result = this.getAlgorithm() else result = this - } - } - - abstract class Algorithm extends Asset { - /** - * Gets the name of this algorithm, e.g., "AES" or "SHA". - */ - abstract string getAlgorithmName(); - - /** - * Gets the raw name of this algorithm from source (no parsing or formatting) - */ - abstract string getRawAlgorithmName(); - - final override string toString() { result = this.getAlgorithmName() } - } - - /** - * A hashing operation that processes data to generate a hash value. - * This operation takes an input message of arbitrary content and length and produces a fixed-size - * hash value as the output using a specified hashing algorithm. - */ - abstract class HashOperation extends Operation { - abstract override HashAlgorithm getAlgorithm(); - - override string getOperationName() { result = "HASH" } - } - - // Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces - // - // Example: HKDF and PKCS12KDF are both key derivation algorithms. - // However, PKCS12KDF also has a property: the iteration count. - // - // If we have HKDF and PKCS12KDF under TKeyDerivationType, - // someone modelling a library might try to make a generic identification of both of those algorithms. - // - // They will therefore not use the specialized type for PKCS12KDF, - // meaning "from PKCS12KDF algo select algo" will have no results. - // - newtype THashType = - // We're saying by this that all of these have an identical interface / properties / edges - MD5() or - SHA1() or - SHA256() or - SHA512() or - OtherHashType() - - /** - * A hashing algorithm that transforms variable-length input into a fixed-size hash value. - */ - abstract class HashAlgorithm extends Algorithm { - final predicate hashTypeToNameMapping(THashType type, string name) { - type instanceof MD5 and name = "MD5" - or - type instanceof SHA1 and name = "SHA-1" - or - type instanceof SHA256 and name = "SHA-256" - or - type instanceof SHA512 and name = "SHA-512" - or - type instanceof OtherHashType and name = this.getRawAlgorithmName() - } - - abstract THashType getHashType(); - - override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } - - /** - * Gets the raw name of this hash algorithm from source. - */ - override abstract string getRawAlgorithmName(); - } - - /** - * An operation that derives one or more keys from an input value. - */ - abstract class KeyDerivationOperation extends Operation { - override string getOperationName() { result = "KEY_DERIVATION" } - } - - /** - * An algorithm that derives one or more keys from an input value. - */ - abstract class KeyDerivationAlgorithm extends Algorithm { - abstract override string getAlgorithmName(); - } - - /** - * HKDF key derivation function - */ - abstract class HKDF extends KeyDerivationAlgorithm { - final override string getAlgorithmName() { result = "HKDF" } - - abstract HashAlgorithm getHashAlgorithm(); - - override NodeBase getChild(string edgeName) { - result = super.getChild(edgeName) - or - edgeName = "digest" and result = this.getHashAlgorithm() - } - } - - /** - * PKCS #12 key derivation function - */ - abstract class PKCS12KDF extends KeyDerivationAlgorithm { - final override string getAlgorithmName() { result = "PKCS12KDF" } - - abstract HashAlgorithm getHashAlgorithm(); - - override NodeBase getChild(string edgeName) { - result = super.getChild(edgeName) - or - edgeName = "digest" and result = this.getHashAlgorithm() - } - } - - /** - * Elliptic curve algorithm - */ - abstract class EllipticCurve extends Algorithm { - abstract string getVersion(Location location); - - abstract string getKeySize(Location location); - - override predicate properties(string key, string value, Location location) { - super.properties(key, value, location) - or - key = "version" and - if exists(this.getVersion(location)) - then value = this.getVersion(location) - else ( - value instanceof UnknownPropertyValue and location instanceof UnknownLocation - ) - or - key = "key_size" and - if exists(this.getKeySize(location)) - then value = this.getKeySize(location) - else ( - value instanceof UnknownPropertyValue and location instanceof UnknownLocation - ) - } - } - - /** - * An encryption operation that processes plaintext to generate a ciphertext. - * This operation takes an input message (plaintext) of arbitrary content and length and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). - */ - abstract class EncryptionOperation extends Operation { - abstract override Algorithm getAlgorithm(); - - override string getOperationName() { result = "ENCRYPTION" } - } - -// newtype TBlockCipherFamilyType = -// // We're saying by this that all of these have an identical interface / properties / edges -// CBC() or ECB() - - -// abstract class BlockCiper extends Algorithm { - -// abstract string getKeySize(Location location); - -// abstract TBlockCipherFamilyType getBlockCipherFamilyType(); - -// override predicate properties(string key, string value, Location location) { -// super.properties(key, value, location) -// or -// key = "key_size" and -// if exists(this.getKeySize(location)) -// then value = this.getKeySize(location) -// else ( -// value instanceof UnknownPropertyValue and location instanceof UnknownLocation -// ) -// // other properties, like field type are possible, but not modeled until considered necessary -// } - -// override string getAlgorithmName() { result = this.getRawAlgorithmName().toUpperCase()} - -// override abstract string getRawAlgorithmName(); -// } - -newtype TModeOperation = -ECB() or OtherMode() - -abstract class ModeOfOperation extends Algorithm { - string getValue() {result = ""} - - final private predicate modeToNameMapping(TModeOperation type, string name) { - type instanceof ECB and name = "ECB" - or - type instanceof OtherMode and name = this.getRawAlgorithmName() - } - - abstract TModeOperation getModeType(); - - override string getAlgorithmName() { this.modeToNameMapping(this.getModeType(), result) } - -} - -newtype TCipherStructure = -Block() or Stream() - - newtype TSymmetricCipherFamilyType = -// We're saying by this that all of these have an identical interface / properties / edges -AES() - - /** - * Symmetric algorithms - */ - abstract class SymmetricAlgorithm extends Algorithm { - - - abstract TSymmetricCipherFamilyType getSymmetricCipherFamilyType(); - - abstract string getKeySize(Location location); - - abstract TCipherStructure getCipherType(); - - - //mode, padding scheme, keysize, block/stream, auth'd - //nodes = mode, padding scheme - //properties = keysize, block/stream, auth'd - //leave authd to lang specific - override predicate properties(string key, string value, Location location) { - super.properties(key, value, location) - or - key = "key_size" and - if exists(this.getKeySize(location)) - then value = this.getKeySize(location) - else ( - value instanceof UnknownPropertyValue and location instanceof UnknownLocation - ) - //add more keys to index props - } - - abstract ModeOfOperation getModeOfOperation(); -} - } - \ No newline at end of file diff --git a/java/ql/lib/experimental/Quantum/Language.qll b/java/ql/lib/experimental/Quantum/Language.qll index 246f2b86367c..485b3e716e69 100644 --- a/java/ql/lib/experimental/Quantum/Language.qll +++ b/java/ql/lib/experimental/Quantum/Language.qll @@ -1,4 +1,4 @@ -private import Base +private import codeql.cryptography.Model private import java as Lang /** diff --git a/java/ql/lib/qlpack.yml b/java/ql/lib/qlpack.yml index 18b74a919dd2..ae7f13ad7ab3 100644 --- a/java/ql/lib/qlpack.yml +++ b/java/ql/lib/qlpack.yml @@ -6,6 +6,7 @@ extractor: java library: true upgrades: upgrades dependencies: + codeql/cryptography: ${workspace} codeql/dataflow: ${workspace} codeql/mad: ${workspace} codeql/rangeanalysis: ${workspace} diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index eba25db60d24..aa626066684b 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -245,4 +245,69 @@ module CryptographyBase Input> { */ abstract override string getRawAlgorithmName(); } + + /** + * An encryption operation that processes plaintext to generate a ciphertext. + * This operation takes an input message (plaintext) of arbitrary content and length and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). + */ + abstract class EncryptionOperation extends Operation { + abstract override Algorithm getAlgorithm(); + + override string getOperationName() { result = "ENCRYPTION" } + } + + newtype TModeOperation = + ECB() or + OtherMode() + + abstract class ModeOfOperation extends Algorithm { + string getValue() { result = "" } + + final private predicate modeToNameMapping(TModeOperation type, string name) { + type instanceof ECB and name = "ECB" + or + type instanceof OtherMode and name = this.getRawAlgorithmName() + } + + abstract TModeOperation getModeType(); + + override string getAlgorithmName() { this.modeToNameMapping(this.getModeType(), result) } + } + + newtype TCipherStructure = + Block() or + Stream() + + newtype TSymmetricCipherFamilyType = + // We're saying by this that all of these have an identical interface / properties / edges + AES() + + /** + * Symmetric algorithms + */ + abstract class SymmetricAlgorithm extends Algorithm { + abstract TSymmetricCipherFamilyType getSymmetricCipherFamilyType(); + + abstract string getKeySize(Location location); + + abstract TCipherStructure getCipherType(); + + //mode, padding scheme, keysize, block/stream, auth'd + //nodes = mode, padding scheme + //properties = keysize, block/stream, auth'd + //leave authd to lang specific + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + key = "key_size" and + if exists(this.getKeySize(location)) + then value = this.getKeySize(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + //add more keys to index props + } + + abstract ModeOfOperation getModeOfOperation(); + } } From 1a12fb309902fa6111c443051ab56359d6867f48 Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Mon, 10 Feb 2025 13:49:32 -0500 Subject: [PATCH 15/28] Update JCA model, refactor modes --- java/ql/lib/experimental/Quantum/JCA.qll | 47 +++++++++++-------- .../codeql/cryptography/Model.qll | 1 + 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index f75cfe7fd083..4443ce85159c 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -47,16 +47,18 @@ module JCAModel { CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/")) } } - class ModeOfOperationStringLiteral extends Crypto::ModeOfOperation instanceof StringLiteral { + class ModeOfOperationStringLiteral extends StringLiteral { ModeOfOperationStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/")) } - override string getRawAlgorithmName() { - result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*", 1) - } + string getRawAlgorithmName() { result = this.getValue().regexpCapture(".*/(.*)/.*", 1) } + } - override string getValue() { - result = this.(StringLiteral).getValue().regexpCapture(".*/(.*)/.*", 1) - } + class ECBMode extends Crypto::ModeOfOperation { + ModeOfOperationStringLiteral mode; + + ECBMode() { modeStringToCipherInstanceArgFlow("ECB", mode, this) } + + override string getRawAlgorithmName() { result = mode.getRawAlgorithmName() } predicate modeToNameMapping(Crypto::TModeOperation type, string name) { name = "ECB" and type instanceof Crypto::ECB @@ -65,24 +67,26 @@ module JCAModel { override Crypto::TModeOperation getModeType() { modeToNameMapping(result, this.getRawAlgorithmName()) } + + override Crypto::LocatableElement getOrigin(string name) { + result = mode and name = mode.toString() + } } abstract class CipherAlgorithmPadding extends Crypto::NodeBase { string getValue() { result = "" } } - class CipherAlgorithmPaddingStringLiteral extends CipherAlgorithmPadding instanceof StringLiteral { - CipherAlgorithmPaddingStringLiteral() { - cipher_padding(this.(StringLiteral).getValue().splitAt("/")) - } - - override string toString() { result = this.(StringLiteral).toString() } - - override string getValue() { - result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)", 1) - } - } - + //todo refactor + // class CipherAlgorithmPaddingStringLiteral extends CipherAlgorithmPadding instanceof StringLiteral { + // CipherAlgorithmPaddingStringLiteral() { + // cipher_padding(this.(StringLiteral).getValue().splitAt("/")) + // } + // override string toString() { result = this.(StringLiteral).toString() } + // override string getValue() { + // result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)", 1) + // } + // } private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherAlgorithmStringLiteral } @@ -108,6 +112,7 @@ module JCAModel { string name, ModeOfOperationStringLiteral mode, Expr arg ) { exists(CipherInstance sinkCall | + //consider if this should be a more specific predicate mode.getRawAlgorithmName() = name and arg = sinkCall and AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(mode), @@ -127,8 +132,10 @@ module JCAModel { AESAlgo() { algorithmStringToCipherInstanceArgFlow("AES", alg, this) } + //todo this is really not correct yet override Crypto::ModeOfOperation getModeOfOperation() { - modeStringToCipherInstanceArgFlow(result.getAlgorithmName(), result, this) + none() + //exists(Crypto::ModeOfOperation mode | mode = this and result = this) } override Crypto::LocatableElement getOrigin(string name) { diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index aa626066684b..2b2919b6d3f8 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -258,6 +258,7 @@ module CryptographyBase Input> { newtype TModeOperation = ECB() or + CBC() or OtherMode() abstract class ModeOfOperation extends Algorithm { From 4d447559457edacc18dad249417e2855e2b7269d Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Tue, 11 Feb 2025 15:37:15 +0100 Subject: [PATCH 16/28] Refactor Model and CBOM print queries --- cpp/ql/src/experimental/Quantum/CBOMGraph.ql | 48 --------- .../experimental/Quantum/PrintCBOMGraph.ql | 21 ++++ java/ql/lib/experimental/Quantum/JCA.qll | 27 ++--- .../experimental/Quantum/PrintCBOMGraph.ql | 21 ++++ .../codeql/cryptography/Model.qll | 101 +++++++++++++----- 5 files changed, 134 insertions(+), 84 deletions(-) delete mode 100644 cpp/ql/src/experimental/Quantum/CBOMGraph.ql create mode 100644 cpp/ql/src/experimental/Quantum/PrintCBOMGraph.ql create mode 100644 java/ql/src/experimental/Quantum/PrintCBOMGraph.ql diff --git a/cpp/ql/src/experimental/Quantum/CBOMGraph.ql b/cpp/ql/src/experimental/Quantum/CBOMGraph.ql deleted file mode 100644 index edcc40aca6a4..000000000000 --- a/cpp/ql/src/experimental/Quantum/CBOMGraph.ql +++ /dev/null @@ -1,48 +0,0 @@ -/** - * @name "Print CBOM Graph" - * @description "Outputs a graph representation of the cryptographic bill of materials." - * @kind graph - * @id cbomgraph - */ - -import experimental.Quantum.Language - -string getPropertyString(Crypto::NodeBase node, string key) { - result = - strictconcat(any(string value, Location location, string parsed | - node.properties(key, value, location) and - parsed = "(" + value + "," + location.toString() + ")" - | - parsed - ), "," - ) -} - -string getLabel(Crypto::NodeBase node) { result = node.toString() } - -query predicate nodes(Crypto::NodeBase node, string key, string value) { - key = "semmle.label" and - value = getLabel(node) - or - // CodeQL's DGML output does not include a location - key = "Location" and - value = node.getLocation().toString() - or - // Known unknown edges should be reported as properties rather than edges - node = node.getChild(key) and - value = "" - or - // Report properties - value = getPropertyString(node, key) -} - -query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { - key = "semmle.label" and - target = source.getChild(value) and - // Known unknowns are reported as properties rather than edges - not source = target -} - -query predicate graphProperties(string key, string value) { - key = "semmle.graphKind" and value = "graph" -} diff --git a/cpp/ql/src/experimental/Quantum/PrintCBOMGraph.ql b/cpp/ql/src/experimental/Quantum/PrintCBOMGraph.ql new file mode 100644 index 000000000000..d9658105aebf --- /dev/null +++ b/cpp/ql/src/experimental/Quantum/PrintCBOMGraph.ql @@ -0,0 +1,21 @@ +/** + * @name Print CBOM Graph + * @description Outputs a graph representation of the cryptographic bill of materials. + * This query only supports DGML output, as CodeQL DOT output omits properties. + * @kind graph + * @id cpp/print-cbom-graph + */ + +import experimental.Quantum.Language + +query predicate nodes(Crypto::NodeBase node, string key, string value) { + Crypto::nodes_graph_impl(node, key, value) +} + +query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { + Crypto::edges_graph_impl(source, target, key, value) +} + +query predicate graphProperties(string key, string value) { + key = "semmle.graphKind" and value = "graph" +} diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 4443ce85159c..44a753bb7db2 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -7,12 +7,14 @@ module JCAModel { abstract class EncryptionOperation extends Crypto::EncryptionOperation { } //TODO PBEWith can have suffixes. how to do? enumerate? or match a pattern? + bindingset[algo] predicate cipher_names(string algo) { - algo = - [ - "AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", - "DES", "DESede", "DESedeWrap", "ECIES", "PBEWith", "RC2", "RC4", "RC5", "RSA" - ] + // "Standard names are not case-sensitive." + algo.toUpperCase() + .matches([ + "AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", + "DES", "DESede", "DESedeWrap", "ECIES", "PBEWith%", "RC2", "RC4", "RC5", "RSA" + ].toUpperCase()) } //TODO solve the fact that x is an int of various values. same as above... enumerate? @@ -33,9 +35,10 @@ module JCAModel { ] } - ////cipher specifics ---------------------------------------- - class CipherInstance extends Call { - CipherInstance() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "getInstance") } + class CipherGetInstanceCall extends Call { + CipherGetInstanceCall() { + this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "getInstance") + } Expr getAlgorithmArg() { result = this.getArgument(0) } } @@ -65,7 +68,7 @@ module JCAModel { } override Crypto::TModeOperation getModeType() { - modeToNameMapping(result, this.getRawAlgorithmName()) + this.modeToNameMapping(result, this.getRawAlgorithmName()) } override Crypto::LocatableElement getOrigin(string name) { @@ -91,7 +94,7 @@ module JCAModel { predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherAlgorithmStringLiteral } predicate isSink(DataFlow::Node sink) { - exists(CipherInstance call | sink.asExpr() = call.getAlgorithmArg()) + exists(CipherGetInstanceCall call | sink.asExpr() = call.getAlgorithmArg()) } } @@ -100,7 +103,7 @@ module JCAModel { predicate algorithmStringToCipherInstanceArgFlow( string name, CipherAlgorithmStringLiteral origin, Expr arg ) { - exists(CipherInstance sinkCall | + exists(CipherGetInstanceCall sinkCall | origin.getValue().splitAt("/") = name and arg = sinkCall and AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), @@ -111,7 +114,7 @@ module JCAModel { predicate modeStringToCipherInstanceArgFlow( string name, ModeOfOperationStringLiteral mode, Expr arg ) { - exists(CipherInstance sinkCall | + exists(CipherGetInstanceCall sinkCall | //consider if this should be a more specific predicate mode.getRawAlgorithmName() = name and arg = sinkCall and diff --git a/java/ql/src/experimental/Quantum/PrintCBOMGraph.ql b/java/ql/src/experimental/Quantum/PrintCBOMGraph.ql new file mode 100644 index 000000000000..063cda564b60 --- /dev/null +++ b/java/ql/src/experimental/Quantum/PrintCBOMGraph.ql @@ -0,0 +1,21 @@ +/** + * @name Print CBOM Graph + * @description Outputs a graph representation of the cryptographic bill of materials. + * This query only supports DGML output, as CodeQL DOT output omits properties. + * @kind graph + * @id java/print-cbom-graph + */ + +import experimental.Quantum.Language + +query predicate nodes(Crypto::NodeBase node, string key, string value) { + Crypto::nodes_graph_impl(node, key, value) +} + +query predicate edges(Crypto::NodeBase source, Crypto::NodeBase target, string key, string value) { + Crypto::edges_graph_impl(source, target, key, value) +} + +query predicate graphProperties(string key, string value) { + key = "semmle.graphKind" and value = "graph" +} diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 2b2919b6d3f8..ad117674dffe 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -22,6 +22,45 @@ module CryptographyBase Input> { UnknownPropertyValue() { this = "" } } + private string getPropertyAsGraphString(NodeBase node, string key) { + result = + strictconcat(any(string value, Location location, string parsed | + node.properties(key, value, location) and + parsed = "(" + value + "," + location.toString() + ")" + | + parsed + ), "," + ) + } + + predicate nodes_graph_impl(NodeBase node, string key, string value) { + key = "semmle.label" and + value = node.toString() + or + // CodeQL's DGML output does not include a location + key = "Location" and + value = node.getLocation().toString() + or + // Known unknown edges should be reported as properties rather than edges + node = node.getChild(key) and + value = "" + or + // Report properties + value = getPropertyAsGraphString(node, key) + } + + predicate edges_graph_impl(NodeBase source, NodeBase target, string key, string value) { + key = "semmle.label" and + target = source.getChild(value) and + // Known unknowns are reported as properties rather than edges + not source = target + } + + /** + * The base class for all cryptographic assets, such as operations and algorithms. + * + * Each `NodeBase` is a node in a graph of cryptographic operations, where the edges are the relationships between the nodes. + */ abstract class NodeBase instanceof LocatableElement { /** * Returns a string representation of this node, usually the name of the operation/algorithm/property. @@ -104,6 +143,7 @@ module CryptographyBase Input> { /** * A hashing operation that processes data to generate a hash value. + * * This operation takes an input message of arbitrary content and length and produces a fixed-size * hash value as the output using a specified hashing algorithm. */ @@ -113,19 +153,7 @@ module CryptographyBase Input> { override string getOperationName() { result = "HASH" } } - // Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces - // - // Example: HKDF and PKCS12KDF are both key derivation algorithms. - // However, PKCS12KDF also has a property: the iteration count. - // - // If we have HKDF and PKCS12KDF under TKeyDerivationType, - // someone modelling a library might try to make a generic identification of both of those algorithms. - // - // They will therefore not use the specialized type for PKCS12KDF, - // meaning "from PKCS12KDF algo select algo" will have no results. - // newtype THashType = - // We're saying by this that all of these have an identical interface / properties / edges MD5() or SHA1() or SHA256() or @@ -197,8 +225,28 @@ module CryptographyBase Input> { } } - newtype TEllipticCurveFamilyType = - // We're saying by this that all of these have an identical interface / properties / edges + /* + * TODO: + * + * Rule: No newtype representing a type of algorithm should be modelled with multiple interfaces + * + * Example 1: HKDF and PKCS12KDF are both key derivation algorithms. + * However, PKCS12KDF also has a property: the iteration count. + * + * If we have HKDF and PKCS12KDF under TKeyDerivationType, + * someone modelling a library might try to make a generic identification of both of those algorithms. + * + * They will therefore not use the specialized type for PKCS12KDF, + * meaning "from PKCS12KDF algo select algo" will have no results. + * + * Example 2: Each type below represents a common family of elliptic curves, with a shared interface, i.e., + * predicates for library modellers to implement as well as the properties and edges reported. + */ + + /** + * Elliptic curve algorithms + */ + newtype TEllipticCurveFamily = NIST() or SEC() or NUMS() or @@ -211,13 +259,10 @@ module CryptographyBase Input> { ES() or OtherEllipticCurveFamilyType() - /** - * Elliptic curve algorithm - */ abstract class EllipticCurve extends Algorithm { abstract string getKeySize(Location location); - abstract TEllipticCurveFamilyType getCurveFamilyType(); + abstract TEllipticCurveFamily getCurveFamilyType(); override predicate properties(string key, string value, Location location) { super.properties(key, value, location) @@ -236,8 +281,10 @@ module CryptographyBase Input> { /** * Mandating that for Elliptic Curves specifically, users are responsible * for providing as the 'raw' name, the official name of the algorithm. + * * Casing doesn't matter, we will enforce further naming restrictions on * `getAlgorithmName` by default. + * * Rationale: elliptic curve names can have a lot of variation in their components * (e.g., "secp256r1" vs "P-256"), trying to produce generalized set of properties * is possible to capture all cases, but such modeling is likely not necessary. @@ -256,17 +303,20 @@ module CryptographyBase Input> { override string getOperationName() { result = "ENCRYPTION" } } + /** + * Block cipher modes of operation algorithms + */ newtype TModeOperation = ECB() or CBC() or OtherMode() abstract class ModeOfOperation extends Algorithm { - string getValue() { result = "" } - final private predicate modeToNameMapping(TModeOperation type, string name) { type instanceof ECB and name = "ECB" or + type instanceof CBC and name = "CBC" + or type instanceof OtherMode and name = this.getRawAlgorithmName() } @@ -275,17 +325,20 @@ module CryptographyBase Input> { override string getAlgorithmName() { this.modeToNameMapping(this.getModeType(), result) } } + /** + * A helper type for distinguishing between block and stream ciphers. + */ newtype TCipherStructure = Block() or Stream() - newtype TSymmetricCipherFamilyType = - // We're saying by this that all of these have an identical interface / properties / edges - AES() - /** * Symmetric algorithms */ + newtype TSymmetricCipherFamilyType = + AES() or + OtherSymmetricCipherFamilyType() + abstract class SymmetricAlgorithm extends Algorithm { abstract TSymmetricCipherFamilyType getSymmetricCipherFamilyType(); From 874e3b5e063bdd403264eea80e367d6a2f4eccdc Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Wed, 12 Feb 2025 17:58:15 +0100 Subject: [PATCH 17/28] Modify model to use newtypes, expand modeling --- cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 204 ++++++-- java/ql/lib/experimental/Quantum/JCA.qll | 143 +++--- java/ql/src/experimental/Quantum/Test.ql | 7 +- .../codeql/cryptography/Model.qll | 467 ++++++++++++++++-- 4 files changed, 665 insertions(+), 156 deletions(-) diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll index bf38e5c0ab5d..cb19092f3fd7 100644 --- a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -4,78 +4,172 @@ import semmle.code.cpp.dataflow.new.DataFlow module OpenSSLModel { import Language - abstract class KeyDerivationOperation extends Crypto::KeyDerivationOperation { } + class FunctionCallOrMacroAccess extends Element { + FunctionCallOrMacroAccess() { this instanceof FunctionCall or this instanceof MacroAccess } + + string getTargetName() { + result = this.(FunctionCall).getTarget().getName() + or + result = this.(MacroAccess).getMacroName() + } + } + + /** + * Hash function references in OpenSSL. + */ + predicate hash_ref_type_mapping_known(string name, Crypto::THashType algo) { + // `ma` name has an LN_ or SN_ prefix, which we want to ignore + // capture any name after the _ prefix using regex matching + name = ["sha1", "sha160"] and algo instanceof Crypto::SHA1 + or + name = ["sha224", "sha256", "sha384", "sha512"] and algo instanceof Crypto::SHA2 + or + name = ["sha3-224", "sha3-256", "sha3-384", "sha3-512"] and algo instanceof Crypto::SHA3 + or + name = "md2" and algo instanceof Crypto::MD2 + or + name = "md4" and algo instanceof Crypto::MD4 + or + name = "md5" and algo instanceof Crypto::MD5 + or + name = "ripemd160" and algo instanceof Crypto::RIPEMD160 + or + name = "whirlpool" and algo instanceof Crypto::WHIRLPOOL + } + + predicate hash_ref_type_mapping(FunctionCallOrMacroAccess ref, string name, Crypto::THashType algo) { + name = ref.getTargetName().regexpCapture("(?:SN_|LN_|EVP_)([a-z0-9]+)", 1) and + hash_ref_type_mapping_known(name, algo) + } + + class HashAlgorithmRef extends Crypto::HashAlgorithm { + FunctionCallOrMacroAccess instance; + + HashAlgorithmRef() { + this = Crypto::THashAlgorithm(instance) and + hash_ref_type_mapping(instance, _, _) + } + + override string getSHA2OrSHA3DigestSize(Location location) { + ( + this.getHashType() instanceof Crypto::SHA2 or + this.getHashType() instanceof Crypto::SHA3 + ) and + exists(string name | + hash_ref_type_mapping(instance, name, this.getHashType()) and + result = name.regexpFind("\\d{3}", 0, _) and + location = instance.getLocation() + ) + } - class SHA1Algo extends Crypto::HashAlgorithm instanceof MacroAccess { - SHA1Algo() { this.getMacro().getName() = "SN_sha1" } + override string getRawAlgorithmName() { result = instance.getTargetName() } - override string getRawAlgorithmName() { result = "SN_sha1" } + override Crypto::THashType getHashType() { hash_ref_type_mapping(instance, _, result) } - override Crypto::THashType getHashType() { result instanceof Crypto::SHA1 } + Element getInstance() { result = instance } + + override Location getLocation() { result = instance.getLocation() } } + /** + * Data-flow configuration for key derivation algorithm flow to EVP_KDF_derive. + */ module AlgorithmToEVPKeyDeriveConfig implements DataFlow::ConfigSig { - predicate isSource(DataFlow::Node source) { source.asExpr() instanceof KeyDerivationAlgorithm } + predicate isSource(DataFlow::Node source) { + source.asExpr() = any(KeyDerivationAlgorithm a).getInstance() + } predicate isSink(DataFlow::Node sink) { - exists(EVP_KDF_derive kdo | sink.asExpr() = kdo.getAlgorithmArg()) + exists(EVP_KDF_derive kdo | + sink.asExpr() = kdo.getAlgorithmArg() + or + sink.asExpr() = kdo.getContextArg() // via `EVP_KDF_CTX_set_params` + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + none() // TODO } } module AlgorithmToEVPKeyDeriveFlow = DataFlow::Global; - predicate algorithm_to_EVP_KDF_derive(Crypto::Algorithm algo, EVP_KDF_derive derive) { - algo.(Expr).getEnclosingFunction() = derive.(Expr).getEnclosingFunction() + predicate algorithm_to_EVP_KDF_derive(KeyDerivationAlgorithm algo, EVP_KDF_derive derive) { + none() } - class EVP_KDF_derive extends KeyDerivationOperation instanceof FunctionCall { - EVP_KDF_derive() { this.getTarget().getName() = "EVP_KDF_derive" } + /** + * Key derivation operation (e.g., `EVP_KDF_derive`) + */ + abstract class KeyDerivationOperation extends Crypto::KeyDerivationOperation { } + + class EVP_KDF_derive extends KeyDerivationOperation { + FunctionCall instance; + + EVP_KDF_derive() { + this = Crypto::TKeyDerivationOperation(instance) and + instance.getTarget().getName() = "EVP_KDF_derive" + } override Crypto::Algorithm getAlgorithm() { algorithm_to_EVP_KDF_derive(result, this) } - Expr getAlgorithmArg() { result = this.(FunctionCall).getArgument(3) } + Expr getAlgorithmArg() { result = instance.getArgument(3) } + + Expr getContextArg() { result = instance.getArgument(0) } } - abstract class KeyDerivationAlgorithm extends Crypto::KeyDerivationAlgorithm { } + /** + * Key derivation algorithm nodes + */ + abstract class KeyDerivationAlgorithm extends Crypto::KeyDerivationAlgorithm { + abstract Expr getInstance(); + } + /** + * `EVP_KDF_fetch` returns a key derivation algorithm. + */ class EVP_KDF_fetch_Call extends FunctionCall { EVP_KDF_fetch_Call() { this.getTarget().getName() = "EVP_KDF_fetch" } Expr getAlgorithmArg() { result = this.getArgument(1) } } - predicate kdf_names(string algo) { algo = ["HKDF", "PKCS12KDF"] } - - class KDFAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLiteral { - KDFAlgorithmStringLiteral() { kdf_names(this.getValue().toUpperCase()) } + class EVP_KDF_fetch_AlgorithmArg extends Expr { + EVP_KDF_fetch_AlgorithmArg() { exists(EVP_KDF_fetch_Call call | this = call.getAlgorithmArg()) } + } - override string toString() { result = this.(StringLiteral).toString() } + predicate kdf_names(string algo) { algo = ["HKDF", "PKCS12KDF", "PBKDF2"] } - string getValue() { result = this.(StringLiteral).getValue() } + class KDFAlgorithmStringLiteral extends StringLiteral { + KDFAlgorithmStringLiteral() { kdf_names(this.getValue().toUpperCase()) } } private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { predicate isSource(DataFlow::Node src) { src.asExpr() instanceof KDFAlgorithmStringLiteral } - predicate isSink(DataFlow::Node sink) { - exists(EVP_KDF_fetch_Call call | sink.asExpr() = call.getAlgorithmArg()) - } + predicate isSink(DataFlow::Node sink) { sink.asExpr() instanceof EVP_KDF_fetch_AlgorithmArg } } module AlgorithmStringToFetchFlow = DataFlow::Global; - predicate algorithmStringToKDFFetchArgFlow(string name, KDFAlgorithmStringLiteral origin, Expr arg) { - exists(EVP_KDF_fetch_Call sinkCall | - origin.getValue().toUpperCase() = name and - arg = sinkCall.getAlgorithmArg() and - AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) - ) + predicate algorithmStringToKDFFetchArgFlow( + string name, KDFAlgorithmStringLiteral origin, EVP_KDF_fetch_AlgorithmArg arg + ) { + origin.getValue().toUpperCase() = name and + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg)) } - class HKDF extends KeyDerivationAlgorithm, Crypto::HKDF instanceof Expr { + /** + * HKDF key derivation algorithm. + */ + class HKDF extends KeyDerivationAlgorithm, Crypto::HKDF { KDFAlgorithmStringLiteral origin; + EVP_KDF_fetch_AlgorithmArg instance; - HKDF() { algorithmStringToKDFFetchArgFlow("HKDF", origin, this) } + HKDF() { + this = Crypto::TKeyDerivationAlgorithm(instance) and + algorithmStringToKDFFetchArgFlow("HKDF", origin, instance) + } override string getRawAlgorithmName() { result = origin.getValue() } @@ -84,19 +178,61 @@ module OpenSSLModel { override Crypto::LocatableElement getOrigin(string name) { result = origin and name = origin.toString() } + + override Expr getInstance() { result = origin } } - class PKCS12KDF extends KeyDerivationAlgorithm, Crypto::PKCS12KDF instanceof Expr { + /** + * PBKDF2 key derivation algorithm. + */ + class PBKDF2 extends KeyDerivationAlgorithm, Crypto::PBKDF2 { KDFAlgorithmStringLiteral origin; + EVP_KDF_fetch_AlgorithmArg instance; - PKCS12KDF() { algorithmStringToKDFFetchArgFlow("PKCS12KDF", origin, this) } + PBKDF2() { + this = Crypto::TKeyDerivationAlgorithm(instance) and + algorithmStringToKDFFetchArgFlow("PBKDF2", origin, instance) + } override string getRawAlgorithmName() { result = origin.getValue() } - override Crypto::HashAlgorithm getHashAlgorithm() { none() } + override string getIterationCount(Location location) { none() } // TODO + + override string getKeyLength(Location location) { none() } // TODO + + override Crypto::HashAlgorithm getHashAlgorithm() { none() } // TODO + + override Crypto::LocatableElement getOrigin(string name) { + result = origin and name = origin.toString() + } - override Crypto::NodeBase getOrigin(string name) { + override Expr getInstance() { result = instance } + } + + /** + * PKCS12KDF key derivation algorithm. + */ + class PKCS12KDF extends KeyDerivationAlgorithm, Crypto::PKCS12KDF { + KDFAlgorithmStringLiteral origin; + EVP_KDF_fetch_AlgorithmArg instance; + + PKCS12KDF() { + this = Crypto::TKeyDerivationAlgorithm(instance) and + algorithmStringToKDFFetchArgFlow("PKCS12KDF", origin, instance) + } + + override string getRawAlgorithmName() { result = origin.getValue() } + + override string getIterationCount(Location location) { none() } // TODO + + override string getIDByte(Location location) { none() } // TODO + + override Crypto::HashAlgorithm getHashAlgorithm() { none() } // TODO + + override Crypto::LocatableElement getOrigin(string name) { result = origin and name = origin.toString() } + + override Expr getInstance() { result = instance } } } diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 44a753bb7db2..807dec96ba40 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -35,6 +35,19 @@ module JCAModel { ] } + /** + * this may be specified either in the ALG/MODE/PADDING or just ALG format + */ + class CipherStringLiteral extends StringLiteral { + CipherStringLiteral() { cipher_names(this.getValue().splitAt("/")) } + + string getAlgorithmName() { result = this.getValue().splitAt("/", 0) } + + string getMode() { result = this.getValue().splitAt("/", 1) } + + string getPadding() { result = this.getValue().splitAt("/", 2) } + } + class CipherGetInstanceCall extends Call { CipherGetInstanceCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "getInstance") @@ -43,41 +56,48 @@ module JCAModel { Expr getAlgorithmArg() { result = this.getArgument(0) } } - /** - * this may be specified either in the ALG/MODE/PADDING or just ALG format - */ - class CipherAlgorithmStringLiteral extends StringLiteral { - CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/")) } + private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherStringLiteral } + + predicate isSink(DataFlow::Node sink) { + exists(CipherGetInstanceCall call | sink.asExpr() = call.getAlgorithmArg()) + } } - class ModeOfOperationStringLiteral extends StringLiteral { - ModeOfOperationStringLiteral() { cipher_modes(this.(StringLiteral).getValue().splitAt("/")) } + module AlgorithmStringToFetchFlow = DataFlow::Global; - string getRawAlgorithmName() { result = this.getValue().regexpCapture(".*/(.*)/.*", 1) } + class CipherGetInstanceAlgorithmArg extends Expr { + CipherGetInstanceAlgorithmArg() { + exists(CipherGetInstanceCall call | this = call.getArgument(0)) + } + + StringLiteral getOrigin() { + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(result), DataFlow::exprNode(this)) + } } - class ECBMode extends Crypto::ModeOfOperation { - ModeOfOperationStringLiteral mode; + class ModeStringLiteral extends Crypto::ModeOfOperation { + CipherStringLiteral instance; - ECBMode() { modeStringToCipherInstanceArgFlow("ECB", mode, this) } + ModeStringLiteral() { + this = Crypto::TModeOfOperationAlgorithm(instance) and + exists(instance.getMode()) and + instance = any(CipherGetInstanceAlgorithmArg call).getOrigin() + } - override string getRawAlgorithmName() { result = mode.getRawAlgorithmName() } + override Location getLocation() { result = instance.getLocation() } - predicate modeToNameMapping(Crypto::TModeOperation type, string name) { - name = "ECB" and type instanceof Crypto::ECB - } + override string getRawAlgorithmName() { result = instance.getMode() } - override Crypto::TModeOperation getModeType() { - this.modeToNameMapping(result, this.getRawAlgorithmName()) + predicate modeToNameMapping(Crypto::TModeOperationType type, string name) { + super.modeToNameMapping(type, name) } - override Crypto::LocatableElement getOrigin(string name) { - result = mode and name = mode.toString() + override Crypto::TModeOperationType getModeType() { + this.modeToNameMapping(result, instance.getMode().toUpperCase()) } - } - abstract class CipherAlgorithmPadding extends Crypto::NodeBase { - string getValue() { result = "" } + CipherStringLiteral getInstance() { result = instance } } //todo refactor @@ -90,39 +110,6 @@ module JCAModel { // result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)", 1) // } // } - private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { - predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherAlgorithmStringLiteral } - - predicate isSink(DataFlow::Node sink) { - exists(CipherGetInstanceCall call | sink.asExpr() = call.getAlgorithmArg()) - } - } - - module AlgorithmStringToFetchFlow = DataFlow::Global; - - predicate algorithmStringToCipherInstanceArgFlow( - string name, CipherAlgorithmStringLiteral origin, Expr arg - ) { - exists(CipherGetInstanceCall sinkCall | - origin.getValue().splitAt("/") = name and - arg = sinkCall and - AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), - DataFlow::exprNode(sinkCall.getAlgorithmArg())) - ) - } - - predicate modeStringToCipherInstanceArgFlow( - string name, ModeOfOperationStringLiteral mode, Expr arg - ) { - exists(CipherGetInstanceCall sinkCall | - //consider if this should be a more specific predicate - mode.getRawAlgorithmName() = name and - arg = sinkCall and - AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(mode), - DataFlow::exprNode(sinkCall.getAlgorithmArg())) - ) - } - /** * A class to represent when AES is used * AND currently it has literal mode and padding provided @@ -130,32 +117,48 @@ module JCAModel { * this currently does not capture the use without a literal * though should be extended to */ - class AESAlgo extends Crypto::SymmetricAlgorithm instanceof Expr { - CipherAlgorithmStringLiteral alg; + class CipherAlgorithm extends Crypto::SymmetricAlgorithm { + CipherStringLiteral origin; + CipherGetInstanceAlgorithmArg instance; + + CipherAlgorithm() { + this = Crypto::TSymmetricAlgorithm(instance) and + instance.getOrigin() = origin + } - AESAlgo() { algorithmStringToCipherInstanceArgFlow("AES", alg, this) } + override Location getLocation() { result = instance.getLocation() } - //todo this is really not correct yet override Crypto::ModeOfOperation getModeOfOperation() { - none() - //exists(Crypto::ModeOfOperation mode | mode = this and result = this) + result.(ModeStringLiteral).getInstance() = origin } override Crypto::LocatableElement getOrigin(string name) { - result = alg and name = alg.toString() + result = origin and name = origin.toString() } - override string getAlgorithmName() { result = "AES" } - - override string getRawAlgorithmName() { result = alg.getValue() } + override string getRawAlgorithmName() { result = origin.getValue() } - override Crypto::TSymmetricCipherFamilyType getSymmetricCipherFamilyType() { - result instanceof Crypto::AES + override Crypto::TSymmetricCipherType getCipherFamily() { + this.cipherNameMapping(result, origin.getAlgorithmName()) } - //temp hacks for testing - override string getKeySize(Location location) { result = "" } + override string getKeySize(Location location) { none() } - override Crypto::TCipherStructure getCipherType() { none() } + bindingset[name] + private predicate cipherNameMappingKnown(Crypto::TSymmetricCipherType type, string name) { + name = "AES" and + type instanceof Crypto::AES + or + name = "RC4" and + type instanceof Crypto::RC4 + } + + bindingset[name] + predicate cipherNameMapping(Crypto::TSymmetricCipherType type, string name) { + this.cipherNameMappingKnown(type, name) + or + not this.cipherNameMappingKnown(_, name) and + type instanceof Crypto::OtherSymmetricCipherType + } } } diff --git a/java/ql/src/experimental/Quantum/Test.ql b/java/ql/src/experimental/Quantum/Test.ql index f35336a846f2..f3ae23a2ccac 100644 --- a/java/ql/src/experimental/Quantum/Test.ql +++ b/java/ql/src/experimental/Quantum/Test.ql @@ -2,7 +2,8 @@ * @name "PQC Test" */ - import experimental.Quantum.Language +import experimental.Quantum.Language -from JCAModel::AESLiteral l -select l, l.getAlg(), l.getMode().getValue(), l.getPadding().getValue() \ No newline at end of file +from Crypto::SymmetricAlgorithm a, Crypto::ModeOfOperation mode +where a.getModeOfOperation() = mode +select a, a.getAlgorithmName(), a.getRawAlgorithmName(), mode, mode.getAlgorithmName() diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index ad117674dffe..dd570a89ef6e 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -56,12 +56,22 @@ module CryptographyBase Input> { not source = target } + newtype TNode = + THashOperation(LocatableElement e) or + THashAlgorithm(LocatableElement e) or + TKeyDerivationOperation(LocatableElement e) or + TKeyDerivationAlgorithm(LocatableElement e) or + TEncryptionOperation(LocatableElement e) or + TSymmetricAlgorithm(LocatableElement e) or + TEllipticCurveAlgorithm(LocatableElement e) or + TModeOfOperationAlgorithm(LocatableElement e) + /** * The base class for all cryptographic assets, such as operations and algorithms. * * Each `NodeBase` is a node in a graph of cryptographic operations, where the edges are the relationships between the nodes. */ - abstract class NodeBase instanceof LocatableElement { + abstract class NodeBase extends TNode { /** * Returns a string representation of this node, usually the name of the operation/algorithm/property. */ @@ -70,7 +80,7 @@ module CryptographyBase Input> { /** * Returns the location of this node in the code. */ - Location getLocation() { result = super.getLocation() } + abstract Location getLocation(); /** * Gets the origin of this node, e.g., a string literal in source describing it. @@ -128,6 +138,8 @@ module CryptographyBase Input> { } abstract class Algorithm extends Asset { + final override string toString() { result = this.getAlgorithmType() } + /** * Gets the name of this algorithm, e.g., "AES" or "SHA". */ @@ -138,7 +150,20 @@ module CryptographyBase Input> { */ abstract string getRawAlgorithmName(); - final override string toString() { result = this.getAlgorithmName() } + /** + * Gets the type of this algorithm, e.g., "hash" or "key derivation". + */ + abstract string getAlgorithmType(); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + // [ONLY_KNOWN] + key = "name" and value = this.getAlgorithmName() and location = this.getLocation() + or + // [ONLY_KNOWN] + key = "raw_name" and value = this.getRawAlgorithmName() and location = this.getLocation() + } } /** @@ -147,81 +172,318 @@ module CryptographyBase Input> { * This operation takes an input message of arbitrary content and length and produces a fixed-size * hash value as the output using a specified hashing algorithm. */ - abstract class HashOperation extends Operation { + abstract class HashOperation extends Operation, THashOperation { abstract override HashAlgorithm getAlgorithm(); - override string getOperationName() { result = "HASH" } + override string getOperationName() { result = "HashOperation" } } newtype THashType = + MD2() or + MD4() or MD5() or SHA1() or - SHA256() or - SHA512() or + SHA2() or + SHA3() or + RIPEMD160() or + WHIRLPOOL() or OtherHashType() /** * A hashing algorithm that transforms variable-length input into a fixed-size hash value. */ - abstract class HashAlgorithm extends Algorithm { + abstract class HashAlgorithm extends Algorithm, THashAlgorithm { + override string getAlgorithmType() { result = "HashAlgorithm" } + final predicate hashTypeToNameMapping(THashType type, string name) { + type instanceof MD2 and name = "MD2" + or + type instanceof MD4 and name = "MD4" + or type instanceof MD5 and name = "MD5" or - type instanceof SHA1 and name = "SHA-1" + type instanceof SHA1 and name = "SHA1" + or + type instanceof SHA2 and name = "SHA2" or - type instanceof SHA256 and name = "SHA-256" + type instanceof SHA3 and name = "SHA3" or - type instanceof SHA512 and name = "SHA-512" + type instanceof RIPEMD160 and name = "RIPEMD160" + or + type instanceof WHIRLPOOL and name = "WHIRLPOOL" or type instanceof OtherHashType and name = this.getRawAlgorithmName() } + /** + * Gets the type of this hashing algorithm, e.g., MD5 or SHA. + * + * When modeling a new hashing algorithm, use this predicate to specify the type of the algorithm. + */ abstract THashType getHashType(); override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) } + + /** + * Gets the digest size of SHA2 or SHA3 algorithms. + * + * This predicate does not need to hold for other algorithms, + * as the digest size is already known based on the algorithm itself. + * + * For `OtherHashType` algorithms where a digest size should be reported, `THashType` + * should be extended to explicitly model that algorithm. If the algorithm has variable + * or multiple digest size variants, a similar predicate to this one must be defined + * for that algorithm to report the digest size. + */ + abstract string getSHA2OrSHA3DigestSize(Location location); + + bindingset[type] + private string getDigestSize(THashType type, Location location) { + type instanceof MD2 and result = "128" + or + type instanceof MD4 and result = "128" + or + type instanceof MD5 and result = "128" + or + type instanceof SHA1 and result = "160" + or + type instanceof SHA2 and result = this.getSHA2OrSHA3DigestSize(location) + or + type instanceof SHA3 and result = this.getSHA2OrSHA3DigestSize(location) + or + type instanceof RIPEMD160 and result = "160" + or + type instanceof WHIRLPOOL and result = "512" + } + + final override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + // [KNOWN_OR_UNKNOWN] + key = "digest_size" and + if exists(this.getDigestSize(this.getHashType(), location)) + then value = this.getDigestSize(this.getHashType(), location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + } } /** * An operation that derives one or more keys from an input value. */ - abstract class KeyDerivationOperation extends Operation { - override string getOperationName() { result = "KEY_DERIVATION" } + abstract class KeyDerivationOperation extends Operation, TKeyDerivationOperation { + final override Location getLocation() { + exists(LocatableElement le | this = TKeyDerivationOperation(le) and result = le.getLocation()) + } + + override string getOperationName() { result = "KeyDerivationOperation" } } /** * An algorithm that derives one or more keys from an input value. + * + * Only use this class to model UNKNOWN key derivation algorithms. + * + * For known algorithms, use the specialized classes, e.g., `HKDF` and `PKCS12KDF`. */ - abstract class KeyDerivationAlgorithm extends Algorithm { - abstract override string getAlgorithmName(); + abstract class KeyDerivationAlgorithm extends Algorithm, TKeyDerivationAlgorithm { + final override Location getLocation() { + exists(LocatableElement le | this = TKeyDerivationAlgorithm(le) and result = le.getLocation()) + } + + override string getAlgorithmType() { result = "KeyDerivationAlgorithm" } + + override string getAlgorithmName() { result = this.getRawAlgorithmName() } } /** - * HKDF key derivation function + * An algorithm that derives one or more keys from an input value, using a configurable digest algorithm. */ - abstract class HKDF extends KeyDerivationAlgorithm { - final override string getAlgorithmName() { result = "HKDF" } - + abstract private class KeyDerivationWithDigestParameter extends KeyDerivationAlgorithm { abstract HashAlgorithm getHashAlgorithm(); override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or - edgeName = "digest" and result = this.getHashAlgorithm() + ( + // [KNOWN_OR_UNKNOWN] + edgeName = "uses" and + if exists(this.getHashAlgorithm()) then result = this.getHashAlgorithm() else result = this + ) } } /** - * PKCS #12 key derivation function + * HKDF key derivation function */ - abstract class PKCS12KDF extends KeyDerivationAlgorithm { - final override string getAlgorithmName() { result = "PKCS12KDF" } + abstract class HKDF extends KeyDerivationWithDigestParameter { + final override string getAlgorithmName() { result = "HKDF" } + } - abstract HashAlgorithm getHashAlgorithm(); + /** + * PBKDF2 key derivation function + */ + abstract class PBKDF2 extends KeyDerivationWithDigestParameter { + final override string getAlgorithmName() { result = "PBKDF2" } - override NodeBase getChild(string edgeName) { - result = super.getChild(edgeName) + /** + * Gets the iteration count of this key derivation algorithm. + */ + abstract string getIterationCount(Location location); + + /** + * Gets the bit-length of the derived key. + */ + abstract string getKeyLength(Location location); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) or - edgeName = "digest" and result = this.getHashAlgorithm() + ( + // [KNOWN_OR_UNKNOWN] + key = "iterations" and + if exists(this.getIterationCount(location)) + then value = this.getIterationCount(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "key_len" and + if exists(this.getKeyLength(location)) + then value = this.getKeyLength(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + } + } + + /** + * PKCS12KDF key derivation function + */ + abstract class PKCS12KDF extends KeyDerivationWithDigestParameter { + override string getAlgorithmName() { result = "PKCS12KDF" } + + /** + * Gets the iteration count of this key derivation algorithm. + */ + abstract string getIterationCount(Location location); + + /** + * Gets the raw ID argument specifying the intended use of the derived key. + * + * The intended use is defined in RFC 7292, appendix B.3, as follows: + * + * This standard specifies 3 different values for the ID byte mentioned above: + * + * 1. If ID=1, then the pseudorandom bits being produced are to be used + * as key material for performing encryption or decryption. + * + * 2. If ID=2, then the pseudorandom bits being produced are to be used + * as an IV (Initial Value) for encryption or decryption. + * + * 3. If ID=3, then the pseudorandom bits being produced are to be used + * as an integrity key for MACing. + */ + abstract string getIDByte(Location location); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "iterations" and + if exists(this.getIterationCount(location)) + then value = this.getIterationCount(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "id_byte" and + if exists(this.getIDByte(location)) + then value = this.getIDByte(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + } + } + + /** + * scrypt key derivation function + */ + abstract class SCRYPT extends KeyDerivationAlgorithm { + final override string getAlgorithmName() { result = "scrypt" } + + /** + * Gets the iteration count (`N`) argument + */ + abstract string get_N(Location location); + + /** + * Gets the block size (`r`) argument + */ + abstract string get_r(Location location); + + /** + * Gets the parallelization factor (`p`) argument + */ + abstract string get_p(Location location); + + /** + * Gets the derived key length argument + */ + abstract string getDerivedKeyLength(Location location); + + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "N" and + if exists(this.get_N(location)) + then value = this.get_N(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "r" and + if exists(this.get_r(location)) + then value = this.get_r(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "p" and + if exists(this.get_p(location)) + then value = this.get_p(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) + or + ( + // [KNOWN_OR_UNKNOWN] + key = "key_len" and + if exists(this.getDerivedKeyLength(location)) + then value = this.getDerivedKeyLength(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) + ) } } @@ -246,7 +508,7 @@ module CryptographyBase Input> { /** * Elliptic curve algorithms */ - newtype TEllipticCurveFamily = + newtype TEllipticCurveType = NIST() or SEC() or NUMS() or @@ -257,16 +519,17 @@ module CryptographyBase Input> { C2() or SM2() or ES() or - OtherEllipticCurveFamilyType() + OtherEllipticCurveType() - abstract class EllipticCurve extends Algorithm { + abstract class EllipticCurve extends Algorithm, TEllipticCurveAlgorithm { abstract string getKeySize(Location location); - abstract TEllipticCurveFamily getCurveFamilyType(); + abstract TEllipticCurveType getCurveFamily(); override predicate properties(string key, string value, Location location) { super.properties(key, value, location) or + // [KNOWN_OR_UNKNOWN] key = "key_size" and if exists(this.getKeySize(location)) then value = this.getKeySize(location) @@ -306,62 +569,168 @@ module CryptographyBase Input> { /** * Block cipher modes of operation algorithms */ - newtype TModeOperation = + newtype TModeOperationType = ECB() or CBC() or + CFB() or + OFB() or + CTR() or + GCM() or + CCM() or + XTS() or OtherMode() abstract class ModeOfOperation extends Algorithm { - final private predicate modeToNameMapping(TModeOperation type, string name) { + override string getAlgorithmType() { result = "ModeOfOperation" } + + /** + * Gets the type of this mode of operation, e.g., "ECB" or "CBC". + * + * When modeling a new mode of operation, use this predicate to specify the type of the mode. + */ + abstract TModeOperationType getModeType(); + + bindingset[type] + final predicate modeToNameMapping(TModeOperationType type, string name) { type instanceof ECB and name = "ECB" or type instanceof CBC and name = "CBC" or + type instanceof CFB and name = "CFB" + or + type instanceof OFB and name = "OFB" + or + type instanceof CTR and name = "CTR" + or + type instanceof GCM and name = "GCM" + or + type instanceof CCM and name = "CCM" + or + type instanceof XTS and name = "XTS" + or type instanceof OtherMode and name = this.getRawAlgorithmName() } - abstract TModeOperation getModeType(); - override string getAlgorithmName() { this.modeToNameMapping(this.getModeType(), result) } } /** * A helper type for distinguishing between block and stream ciphers. */ - newtype TCipherStructure = + newtype TCipherStructureType = Block() or - Stream() + Stream() or + UnknownCipherStructureType() + + private string getCipherStructureTypeString(TCipherStructureType type) { + type instanceof Block and result = "Block" + or + type instanceof Stream and result = "Stream" + or + type instanceof UnknownCipherStructureType and result instanceof UnknownPropertyValue + } /** * Symmetric algorithms */ - newtype TSymmetricCipherFamilyType = + newtype TSymmetricCipherType = AES() or - OtherSymmetricCipherFamilyType() + Camellia() or + DES() or + TripleDES() or + IDEA() or + CAST5() or + ChaCha20() or + RC4() or + RC5() or + OtherSymmetricCipherType() abstract class SymmetricAlgorithm extends Algorithm { - abstract TSymmetricCipherFamilyType getSymmetricCipherFamilyType(); + final TCipherStructureType getCipherStructure() { + this.cipherFamilyToNameAndStructure(this.getCipherFamily(), _, result) + } + + final override string getAlgorithmName() { + this.cipherFamilyToNameAndStructure(this.getCipherFamily(), result, _) + } + final override string getAlgorithmType() { result = "SymmetricAlgorithm" } + + /** + * Gets the key size of this symmetric cipher, e.g., "128" or "256". + */ abstract string getKeySize(Location location); - abstract TCipherStructure getCipherType(); + /** + * Gets the type of this symmetric cipher, e.g., "AES" or "ChaCha20". + */ + abstract TSymmetricCipherType getCipherFamily(); + + /** + * Gets the mode of operation of this symmetric cipher, e.g., "GCM" or "CBC". + */ + abstract ModeOfOperation getModeOfOperation(); + + bindingset[type] + final private predicate cipherFamilyToNameAndStructure( + TSymmetricCipherType type, string name, TCipherStructureType s + ) { + type instanceof AES and name = "AES" and s = Block() + or + type instanceof Camellia and name = "Camellia" and s = Block() + or + type instanceof DES and name = "DES" and s = Block() + or + type instanceof TripleDES and name = "TripleDES" and s = Block() + or + type instanceof IDEA and name = "IDEA" and s = Block() + or + type instanceof CAST5 and name = "CAST5" and s = Block() + or + type instanceof ChaCha20 and name = "ChaCha20" and s = Stream() + or + type instanceof RC4 and name = "RC4" and s = Stream() + or + type instanceof RC5 and name = "RC5" and s = Block() + or + type instanceof OtherSymmetricCipherType and + name = this.getRawAlgorithmName() and + s = UnknownCipherStructureType() + } //mode, padding scheme, keysize, block/stream, auth'd //nodes = mode, padding scheme //properties = keysize, block/stream, auth'd //leave authd to lang specific + override NodeBase getChild(string edgeName) { + result = super.getChild(edgeName) + or + ( + // [KNOWN_OR_UNKNOWN] + edgeName = "mode" and + if exists(this.getModeOfOperation()) + then result = this.getModeOfOperation() + else result = this + ) + } + override predicate properties(string key, string value, Location location) { super.properties(key, value, location) or - key = "key_size" and - if exists(this.getKeySize(location)) - then value = this.getKeySize(location) - else ( - value instanceof UnknownPropertyValue and location instanceof UnknownLocation + // [ALWAYS_KNOWN]: unknown case is handled in `getCipherStructureTypeString` + key = "structure" and + getCipherStructureTypeString(this.getCipherStructure()) = value and + location instanceof UnknownLocation + or + ( + // [KNOWN_OR_UNKNOWN] + key = "key_size" and + if exists(this.getKeySize(location)) + then value = this.getKeySize(location) + else ( + value instanceof UnknownPropertyValue and location instanceof UnknownLocation + ) ) - //add more keys to index props } - - abstract ModeOfOperation getModeOfOperation(); } } From b777a22d3578a057e58082310b2ab9e7a01b522e Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Fri, 14 Feb 2025 23:43:07 +0100 Subject: [PATCH 18/28] Expand model and specialize newtype relations --- cpp/ql/lib/experimental/Quantum/OpenSSL.qll | 62 ++++---- java/ql/lib/experimental/Quantum/JCA.qll | 116 ++++++++------- java/ql/src/experimental/Quantum/Test.ql | 2 +- .../codeql/cryptography/Model.qll | 135 ++++++++++++++---- 4 files changed, 203 insertions(+), 112 deletions(-) diff --git a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll index cb19092f3fd7..821fc0aec8ff 100644 --- a/cpp/ql/lib/experimental/Quantum/OpenSSL.qll +++ b/cpp/ql/lib/experimental/Quantum/OpenSSL.qll @@ -4,16 +4,6 @@ import semmle.code.cpp.dataflow.new.DataFlow module OpenSSLModel { import Language - class FunctionCallOrMacroAccess extends Element { - FunctionCallOrMacroAccess() { this instanceof FunctionCall or this instanceof MacroAccess } - - string getTargetName() { - result = this.(FunctionCall).getTarget().getName() - or - result = this.(MacroAccess).getMacroName() - } - } - /** * Hash function references in OpenSSL. */ @@ -42,13 +32,27 @@ module OpenSSLModel { hash_ref_type_mapping_known(name, algo) } - class HashAlgorithmRef extends Crypto::HashAlgorithm { - FunctionCallOrMacroAccess instance; + class FunctionCallOrMacroAccess extends Element { + FunctionCallOrMacroAccess() { this instanceof FunctionCall or this instanceof MacroAccess } - HashAlgorithmRef() { - this = Crypto::THashAlgorithm(instance) and - hash_ref_type_mapping(instance, _, _) + string getTargetName() { + result = this.(FunctionCall).getTarget().getName() + or + result = this.(MacroAccess).getMacroName() } + } + + class HashAlgorithmCallOrMacro extends Crypto::HashAlgorithmInstance instanceof FunctionCallOrMacroAccess + { + HashAlgorithmCallOrMacro() { hash_ref_type_mapping(this, _, _) } + + string getTargetName() { result = this.(FunctionCallOrMacroAccess).getTargetName() } + } + + class HashAlgorithm extends Crypto::HashAlgorithm { + HashAlgorithmCallOrMacro instance; + + HashAlgorithm() { this = Crypto::THashAlgorithm(instance) } override string getSHA2OrSHA3DigestSize(Location location) { ( @@ -81,9 +85,9 @@ module OpenSSLModel { predicate isSink(DataFlow::Node sink) { exists(EVP_KDF_derive kdo | - sink.asExpr() = kdo.getAlgorithmArg() + sink.asExpr() = kdo.getCall().getAlgorithmArg() or - sink.asExpr() = kdo.getContextArg() // via `EVP_KDF_CTX_set_params` + sink.asExpr() = kdo.getCall().getContextArg() // via `EVP_KDF_CTX_set_params` ) } @@ -101,21 +105,23 @@ module OpenSSLModel { /** * Key derivation operation (e.g., `EVP_KDF_derive`) */ - abstract class KeyDerivationOperation extends Crypto::KeyDerivationOperation { } + class EVP_KDF_derive_FunctionCall extends Crypto::KeyDerivationOperationInstance instanceof FunctionCall + { + EVP_KDF_derive_FunctionCall() { this.getTarget().getName() = "EVP_KDF_derive" } - class EVP_KDF_derive extends KeyDerivationOperation { - FunctionCall instance; + Expr getAlgorithmArg() { result = super.getArgument(3) } - EVP_KDF_derive() { - this = Crypto::TKeyDerivationOperation(instance) and - instance.getTarget().getName() = "EVP_KDF_derive" - } + Expr getContextArg() { result = super.getArgument(0) } + } - override Crypto::Algorithm getAlgorithm() { algorithm_to_EVP_KDF_derive(result, this) } + class EVP_KDF_derive extends Crypto::KeyDerivationOperation { + EVP_KDF_derive_FunctionCall instance; + + EVP_KDF_derive() { this = Crypto::TKeyDerivationOperation(instance) } - Expr getAlgorithmArg() { result = instance.getArgument(3) } + override Crypto::Algorithm getAlgorithm() { algorithm_to_EVP_KDF_derive(result, this) } - Expr getContextArg() { result = instance.getArgument(0) } + EVP_KDF_derive_FunctionCall getCall() { result = instance } } /** @@ -134,7 +140,7 @@ module OpenSSLModel { Expr getAlgorithmArg() { result = this.getArgument(1) } } - class EVP_KDF_fetch_AlgorithmArg extends Expr { + class EVP_KDF_fetch_AlgorithmArg extends Crypto::KeyDerivationAlgorithmInstance instanceof Expr { EVP_KDF_fetch_AlgorithmArg() { exists(EVP_KDF_fetch_Call call | this = call.getAlgorithmArg()) } } diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 807dec96ba40..299d9558ee10 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -4,12 +4,9 @@ import semmle.code.java.dataflow.DataFlow module JCAModel { import Language - abstract class EncryptionOperation extends Crypto::EncryptionOperation { } - - //TODO PBEWith can have suffixes. how to do? enumerate? or match a pattern? + // TODO: Verify that the PBEWith% case works correctly bindingset[algo] predicate cipher_names(string algo) { - // "Standard names are not case-sensitive." algo.toUpperCase() .matches([ "AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", @@ -17,26 +14,29 @@ module JCAModel { ].toUpperCase()) } - //TODO solve the fact that x is an int of various values. same as above... enumerate? + // TODO: Verify that the CFB% case works correctly + bindingset[mode] predicate cipher_modes(string mode) { - mode = - [ - "NONE", "CBC", "CCM", "CFB", "CFBx", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB", "OFBx", - "PCBC" - ] + mode.toUpperCase() + .matches([ + "NONE", "CBC", "CCM", "CFB", "CFB%", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB", + "OFB%", "PCBC" + ].toUpperCase()) } - //todo same as above, OAEPWith has asuffix type + // TODO: Verify that the OAEPWith% case works correctly + bindingset[padding] predicate cipher_padding(string padding) { - padding = - [ - "NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", - "SSL3Padding" - ] + padding + .toUpperCase() + .matches([ + "NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith%", "PKCS1Padding", + "PKCS5Padding", "SSL3Padding" + ].toUpperCase()) } /** - * this may be specified either in the ALG/MODE/PADDING or just ALG format + * A `StringLiteral` in the `"ALG/MODE/PADDING"` or `"ALG"` format */ class CipherStringLiteral extends StringLiteral { CipherStringLiteral() { cipher_names(this.getValue().splitAt("/")) } @@ -56,6 +56,9 @@ module JCAModel { Expr getAlgorithmArg() { result = this.getArgument(0) } } + /** + * Data-flow configuration modelling flow from a cipher string literal to a `CipherGetInstanceCall` argument. + */ private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig { predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherStringLiteral } @@ -66,70 +69,77 @@ module JCAModel { module AlgorithmStringToFetchFlow = DataFlow::Global; - class CipherGetInstanceAlgorithmArg extends Expr { + /** + * The cipher algorithm argument to a `CipherGetInstanceCall`. + * + * For example, in `Cipher.getInstance(algorithm)`, this class represents `algorithm`. + */ + class CipherGetInstanceAlgorithmArg extends Crypto::EncryptionAlgorithmInstance, + Crypto::ModeOfOperationAlgorithmInstance instanceof Expr + { CipherGetInstanceAlgorithmArg() { exists(CipherGetInstanceCall call | this = call.getArgument(0)) } - StringLiteral getOrigin() { - AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(result), DataFlow::exprNode(this)) + /** + * Returns the `StringLiteral` from which this argument is derived, if known. + */ + CipherStringLiteral getOrigin() { + AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(result), + DataFlow::exprNode(this.(Expr).getAChildExpr*())) } } - class ModeStringLiteral extends Crypto::ModeOfOperation { - CipherStringLiteral instance; + /** + * A block cipher mode of operation, where the mode is specified in the ALG or ALG/MODE/PADDING format. + * + * This class will only exist when the mode (*and its type*) is determinable. + * This is because the mode will always be specified alongside the algorithm and never independently. + * Therefore, we can always assume that a determinable algorithm will have a determinable mode. + * + * In the case that only an algorithm is specified, e.g., "AES", the provider provides a default mode. + * + * TODO: Model the case of relying on a provider default, but alert on it as a bad practice. + */ + class ModeOfOperation extends Crypto::ModeOfOperationAlgorithm { + CipherGetInstanceAlgorithmArg instance; - ModeStringLiteral() { + ModeOfOperation() { this = Crypto::TModeOfOperationAlgorithm(instance) and - exists(instance.getMode()) and - instance = any(CipherGetInstanceAlgorithmArg call).getOrigin() + // TODO: this currently only holds for explicitly defined modes in a string literal. + // Cases with defaults, e.g., "AES", are not yet modelled. + // For these cases, in a CBOM, the AES node would have an unknown edge to its mode child. + exists(instance.getOrigin().getMode()) } override Location getLocation() { result = instance.getLocation() } - override string getRawAlgorithmName() { result = instance.getMode() } + override string getRawAlgorithmName() { result = instance.getOrigin().getValue() } predicate modeToNameMapping(Crypto::TModeOperationType type, string name) { super.modeToNameMapping(type, name) } override Crypto::TModeOperationType getModeType() { - this.modeToNameMapping(result, instance.getMode().toUpperCase()) + this.modeToNameMapping(result, instance.getOrigin().getMode()) } CipherStringLiteral getInstance() { result = instance } } - //todo refactor - // class CipherAlgorithmPaddingStringLiteral extends CipherAlgorithmPadding instanceof StringLiteral { - // CipherAlgorithmPaddingStringLiteral() { - // cipher_padding(this.(StringLiteral).getValue().splitAt("/")) - // } - // override string toString() { result = this.(StringLiteral).toString() } - // override string getValue() { - // result = this.(StringLiteral).getValue().regexpCapture(".*/.*/(.*)", 1) - // } - // } - /** - * A class to represent when AES is used - * AND currently it has literal mode and padding provided - * - * this currently does not capture the use without a literal - * though should be extended to - */ - class CipherAlgorithm extends Crypto::SymmetricAlgorithm { + class EncryptionAlgorithm extends Crypto::EncryptionAlgorithm { CipherStringLiteral origin; CipherGetInstanceAlgorithmArg instance; - CipherAlgorithm() { - this = Crypto::TSymmetricAlgorithm(instance) and + EncryptionAlgorithm() { + this = Crypto::TEncryptionAlgorithm(instance) and instance.getOrigin() = origin } override Location getLocation() { result = instance.getLocation() } - override Crypto::ModeOfOperation getModeOfOperation() { - result.(ModeStringLiteral).getInstance() = origin + override Crypto::ModeOfOperationAlgorithm getModeOfOperation() { + result.(ModeOfOperation).getInstance() = origin } override Crypto::LocatableElement getOrigin(string name) { @@ -138,23 +148,25 @@ module JCAModel { override string getRawAlgorithmName() { result = origin.getValue() } - override Crypto::TSymmetricCipherType getCipherFamily() { + override Crypto::TCipherType getCipherFamily() { this.cipherNameMapping(result, origin.getAlgorithmName()) } override string getKeySize(Location location) { none() } bindingset[name] - private predicate cipherNameMappingKnown(Crypto::TSymmetricCipherType type, string name) { + private predicate cipherNameMappingKnown(Crypto::TCipherType type, string name) { name = "AES" and type instanceof Crypto::AES or name = "RC4" and type instanceof Crypto::RC4 + // or + // TODO } bindingset[name] - predicate cipherNameMapping(Crypto::TSymmetricCipherType type, string name) { + predicate cipherNameMapping(Crypto::TCipherType type, string name) { this.cipherNameMappingKnown(type, name) or not this.cipherNameMappingKnown(_, name) and diff --git a/java/ql/src/experimental/Quantum/Test.ql b/java/ql/src/experimental/Quantum/Test.ql index f3ae23a2ccac..5496e5a70cf9 100644 --- a/java/ql/src/experimental/Quantum/Test.ql +++ b/java/ql/src/experimental/Quantum/Test.ql @@ -4,6 +4,6 @@ import experimental.Quantum.Language -from Crypto::SymmetricAlgorithm a, Crypto::ModeOfOperation mode +from Crypto::EncryptionAlgorithm a, Crypto::ModeOfOperationAlgorithm mode where a.getModeOfOperation() = mode select a, a.getAlgorithmName(), a.getRawAlgorithmName(), mode, mode.getAlgorithmName() diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index dd570a89ef6e..38ea6e475c05 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -8,6 +8,8 @@ import codeql.util.Option signature module InputSig { class LocatableElement { Location getLocation(); + + string toString(); } class UnknownLocation instanceof Location; @@ -56,15 +58,67 @@ module CryptographyBase Input> { not source = target } + /** + * All elements in the database that are mapped to nodes must extend the following classes + */ + abstract class HashOperationInstance extends LocatableElement { } + + abstract class HashAlgorithmInstance extends LocatableElement { } + + abstract class KeyDerivationOperationInstance extends LocatableElement { } + + abstract class KeyDerivationAlgorithmInstance extends LocatableElement { } + + abstract class EncryptionOperationInstance extends LocatableElement { } + + abstract class EncryptionAlgorithmInstance extends LocatableElement { } + + abstract class KeyEncapsulationOperationInstance extends LocatableElement { } + + abstract class KeyEncapsulationAlgorithmInstance extends LocatableElement { } + + abstract class EllipticCurveAlgorithmInstance extends LocatableElement { } + + // Non-standalone algorithms + abstract class ModeOfOperationAlgorithmInstance extends LocatableElement { } + + abstract class PaddingAlgorithmInstance extends LocatableElement { } + + // Artifacts + abstract class DigestArtifactInstance extends LocatableElement { } + + abstract class KeyArtifactInstance extends LocatableElement { } + + abstract class InitializationVectorArtifactInstance extends LocatableElement { } + + abstract class NonceArtifactInstance extends LocatableElement { } + newtype TNode = - THashOperation(LocatableElement e) or - THashAlgorithm(LocatableElement e) or - TKeyDerivationOperation(LocatableElement e) or - TKeyDerivationAlgorithm(LocatableElement e) or - TEncryptionOperation(LocatableElement e) or - TSymmetricAlgorithm(LocatableElement e) or - TEllipticCurveAlgorithm(LocatableElement e) or - TModeOfOperationAlgorithm(LocatableElement e) + // Artifacts (data that is not an operation or algorithm, e.g., a key) + TDigest(DigestArtifactInstance e) or + TKey(KeyArtifactInstance e) or + TInitializationVector(InitializationVectorArtifactInstance e) or + TNonce(NonceArtifactInstance e) or + // Operations (e.g., hashing, encryption) + THashOperation(HashOperationInstance e) or + TKeyDerivationOperation(KeyDerivationOperationInstance e) or + TEncryptionOperation(EncryptionOperationInstance e) or + TKeyEncapsulationOperation(KeyEncapsulationOperationInstance e) or + // Algorithms (e.g., SHA-256, AES) + TEncryptionAlgorithm(EncryptionAlgorithmInstance e) or + TEllipticCurveAlgorithm(EllipticCurveAlgorithmInstance e) or + THashAlgorithm(HashAlgorithmInstance e) or + TKeyDerivationAlgorithm(KeyDerivationAlgorithmInstance e) or + TKeyEncapsulationAlgorithm(KeyEncapsulationAlgorithmInstance e) or + // Non-standalone Algorithms (e.g., Mode, Padding) + TModeOfOperationAlgorithm(ModeOfOperationAlgorithmInstance e) or + TPaddingAlgorithm(PaddingAlgorithmInstance e) or + // Composite and hybrid cryptosystems (e.g., RSA-OAEP used with AES, post-quantum hybrid cryptosystems) + // These nodes are always parent nodes and are not modeled but rather defined via library-agnostic patterns. + TKemDemHybridCryptosystem(EncryptionAlgorithmInstance dem) or + TKeyAgreementHybridCryptosystem(EncryptionAlgorithmInstance ka) or + TAsymmetricEncryptionMacHybridCryptosystem(EncryptionAlgorithmInstance enc) or + TPostQuantumHybridCryptosystem(EncryptionAlgorithmInstance enc) /** * The base class for all cryptographic assets, such as operations and algorithms. @@ -90,14 +144,14 @@ module CryptographyBase Input> { /** * Returns the child of this node with the given edge name. * - * This predicate is used by derived classes to construct the graph of cryptographic operations. + * This predicate is overriden by derived classes to construct the graph of cryptographic operations. */ NodeBase getChild(string edgeName) { none() } /** * Defines properties of this node by name and either a value or location or both. * - * This predicate is used by derived classes to construct the graph of cryptographic operations. + * This predicate is overriden by derived classes to construct the graph of cryptographic operations. */ predicate properties(string key, string value, Location location) { key = "origin" and @@ -113,6 +167,8 @@ module CryptographyBase Input> { class Asset = NodeBase; + class Artifact = NodeBase; + /** * A cryptographic operation, such as hashing or encryption. */ @@ -125,9 +181,9 @@ module CryptographyBase Input> { /** * Gets the name of this operation, e.g., "hash" or "encrypt". */ - abstract string getOperationName(); + abstract string getOperationType(); - final override string toString() { result = this.getOperationName() } + final override string toString() { result = this.getOperationType() } override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) @@ -175,7 +231,7 @@ module CryptographyBase Input> { abstract class HashOperation extends Operation, THashOperation { abstract override HashAlgorithm getAlgorithm(); - override string getOperationName() { result = "HashOperation" } + override string getOperationType() { result = "HashOperation" } } newtype THashType = @@ -238,7 +294,7 @@ module CryptographyBase Input> { abstract string getSHA2OrSHA3DigestSize(Location location); bindingset[type] - private string getDigestSize(THashType type, Location location) { + private string type_to_digest_size_fixed(THashType type) { type instanceof MD2 and result = "128" or type instanceof MD4 and result = "128" @@ -247,15 +303,20 @@ module CryptographyBase Input> { or type instanceof SHA1 and result = "160" or - type instanceof SHA2 and result = this.getSHA2OrSHA3DigestSize(location) - or - type instanceof SHA3 and result = this.getSHA2OrSHA3DigestSize(location) - or type instanceof RIPEMD160 and result = "160" or type instanceof WHIRLPOOL and result = "512" } + bindingset[type] + private string getDigestSize(THashType type, Location location) { + result = this.type_to_digest_size_fixed(type) and location = this.getLocation() + or + type instanceof SHA2 and result = this.getSHA2OrSHA3DigestSize(location) + or + type instanceof SHA3 and result = this.getSHA2OrSHA3DigestSize(location) + } + final override predicate properties(string key, string value, Location location) { super.properties(key, value, location) or @@ -277,7 +338,7 @@ module CryptographyBase Input> { exists(LocatableElement le | this = TKeyDerivationOperation(le) and result = le.getLocation()) } - override string getOperationName() { result = "KeyDerivationOperation" } + override string getOperationType() { result = "KeyDerivationOperation" } } /** @@ -560,10 +621,10 @@ module CryptographyBase Input> { * An encryption operation that processes plaintext to generate a ciphertext. * This operation takes an input message (plaintext) of arbitrary content and length and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). */ - abstract class EncryptionOperation extends Operation { + abstract class EncryptionOperation extends Operation, TEncryptionOperation { abstract override Algorithm getAlgorithm(); - override string getOperationName() { result = "ENCRYPTION" } + override string getOperationType() { result = "EncryptionOperation" } } /** @@ -578,15 +639,18 @@ module CryptographyBase Input> { GCM() or CCM() or XTS() or + OAEP() or OtherMode() - abstract class ModeOfOperation extends Algorithm { + abstract class ModeOfOperationAlgorithm extends Algorithm, TModeOfOperationAlgorithm { override string getAlgorithmType() { result = "ModeOfOperation" } /** * Gets the type of this mode of operation, e.g., "ECB" or "CBC". * * When modeling a new mode of operation, use this predicate to specify the type of the mode. + * + * If a type cannot be determined, the result is `OtherMode`. */ abstract TModeOperationType getModeType(); @@ -633,7 +697,7 @@ module CryptographyBase Input> { /** * Symmetric algorithms */ - newtype TSymmetricCipherType = + newtype TCipherType = AES() or Camellia() or DES() or @@ -643,9 +707,12 @@ module CryptographyBase Input> { ChaCha20() or RC4() or RC5() or + RSA() or OtherSymmetricCipherType() - abstract class SymmetricAlgorithm extends Algorithm { + abstract class EncryptionAlgorithm extends Algorithm, TEncryptionAlgorithm { + final LocatableElement getInstance() { this = TEncryptionAlgorithm(result) } + final TCipherStructureType getCipherStructure() { this.cipherFamilyToNameAndStructure(this.getCipherFamily(), _, result) } @@ -654,26 +721,26 @@ module CryptographyBase Input> { this.cipherFamilyToNameAndStructure(this.getCipherFamily(), result, _) } - final override string getAlgorithmType() { result = "SymmetricAlgorithm" } + final override string getAlgorithmType() { result = "EncryptionAlgorithm" } /** - * Gets the key size of this symmetric cipher, e.g., "128" or "256". + * Gets the key size of this cipher, e.g., "128" or "256". */ abstract string getKeySize(Location location); /** - * Gets the type of this symmetric cipher, e.g., "AES" or "ChaCha20". + * Gets the type of this cipher, e.g., "AES" or "ChaCha20". */ - abstract TSymmetricCipherType getCipherFamily(); + abstract TCipherType getCipherFamily(); /** - * Gets the mode of operation of this symmetric cipher, e.g., "GCM" or "CBC". + * Gets the mode of operation of this cipher, e.g., "GCM" or "CBC". */ - abstract ModeOfOperation getModeOfOperation(); + abstract ModeOfOperationAlgorithm getModeOfOperation(); bindingset[type] final private predicate cipherFamilyToNameAndStructure( - TSymmetricCipherType type, string name, TCipherStructureType s + TCipherType type, string name, TCipherStructureType s ) { type instanceof AES and name = "AES" and s = Block() or @@ -693,6 +760,8 @@ module CryptographyBase Input> { or type instanceof RC5 and name = "RC5" and s = Block() or + type instanceof RSA and name = "RSA" and s = Block() + or type instanceof OtherSymmetricCipherType and name = this.getRawAlgorithmName() and s = UnknownCipherStructureType() @@ -733,4 +802,8 @@ module CryptographyBase Input> { ) } } + + abstract class KEMAlgorithm extends TKeyEncapsulationAlgorithm, Algorithm { + final override string getAlgorithmType() { result = "KeyEncapsulationAlgorithm" } + } } From df01fa7a9cd6a3b8c750c47d658ec4f6e37cd3c6 Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Mon, 17 Feb 2025 00:16:08 +0100 Subject: [PATCH 19/28] Expand model and JCA modeling --- java/ql/lib/experimental/Quantum/JCA.qll | 149 ++++++++++++++++-- java/ql/src/experimental/Quantum/Test.ql | 6 +- .../codeql/cryptography/Model.qll | 124 ++++++++++++--- 3 files changed, 237 insertions(+), 42 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 299d9558ee10..5a30e96b13ca 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -54,6 +54,8 @@ module JCAModel { } Expr getAlgorithmArg() { result = this.getArgument(0) } + + Expr getProviderArg() { result = this.getArgument(1) } } /** @@ -75,7 +77,7 @@ module JCAModel { * For example, in `Cipher.getInstance(algorithm)`, this class represents `algorithm`. */ class CipherGetInstanceAlgorithmArg extends Crypto::EncryptionAlgorithmInstance, - Crypto::ModeOfOperationAlgorithmInstance instanceof Expr + Crypto::ModeOfOperationAlgorithmInstance, Crypto::PaddingAlgorithmInstance instanceof Expr { CipherGetInstanceAlgorithmArg() { exists(CipherGetInstanceCall call | this = call.getArgument(0)) @@ -114,14 +116,62 @@ module JCAModel { override Location getLocation() { result = instance.getLocation() } - override string getRawAlgorithmName() { result = instance.getOrigin().getValue() } + // In this case, the raw name is still only the /MODE/ part. + // TODO: handle defaults + override string getRawAlgorithmName() { result = instance.getOrigin().getMode() } - predicate modeToNameMapping(Crypto::TModeOperationType type, string name) { - super.modeToNameMapping(type, name) + private predicate modeToNameMappingKnown(Crypto::TModeOperationType type, string name) { + type instanceof Crypto::ECB and name = "ECB" + or + type instanceof Crypto::CBC and name = "CBC" + or + type instanceof Crypto::GCM and name = "GCM" + or + type instanceof Crypto::CTR and name = "CTR" + or + type instanceof Crypto::XTS and name = "XTS" + or + type instanceof Crypto::CCM and name = "CCM" + or + type instanceof Crypto::SIV and name = "SIV" + or + type instanceof Crypto::OCB and name = "OCB" } override Crypto::TModeOperationType getModeType() { - this.modeToNameMapping(result, instance.getOrigin().getMode()) + if this.modeToNameMappingKnown(_, instance.getOrigin().getMode()) + then this.modeToNameMappingKnown(result, instance.getOrigin().getMode()) + else result instanceof Crypto::OtherMode + } + + CipherStringLiteral getInstance() { result = instance } + } + + class PaddingAlgorithm extends Crypto::PaddingAlgorithm { + CipherGetInstanceAlgorithmArg instance; + + PaddingAlgorithm() { + this = Crypto::TPaddingAlgorithm(instance) and + exists(instance.getOrigin().getPadding()) + } + + override Location getLocation() { result = instance.getLocation() } + + override string getRawAlgorithmName() { result = instance.getOrigin().getPadding() } + + bindingset[name] + private predicate paddingToNameMappingKnown(Crypto::TPaddingType type, string name) { + type instanceof Crypto::NoPadding and name = "NOPADDING" + or + type instanceof Crypto::PKCS7 and name = ["PKCS5Padding", "PKCS7Padding"] // TODO: misnomer in the JCA? + or + type instanceof Crypto::OAEP and name.matches("OAEP%") // TODO: handle OAEPWith% + } + + override Crypto::TPaddingType getPaddingType() { + if this.paddingToNameMappingKnown(_, instance.getOrigin().getPadding()) + then this.paddingToNameMappingKnown(result, instance.getOrigin().getPadding()) + else result instanceof Crypto::OtherPadding } CipherStringLiteral getInstance() { result = instance } @@ -142,6 +192,10 @@ module JCAModel { result.(ModeOfOperation).getInstance() = origin } + override Crypto::PaddingAlgorithm getPadding() { + result.(PaddingAlgorithm).getInstance() = origin + } + override Crypto::LocatableElement getOrigin(string name) { result = origin and name = origin.toString() } @@ -149,7 +203,9 @@ module JCAModel { override string getRawAlgorithmName() { result = origin.getValue() } override Crypto::TCipherType getCipherFamily() { - this.cipherNameMapping(result, origin.getAlgorithmName()) + if this.cipherNameMappingKnown(_, origin.getAlgorithmName()) + then this.cipherNameMappingKnown(result, origin.getAlgorithmName()) + else result instanceof Crypto::OtherSymmetricCipherType } override string getKeySize(Location location) { none() } @@ -159,18 +215,83 @@ module JCAModel { name = "AES" and type instanceof Crypto::AES or + name = "DES" and + type instanceof Crypto::DES + or + name = "TripleDES" and + type instanceof Crypto::TripleDES + or + name = "IDEA" and + type instanceof Crypto::IDEA + or + name = "CAST5" and + type instanceof Crypto::CAST5 + or + name = "ChaCha20" and + type instanceof Crypto::ChaCha20 + or name = "RC4" and type instanceof Crypto::RC4 - // or - // TODO + or + name = "RC5" and + type instanceof Crypto::RC5 + or + name = "RSA" and + type instanceof Crypto::RSA } + } - bindingset[name] - predicate cipherNameMapping(Crypto::TCipherType type, string name) { - this.cipherNameMappingKnown(type, name) - or - not this.cipherNameMappingKnown(_, name) and - type instanceof Crypto::OtherSymmetricCipherType + /** + * Initialiation vectors + */ + abstract class IVParameterInstantiation extends ClassInstanceExpr { + abstract Expr getIV(); + } + + class IvParameterSpecInstance extends IVParameterInstantiation { + IvParameterSpecInstance() { + this.getConstructedType().hasQualifiedName("javax.crypto.spec", "IvParameterSpec") + } + + override Expr getIV() { result = super.getArgument(0) } + } + + class GCMParameterSpecInstance extends IVParameterInstantiation { + GCMParameterSpecInstance() { + this.getConstructedType().hasQualifiedName("javax.crypto.spec", "GCMParameterSpec") } + + override Expr getIV() { result = super.getArgument(1) } + } + + class CipherInitCall extends MethodCall { + CipherInitCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "init") } + + Expr getModeArg() { result = this.getArgument(0) } + + Expr getKey() { + result = this.getArgument(1) and this.getMethod().getParameterType(1).hasName("Key") + } + + Expr getIV() { + result = this.getArgument(2) and + this.getMethod().getParameterType(2).hasName("AlgorithmParameterSpec") + } + } + + // TODO: cipher.getParameters().getParameterSpec(GCMParameterSpec.class); + class InitializationVectorExpr extends Crypto::InitializationVectorArtifactInstance instanceof Expr + { + CipherInitCall call; // TODO: add origin to known sources (e.g. RNG, etc.) + + InitializationVectorExpr() { this = call.getIV() } + } + + class InitializationVector extends Crypto::InitializationVector { + InitializationVectorExpr instance; + + InitializationVector() { this = Crypto::TInitializationVector(instance) } + + override Location getLocation() { result = instance.getLocation() } } } diff --git a/java/ql/src/experimental/Quantum/Test.ql b/java/ql/src/experimental/Quantum/Test.ql index 5496e5a70cf9..ba76213132c3 100644 --- a/java/ql/src/experimental/Quantum/Test.ql +++ b/java/ql/src/experimental/Quantum/Test.ql @@ -4,6 +4,6 @@ import experimental.Quantum.Language -from Crypto::EncryptionAlgorithm a, Crypto::ModeOfOperationAlgorithm mode -where a.getModeOfOperation() = mode -select a, a.getAlgorithmName(), a.getRawAlgorithmName(), mode, mode.getAlgorithmName() +from Crypto::EncryptionAlgorithm a, Crypto::ModeOfOperationAlgorithm m, Crypto::PaddingAlgorithm p +where m = a.getModeOfOperation() and p = a.getPadding() +select a, a.getRawAlgorithmName(), m, m.getRawAlgorithmName(), p, p.getRawAlgorithmName() diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 38ea6e475c05..9814f1519950 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -115,7 +115,7 @@ module CryptographyBase Input> { TPaddingAlgorithm(PaddingAlgorithmInstance e) or // Composite and hybrid cryptosystems (e.g., RSA-OAEP used with AES, post-quantum hybrid cryptosystems) // These nodes are always parent nodes and are not modeled but rather defined via library-agnostic patterns. - TKemDemHybridCryptosystem(EncryptionAlgorithmInstance dem) or + TKemDemHybridCryptosystem(EncryptionAlgorithmInstance dem) or // TODO, change this relation and the below ones TKeyAgreementHybridCryptosystem(EncryptionAlgorithmInstance ka) or TAsymmetricEncryptionMacHybridCryptosystem(EncryptionAlgorithmInstance enc) or TPostQuantumHybridCryptosystem(EncryptionAlgorithmInstance enc) @@ -131,6 +131,11 @@ module CryptographyBase Input> { */ abstract string toString(); + /** + * Returns a string representation of the internal type of this node, usually the name of the class. + */ + abstract string getInternalType(); + /** * Returns the location of this node in the code. */ @@ -169,6 +174,15 @@ module CryptographyBase Input> { class Artifact = NodeBase; + /** + * An initialization vector + */ + abstract class InitializationVector extends Asset, TInitializationVector { + final override string getInternalType() { result = "InitializationVector" } + + final override string toString() { result = this.getInternalType() } + } + /** * A cryptographic operation, such as hashing or encryption. */ @@ -185,6 +199,8 @@ module CryptographyBase Input> { final override string toString() { result = this.getOperationType() } + final override string getInternalType() { result = this.getOperationType() } + override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or @@ -196,6 +212,8 @@ module CryptographyBase Input> { abstract class Algorithm extends Asset { final override string toString() { result = this.getAlgorithmType() } + final override string getInternalType() { result = this.getAlgorithmType() } + /** * Gets the name of this algorithm, e.g., "AES" or "SHA". */ @@ -294,7 +312,7 @@ module CryptographyBase Input> { abstract string getSHA2OrSHA3DigestSize(Location location); bindingset[type] - private string type_to_digest_size_fixed(THashType type) { + private string getTypeDigestSizeFixed(THashType type) { type instanceof MD2 and result = "128" or type instanceof MD4 and result = "128" @@ -309,21 +327,25 @@ module CryptographyBase Input> { } bindingset[type] - private string getDigestSize(THashType type, Location location) { - result = this.type_to_digest_size_fixed(type) and location = this.getLocation() + private string getTypeDigestSize(THashType type, Location location) { + result = this.getTypeDigestSizeFixed(type) and location = this.getLocation() or type instanceof SHA2 and result = this.getSHA2OrSHA3DigestSize(location) or type instanceof SHA3 and result = this.getSHA2OrSHA3DigestSize(location) } + string getDigestSize(Location location) { + result = this.getTypeDigestSize(this.getHashType(), location) + } + final override predicate properties(string key, string value, Location location) { super.properties(key, value, location) or // [KNOWN_OR_UNKNOWN] key = "digest_size" and - if exists(this.getDigestSize(this.getHashType(), location)) - then value = this.getDigestSize(this.getHashType(), location) + if exists(this.getDigestSize(location)) + then value = this.getDigestSize(location) else ( value instanceof UnknownPropertyValue and location instanceof UnknownLocation ) @@ -619,27 +641,33 @@ module CryptographyBase Input> { /** * An encryption operation that processes plaintext to generate a ciphertext. - * This operation takes an input message (plaintext) of arbitrary content and length and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). + * This operation takes an input message (plaintext) of arbitrary content and length + * and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). */ abstract class EncryptionOperation extends Operation, TEncryptionOperation { - abstract override Algorithm getAlgorithm(); - override string getOperationType() { result = "EncryptionOperation" } + + /** + * Gets the initialization vector associated with this encryption operation. + * + * This predicate does not need to hold for all encryption operations, + * as the initialization vector is not always required. + */ + abstract InitializationVector getInitializationVector(); } /** * Block cipher modes of operation algorithms */ newtype TModeOperationType = - ECB() or - CBC() or - CFB() or - OFB() or - CTR() or - GCM() or - CCM() or - XTS() or - OAEP() or + ECB() or // Not secure, widely used + CBC() or // Vulnerable to padding oracle attacks + GCM() or // Widely used AEAD mode (TLS 1.3, SSH, IPsec) + CTR() or // Fast stream-like encryption (SSH, disk encryption) + XTS() or // Standard for full-disk encryption (BitLocker, LUKS, FileVault) + CCM() or // Used in lightweight cryptography (IoT, WPA2) + SIV() or // Misuse-resistant encryption, used in secure storage + OCB() or // Efficient AEAD mode OtherMode() abstract class ModeOfOperationAlgorithm extends Algorithm, TModeOfOperationAlgorithm { @@ -655,22 +683,22 @@ module CryptographyBase Input> { abstract TModeOperationType getModeType(); bindingset[type] - final predicate modeToNameMapping(TModeOperationType type, string name) { + final private predicate modeToNameMapping(TModeOperationType type, string name) { type instanceof ECB and name = "ECB" or type instanceof CBC and name = "CBC" or - type instanceof CFB and name = "CFB" - or - type instanceof OFB and name = "OFB" + type instanceof GCM and name = "GCM" or type instanceof CTR and name = "CTR" or - type instanceof GCM and name = "GCM" + type instanceof XTS and name = "XTS" or type instanceof CCM and name = "CCM" or - type instanceof XTS and name = "XTS" + type instanceof SIV and name = "SIV" + or + type instanceof OCB and name = "OCB" or type instanceof OtherMode and name = this.getRawAlgorithmName() } @@ -678,12 +706,51 @@ module CryptographyBase Input> { override string getAlgorithmName() { this.modeToNameMapping(this.getModeType(), result) } } + newtype TPaddingType = + PKCS1_v1_5() or // RSA encryption/signing padding + PKCS7() or // Standard block cipher padding (PKCS5 for 8-byte blocks) + ANSI_X9_23() or // Zero-padding except last byte = padding length + NoPadding() or // Explicit no-padding + OAEP() or // RSA OAEP padding + OtherPadding() + + abstract class PaddingAlgorithm extends Algorithm, TPaddingAlgorithm { + override string getAlgorithmType() { result = "PaddingAlgorithm" } + + /** + * Gets the type of this padding algorithm, e.g., "PKCS7" or "OAEP". + * + * When modeling a new padding algorithm, use this predicate to specify the type of the padding. + * + * If a type cannot be determined, the result is `OtherPadding`. + */ + abstract TPaddingType getPaddingType(); + + bindingset[type] + final private predicate paddingToNameMapping(TPaddingType type, string name) { + type instanceof PKCS1_v1_5 and name = "PKCS1_v1_5" + or + type instanceof PKCS7 and name = "PKCS7" + or + type instanceof ANSI_X9_23 and name = "ANSI_X9_23" + or + type instanceof NoPadding and name = "NoPadding" + or + type instanceof OAEP and name = "OAEP" + or + type instanceof OtherPadding and name = this.getRawAlgorithmName() + } + + override string getAlgorithmName() { this.paddingToNameMapping(this.getPaddingType(), result) } + } + /** * A helper type for distinguishing between block and stream ciphers. */ newtype TCipherStructureType = Block() or Stream() or + Asymmetric() or UnknownCipherStructureType() private string getCipherStructureTypeString(TCipherStructureType type) { @@ -691,6 +758,8 @@ module CryptographyBase Input> { or type instanceof Stream and result = "Stream" or + type instanceof Asymmetric and result = "Asymmetric" + or type instanceof UnknownCipherStructureType and result instanceof UnknownPropertyValue } @@ -738,6 +807,11 @@ module CryptographyBase Input> { */ abstract ModeOfOperationAlgorithm getModeOfOperation(); + /** + * Gets the padding scheme of this cipher, e.g., "PKCS7" or "NoPadding". + */ + abstract PaddingAlgorithm getPadding(); + bindingset[type] final private predicate cipherFamilyToNameAndStructure( TCipherType type, string name, TCipherStructureType s @@ -760,7 +834,7 @@ module CryptographyBase Input> { or type instanceof RC5 and name = "RC5" and s = Block() or - type instanceof RSA and name = "RSA" and s = Block() + type instanceof RSA and name = "RSA" and s = Asymmetric() or type instanceof OtherSymmetricCipherType and name = this.getRawAlgorithmName() and From 8707e4d9a394aea6081fbcf52dffc0d29e0c6e8b Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Tue, 18 Feb 2025 18:35:49 +0100 Subject: [PATCH 20/28] Continue Artifact data-flow WIP --- java/ql/lib/experimental/Quantum/JCA.qll | 37 +++++---- java/ql/lib/experimental/Quantum/Language.qll | 76 ++++++++++++++++--- .../codeql/cryptography/Model.qll | 62 ++++++++++++--- 3 files changed, 141 insertions(+), 34 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 5a30e96b13ca..e961310334f9 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -244,24 +244,29 @@ module JCAModel { /** * Initialiation vectors */ - abstract class IVParameterInstantiation extends ClassInstanceExpr { - abstract Expr getIV(); + abstract class IVParameterInstantiation extends Crypto::InitializationVectorArtifactInstance instanceof ClassInstanceExpr + { + abstract Expr getInput(); } class IvParameterSpecInstance extends IVParameterInstantiation { IvParameterSpecInstance() { - this.getConstructedType().hasQualifiedName("javax.crypto.spec", "IvParameterSpec") + this.(ClassInstanceExpr) + .getConstructedType() + .hasQualifiedName("javax.crypto.spec", "IvParameterSpec") } - override Expr getIV() { result = super.getArgument(0) } + override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(0) } } class GCMParameterSpecInstance extends IVParameterInstantiation { GCMParameterSpecInstance() { - this.getConstructedType().hasQualifiedName("javax.crypto.spec", "GCMParameterSpec") + this.(ClassInstanceExpr) + .getConstructedType() + .hasQualifiedName("javax.crypto.spec", "GCMParameterSpec") } - override Expr getIV() { result = super.getArgument(1) } + override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(1) } } class CipherInitCall extends MethodCall { @@ -280,18 +285,24 @@ module JCAModel { } // TODO: cipher.getParameters().getParameterSpec(GCMParameterSpec.class); - class InitializationVectorExpr extends Crypto::InitializationVectorArtifactInstance instanceof Expr - { - CipherInitCall call; // TODO: add origin to known sources (e.g. RNG, etc.) - - InitializationVectorExpr() { this = call.getIV() } - } + /* + * class InitializationVectorArg extends Crypto::InitializationVectorArtifactInstance instanceof Expr + * { + * IVParameterInstantiation creation; + * + * InitializationVectorArg() { this = creation.getInput() } + * } + */ class InitializationVector extends Crypto::InitializationVector { - InitializationVectorExpr instance; + IVParameterInstantiation instance; InitializationVector() { this = Crypto::TInitializationVector(instance) } override Location getLocation() { result = instance.getLocation() } + + override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance } + + override Crypto::DataFlowNode getInputData() { result.asExpr() = instance.getInput() } } } diff --git a/java/ql/lib/experimental/Quantum/Language.qll b/java/ql/lib/experimental/Quantum/Language.qll index 485b3e716e69..5801815109b0 100644 --- a/java/ql/lib/experimental/Quantum/Language.qll +++ b/java/ql/lib/experimental/Quantum/Language.qll @@ -1,5 +1,11 @@ private import codeql.cryptography.Model -private import java as Lang +private import java as Language +private import semmle.code.java.security.InsecureRandomnessQuery +private import semmle.code.java.security.RandomQuery + +private class UnknownLocation extends Language::Location { + UnknownLocation() { this.getFile().getAbsolutePath() = "" } +} /** * A dummy location which is used when something doesn't have a location in @@ -7,24 +13,72 @@ private import java as Lang * may be several distinct kinds of unknown locations. For example: one for * expressions, one for statements and one for other program elements. */ -class UnknownLocation extends Location { - UnknownLocation() { this.getFile().getAbsolutePath() = "" } +private class UnknownDefaultLocation extends UnknownLocation { + UnknownDefaultLocation() { locations_default(this, _, 0, 0, 0, 0) } +} + +module CryptoInput implements InputSig { + class DataFlowNode = DataFlow::Node; + + class LocatableElement = Language::Element; + + class UnknownLocation = UnknownDefaultLocation; + + predicate rngToIvFlow(DataFlowNode rng, DataFlowNode iv) { none() } } /** - * A dummy location which is used when something doesn't have a location in - * the source code but needs to have a `Location` associated with it. + * Instantiate the model */ -class UnknownDefaultLocation extends UnknownLocation { - UnknownDefaultLocation() { locations_default(this, _, 0, 0, 0, 0) } +module Crypto = CryptographyBase; + +/** + * Random number generation, where each instance is modelled as the expression + * tied to an output node (i.e., the result of the source of randomness) + */ +abstract class RandomnessInstance extends Crypto::RandomNumberGenerationInstance { + abstract Crypto::RNGSourceSecurity getSourceSecurity(); + + Crypto::TRNGSeedSecurity getSeedSecurity(Location location) { none() } } -module CryptoInput implements InputSig { - class LocatableElement = Lang::Element; +class SecureRandomnessInstance extends RandomnessInstance { + SecureRandomnessInstance() { + exists(RandomDataSource s | this = s.getOutput() | + s.getSourceOfRandomness() instanceof SecureRandomNumberGenerator + ) + } - class UnknownLocation = UnknownDefaultLocation; + override Crypto::RNGSourceSecurity getSourceSecurity() { + result instanceof Crypto::RNGSourceSecure + } +} + +class InsecureRandomnessInstance extends RandomnessInstance { + InsecureRandomnessInstance() { exists(InsecureRandomnessSource node | this = node.asExpr()) } + + override Crypto::RNGSourceSecurity getSourceSecurity() { + result instanceof Crypto::RNGSourceInsecure + } } -module Crypto = CryptographyBase; +class RandomnessArtifact extends Crypto::RandomNumberGeneration { + RandomnessInstance instance; + + RandomnessArtifact() { this = Crypto::TRandomNumberGeneration(instance) } + + override Location getLocation() { result = instance.getLocation() } + + override Crypto::RNGSourceSecurity getSourceSecurity() { result = instance.getSourceSecurity() } + + override Crypto::TRNGSeedSecurity getSeedSecurity(Location location) { + result = instance.getSeedSecurity(location) + } + + override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance } + + override Crypto::DataFlowNode getInputData() { none() } +} +// Import library-specific modeling import JCA diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 9814f1519950..205400e8a3ca 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -12,7 +12,15 @@ signature module InputSig { string toString(); } + class DataFlowNode { + Location getLocation(); + + string toString(); + } + class UnknownLocation instanceof Location; + + predicate rngToIvFlow(DataFlowNode rng, DataFlowNode iv); } module CryptographyBase Input> { @@ -20,6 +28,8 @@ module CryptographyBase Input> { final class UnknownLocation = Input::UnknownLocation; + final class DataFlowNode = Input::DataFlowNode; + final class UnknownPropertyValue extends string { UnknownPropertyValue() { this = "" } } @@ -93,12 +103,15 @@ module CryptographyBase Input> { abstract class NonceArtifactInstance extends LocatableElement { } + abstract class RandomNumberGenerationInstance extends LocatableElement { } + newtype TNode = // Artifacts (data that is not an operation or algorithm, e.g., a key) TDigest(DigestArtifactInstance e) or TKey(KeyArtifactInstance e) or TInitializationVector(InitializationVectorArtifactInstance e) or TNonce(NonceArtifactInstance e) or + TRandomNumberGeneration(RandomNumberGenerationInstance e) or // Operations (e.g., hashing, encryption) THashOperation(HashOperationInstance e) or TKeyDerivationOperation(KeyDerivationOperationInstance e) or @@ -115,7 +128,7 @@ module CryptographyBase Input> { TPaddingAlgorithm(PaddingAlgorithmInstance e) or // Composite and hybrid cryptosystems (e.g., RSA-OAEP used with AES, post-quantum hybrid cryptosystems) // These nodes are always parent nodes and are not modeled but rather defined via library-agnostic patterns. - TKemDemHybridCryptosystem(EncryptionAlgorithmInstance dem) or // TODO, change this relation and the below ones + TKemDemHybridCryptosystem(EncryptionAlgorithm dem) or // TODO, change this relation and the below ones TKeyAgreementHybridCryptosystem(EncryptionAlgorithmInstance ka) or TAsymmetricEncryptionMacHybridCryptosystem(EncryptionAlgorithmInstance enc) or TPostQuantumHybridCryptosystem(EncryptionAlgorithmInstance enc) @@ -127,9 +140,9 @@ module CryptographyBase Input> { */ abstract class NodeBase extends TNode { /** - * Returns a string representation of this node, usually the name of the operation/algorithm/property. + * Returns a string representation of this node. */ - abstract string toString(); + string toString() { result = this.getInternalType() } /** * Returns a string representation of the internal type of this node, usually the name of the class. @@ -172,15 +185,48 @@ module CryptographyBase Input> { class Asset = NodeBase; - class Artifact = NodeBase; + abstract class Artifact extends NodeBase { + abstract DataFlowNode asOutputData(); + + abstract DataFlowNode getInputData(); + } /** * An initialization vector */ - abstract class InitializationVector extends Asset, TInitializationVector { + abstract class InitializationVector extends Artifact, TInitializationVector { final override string getInternalType() { result = "InitializationVector" } - final override string toString() { result = this.getInternalType() } + RandomNumberGeneration getRNGSource() { + Input::rngToIvFlow(result.asOutputData(), this.getInputData()) + } + } + + newtype TRNGSourceSecurity = + RNGSourceSecure() or // Secure RNG source (unrelated to seed) + RNGSourceInsecure() // Insecure RNG source (unrelated to seed) + + class RNGSourceSecurity extends TRNGSourceSecurity { + string toString() { + this instanceof RNGSourceSecure and result = "Secure RNG Source" + or + this instanceof RNGSourceInsecure and result = "Insecure RNG Source" + } + } + + newtype TRNGSeedSecurity = + RNGSeedSecure() or + RNGSeedInsecure() + + /** + * A source of random number generation + */ + abstract class RandomNumberGeneration extends Artifact, TRandomNumberGeneration { + final override string getInternalType() { result = "RandomNumberGeneration" } + + abstract RNGSourceSecurity getSourceSecurity(); + + abstract TRNGSeedSecurity getSeedSecurity(Location location); } /** @@ -197,8 +243,6 @@ module CryptographyBase Input> { */ abstract string getOperationType(); - final override string toString() { result = this.getOperationType() } - final override string getInternalType() { result = this.getOperationType() } override NodeBase getChild(string edgeName) { @@ -210,8 +254,6 @@ module CryptographyBase Input> { } abstract class Algorithm extends Asset { - final override string toString() { result = this.getAlgorithmType() } - final override string getInternalType() { result = this.getAlgorithmType() } /** From 3871c6a33ed3e3c0399de39b389e6cb7712eea64 Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Tue, 18 Feb 2025 16:09:00 -0500 Subject: [PATCH 21/28] Adding support for encryption operation detection. --- java/ql/lib/experimental/Quantum/JCA.qll | 57 +++++++++++++++++++ .../codeql/cryptography/Model.qll | 15 ++--- 2 files changed, 65 insertions(+), 7 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index e961310334f9..5b55090bd9e2 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -58,6 +58,10 @@ module JCAModel { Expr getProviderArg() { result = this.getArgument(1) } } + class CipherDoFinalCall extends Call { + CipherDoFinalCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "doFinal") } + } + /** * Data-flow configuration modelling flow from a cipher string literal to a `CipherGetInstanceCall` argument. */ @@ -92,6 +96,57 @@ module JCAModel { } } + // TODO: what if encrypt/decrypt mode isn't known + private module CipherGetInstanceToFinalizeConfig implements DataFlow::StateConfigSig { + class FlowState = string; + + predicate isSource(DataFlow::Node src, FlowState state) { + state = "UNKNOWN" and + src.asExpr() instanceof CipherGetInstanceCall + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + state in ["ENCRYPT", "DECRYPT", "UNKNOWN"] and + exists(CipherDoFinalCall c | c.getQualifier() = sink.asExpr()) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + state1 in ["UNKNOWN", "ENCRYPT", "DECRYPT"] and + exists(CipherInitCall c | + c.getQualifier() = node1.asExpr() and + // TODO: not taking into consideration if the mode traces to this arg + exists(FieldAccess fa | + c.getModeArg() = fa and + ( + fa.getField().getName() = "ENCRYPT_MODE" and + state2 = "ENCRYPT" + or + fa.getField().getName() = "DECRYPT_MODE" and + state2 = "DECRYPT" + ) + ) + ) and + node2 = node1 + } + } + + module CipherGetInstanceToFinalizeFlow = + DataFlow::GlobalWithState; + + // TODO: what if the mode is UNKNOWN? + class CipherEncryptionOperation extends Crypto::EncryptionOperationInstance instanceof Call { + CipherEncryptionOperation() { + exists(CipherGetInstanceToFinalizeFlow::PathNode sink, CipherDoFinalCall c | + CipherGetInstanceToFinalizeFlow::flowPath(_, sink) and + sink.getNode().asExpr() = c.getQualifier() and + sink.getState() = "ENCRYPT" and + this = c + ) + } + } + /** * A block cipher mode of operation, where the mode is specified in the ALG or ALG/MODE/PADDING format. * @@ -272,6 +327,8 @@ module JCAModel { class CipherInitCall extends MethodCall { CipherInitCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "init") } + // TODO: this doesn't account for tracing the mode to this arg if expending this arg to have + // the actual mode directly Expr getModeArg() { result = this.getArgument(0) } Expr getKey() { diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 205400e8a3ca..8a5011489a67 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -689,13 +689,14 @@ module CryptographyBase Input> { abstract class EncryptionOperation extends Operation, TEncryptionOperation { override string getOperationType() { result = "EncryptionOperation" } - /** - * Gets the initialization vector associated with this encryption operation. - * - * This predicate does not need to hold for all encryption operations, - * as the initialization vector is not always required. - */ - abstract InitializationVector getInitializationVector(); + abstract override EncryptionAlgorithm getAlgorithm(); + // /** + // * Gets the initialization vector associated with this encryption operation. + // * + // * This predicate does not need to hold for all encryption operations, + // * as the initialization vector is not always required. + // */ + // abstract InitializationVector getInitializationVector(); } /** From 9ee4a7a7b8798efb33b18271527e5dd167d9bc94 Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Thu, 20 Feb 2025 10:37:40 -0500 Subject: [PATCH 22/28] Adding a sketch for a CipherOperation concept to model encryption/decryption operations. --- java/ql/lib/experimental/Quantum/JCA.qll | 51 +++++++++++++------ .../codeql/cryptography/Model.qll | 51 +++++++++++++------ 2 files changed, 70 insertions(+), 32 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 5b55090bd9e2..0f505e400a06 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -83,9 +83,9 @@ module JCAModel { class CipherGetInstanceAlgorithmArg extends Crypto::EncryptionAlgorithmInstance, Crypto::ModeOfOperationAlgorithmInstance, Crypto::PaddingAlgorithmInstance instanceof Expr { - CipherGetInstanceAlgorithmArg() { - exists(CipherGetInstanceCall call | this = call.getArgument(0)) - } + CipherGetInstanceCall call; + + CipherGetInstanceAlgorithmArg() { this = call.getAlgorithmArg() } /** * Returns the `StringLiteral` from which this argument is derived, if known. @@ -94,26 +94,26 @@ module JCAModel { AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(result), DataFlow::exprNode(this.(Expr).getAChildExpr*())) } + + CipherGetInstanceCall getCall() { result = call } } // TODO: what if encrypt/decrypt mode isn't known private module CipherGetInstanceToFinalizeConfig implements DataFlow::StateConfigSig { - class FlowState = string; + class FlowState = Crypto::TCipherOperationMode; predicate isSource(DataFlow::Node src, FlowState state) { - state = "UNKNOWN" and + state = Crypto::UnknownCipherOperationMode() and src.asExpr() instanceof CipherGetInstanceCall } predicate isSink(DataFlow::Node sink, FlowState state) { - state in ["ENCRYPT", "DECRYPT", "UNKNOWN"] and exists(CipherDoFinalCall c | c.getQualifier() = sink.asExpr()) } predicate isAdditionalFlowStep( DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 ) { - state1 in ["UNKNOWN", "ENCRYPT", "DECRYPT"] and exists(CipherInitCall c | c.getQualifier() = node1.asExpr() and // TODO: not taking into consideration if the mode traces to this arg @@ -121,10 +121,16 @@ module JCAModel { c.getModeArg() = fa and ( fa.getField().getName() = "ENCRYPT_MODE" and - state2 = "ENCRYPT" + state2 = Crypto::EncryptionMode() or fa.getField().getName() = "DECRYPT_MODE" and - state2 = "DECRYPT" + state2 = Crypto::DecryptionMode() + or + fa.getField().getName() = "WRAP_MODE" and + state2 = Crypto::EncryptionMode() + or + fa.getField().getName() = "UNWRAP_MODE" and + state2 = Crypto::DecryptionMode() ) ) ) and @@ -135,16 +141,29 @@ module JCAModel { module CipherGetInstanceToFinalizeFlow = DataFlow::GlobalWithState; - // TODO: what if the mode is UNKNOWN? - class CipherEncryptionOperation extends Crypto::EncryptionOperationInstance instanceof Call { + class CipherEncryptionOperation extends Crypto::CipherOperationInstance instanceof Call { + Crypto::TCipherOperationMode mode; + Crypto::EncryptionAlgorithmInstance algorithm; + CipherEncryptionOperation() { - exists(CipherGetInstanceToFinalizeFlow::PathNode sink, CipherDoFinalCall c | - CipherGetInstanceToFinalizeFlow::flowPath(_, sink) and - sink.getNode().asExpr() = c.getQualifier() and - sink.getState() = "ENCRYPT" and - this = c + exists( + CipherGetInstanceToFinalizeFlow::PathNode sink, + CipherGetInstanceToFinalizeFlow::PathNode src, CipherGetInstanceCall getCipher, + CipherDoFinalCall doFinalize, CipherGetInstanceAlgorithmArg arg + | + CipherGetInstanceToFinalizeFlow::flowPath(src, sink) and + src.getNode().asExpr() = getCipher and + sink.getNode().asExpr() = doFinalize.getQualifier() and + sink.getState() = mode and + this = doFinalize and + arg.getCall() = getCipher and + algorithm = arg ) } + + override Crypto::EncryptionAlgorithmInstance getAlgorithm() { result = algorithm } + + override Crypto::TCipherOperationMode getCipherOperationMode() { result = mode } } /** diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 8a5011489a67..24e3d4f48ebd 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -79,7 +79,11 @@ module CryptographyBase Input> { abstract class KeyDerivationAlgorithmInstance extends LocatableElement { } - abstract class EncryptionOperationInstance extends LocatableElement { } + abstract class CipherOperationInstance extends LocatableElement { + abstract EncryptionAlgorithmInstance getAlgorithm(); + + abstract TCipherOperationMode getCipherOperationMode(); + } abstract class EncryptionAlgorithmInstance extends LocatableElement { } @@ -115,7 +119,7 @@ module CryptographyBase Input> { // Operations (e.g., hashing, encryption) THashOperation(HashOperationInstance e) or TKeyDerivationOperation(KeyDerivationOperationInstance e) or - TEncryptionOperation(EncryptionOperationInstance e) or + TCipherOperation(CipherOperationInstance e) or TKeyEncapsulationOperation(KeyEncapsulationOperationInstance e) or // Algorithms (e.g., SHA-256, AES) TEncryptionAlgorithm(EncryptionAlgorithmInstance e) or @@ -238,13 +242,14 @@ module CryptographyBase Input> { */ abstract Algorithm getAlgorithm(); - /** - * Gets the name of this operation, e.g., "hash" or "encrypt". - */ - abstract string getOperationType(); - - final override string getInternalType() { result = this.getOperationType() } - + // TODO: I only removed this because I want the operation type to be non-string + // since for CipherOperations the user will have to pick the right type, + // and I want to force them to use a type that is restricted. In this case to a TCipherOperationType + // /** + // * Gets the name of this operation, e.g., "hash" or "encrypt". + // */ + // abstract string getOperationType(); + // final override string getInternalType() { result = this.getOperationType() } override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or @@ -290,8 +295,7 @@ module CryptographyBase Input> { */ abstract class HashOperation extends Operation, THashOperation { abstract override HashAlgorithm getAlgorithm(); - - override string getOperationType() { result = "HashOperation" } + //override string getOperationType() { result = "HashOperation" } } newtype THashType = @@ -401,8 +405,7 @@ module CryptographyBase Input> { final override Location getLocation() { exists(LocatableElement le | this = TKeyDerivationOperation(le) and result = le.getLocation()) } - - override string getOperationType() { result = "KeyDerivationOperation" } + //override string getOperationType() { result = "KeyDerivationOperation" } } /** @@ -681,15 +684,31 @@ module CryptographyBase Input> { abstract override string getRawAlgorithmName(); } + newtype TCipherOperationMode = + EncryptionMode() or + DecryptionMode() or + UnknownCipherOperationMode() + /** * An encryption operation that processes plaintext to generate a ciphertext. * This operation takes an input message (plaintext) of arbitrary content and length * and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). */ - abstract class EncryptionOperation extends Operation, TEncryptionOperation { - override string getOperationType() { result = "EncryptionOperation" } + // NOTE FOR NICK: making this concrete here as I don't think users need to worry about making/extending these operations, just instances + class CipherOperation extends Operation, TCipherOperation { + CipherOperationInstance instance; + + CipherOperation() { this = TCipherOperation(instance) } + + override Location getLocation() { result = instance.getLocation() } + + final TCipherOperationMode getCipherOperationMode() { + result = instance.getCipherOperationMode() + } + + final override EncryptionAlgorithm getAlgorithm() { result = instance.getAlgorithm() } - abstract override EncryptionAlgorithm getAlgorithm(); + override string getInternalType() { result = "CipherOperation" } // /** // * Gets the initialization vector associated with this encryption operation. // * From 83dc5b99065f8d4482899bb05d8736e8d6e0d13d Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Thu, 20 Feb 2025 10:45:33 -0500 Subject: [PATCH 23/28] Fixing type bug --- shared/cryptography/codeql/cryptography/Model.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 24e3d4f48ebd..17834343e6d5 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -706,7 +706,7 @@ module CryptographyBase Input> { result = instance.getCipherOperationMode() } - final override EncryptionAlgorithm getAlgorithm() { result = instance.getAlgorithm() } + final override EncryptionAlgorithm getAlgorithm() { result.getInstance() = instance.getAlgorithm() } override string getInternalType() { result = "CipherOperation" } // /** From 011ed3fbfd11a6cd7ab5b8aa13c3945881a37faf Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Thu, 20 Feb 2025 11:10:24 -0500 Subject: [PATCH 24/28] Simplifying additional flow step logic. --- java/ql/lib/experimental/Quantum/JCA.qll | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 0f505e400a06..0a7903aa2722 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -120,17 +120,13 @@ module JCAModel { exists(FieldAccess fa | c.getModeArg() = fa and ( - fa.getField().getName() = "ENCRYPT_MODE" and - state2 = Crypto::EncryptionMode() - or - fa.getField().getName() = "DECRYPT_MODE" and - state2 = Crypto::DecryptionMode() - or - fa.getField().getName() = "WRAP_MODE" and - state2 = Crypto::EncryptionMode() - or - fa.getField().getName() = "UNWRAP_MODE" and - state2 = Crypto::DecryptionMode() + if fa.getField().getName() in ["ENCRYPT_MODE", "WRAP_MODE"] + then state2 = Crypto::EncryptionMode() + else ( + if fa.getField().getName() in ["DECRYPT_MODE", "UNWRAP_MODE"] + then state2 = Crypto::DecryptionMode() + else state2 = Crypto::UnknownCipherOperationMode() + ) ) ) ) and From 9ac9252f7548d1c6f59cd2b4f159ebe57db60aa8 Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Thu, 20 Feb 2025 11:11:41 -0500 Subject: [PATCH 25/28] Adding a todo --- java/ql/lib/experimental/Quantum/JCA.qll | 2 ++ 1 file changed, 2 insertions(+) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 0a7903aa2722..3c37d1d717e1 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -346,6 +346,8 @@ module JCAModel { // the actual mode directly Expr getModeArg() { result = this.getArgument(0) } + // TODO: need a getModeOrigin + Expr getKey() { result = this.getArgument(1) and this.getMethod().getParameterType(1).hasName("Key") } From 86cab46b8d7bd15213ce40d57cc1fa86b01d0e43 Mon Sep 17 00:00:00 2001 From: "REDMOND\\brodes" Date: Fri, 21 Feb 2025 12:53:35 -0500 Subject: [PATCH 26/28] Misc. updates to support all JCA cipher operations, including wrap, unwrap and doFinal calls. Corrected pathing for init tracing to detect what mode is being set along a path. Added support for tracing the init operation mode argument to source. Since this involved creating an Operation Mode, changes were also made to make cipher block modes (CBC) more explicit (previously just called mode, but now that term is used for various purposes). --- java/ql/lib/experimental/Quantum/JCA.qll | 193 ++++++++++++++---- .../codeql/cryptography/Model.qll | 41 +++- 2 files changed, 181 insertions(+), 53 deletions(-) diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 3c37d1d717e1..acbe6c67888f 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -58,8 +58,12 @@ module JCAModel { Expr getProviderArg() { result = this.getArgument(1) } } - class CipherDoFinalCall extends Call { - CipherDoFinalCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "doFinal") } + private class JCACipherOperationCall extends Call { + JCACipherOperationCall() { + exists(string s | s in ["doFinal", "wrap", "unwrap"] | + this.getCallee().hasQualifiedName("javax.crypto", "Cipher", s) + ) + } } /** @@ -81,7 +85,7 @@ module JCAModel { * For example, in `Cipher.getInstance(algorithm)`, this class represents `algorithm`. */ class CipherGetInstanceAlgorithmArg extends Crypto::EncryptionAlgorithmInstance, - Crypto::ModeOfOperationAlgorithmInstance, Crypto::PaddingAlgorithmInstance instanceof Expr + Crypto::BlockCipherModeOfOperationAlgorithmInstance, Crypto::PaddingAlgorithmInstance instanceof Expr { CipherGetInstanceCall call; @@ -98,68 +102,136 @@ module JCAModel { CipherGetInstanceCall getCall() { result = call } } - // TODO: what if encrypt/decrypt mode isn't known - private module CipherGetInstanceToFinalizeConfig implements DataFlow::StateConfigSig { - class FlowState = Crypto::TCipherOperationMode; + /** + * An access to the `javax.crypto.Cipher` class. + */ + private class CipherAccess extends TypeAccess { + CipherAccess() { this.getType().(Class).hasQualifiedName("javax.crypto", "Cipher") } + } + + /** + * An access to a cipher mode field of the `javax.crypto.Cipher` class, + * specifically `ENCRYPT_MODE`, `DECRYPT_MODE`, `WRAP_MODE`, or `UNWRAP_MODE`. + */ + private class JavaxCryptoCipherOperationModeAccess extends FieldAccess { + JavaxCryptoCipherOperationModeAccess() { + this.getQualifier() instanceof CipherAccess and + this.getField().getName() in ["ENCRYPT_MODE", "DECRYPT_MODE", "WRAP_MODE", "UNWRAP_MODE"] + } + } + + private newtype TCipherModeFlowState = + TUninitializedCipherModeFlowState() or + TInitializedCipherModeFlowState(CipherInitCall call) + + abstract private class CipherModeFlowState extends TCipherModeFlowState { + string toString() { + this = TUninitializedCipherModeFlowState() and result = "uninitialized" + or + this = TInitializedCipherModeFlowState(_) and result = "initialized" + } + + abstract Crypto::CipherOperationMode getCipherOperationMode(); + } + + private class UninitializedCipherModeFlowState extends CipherModeFlowState, + TUninitializedCipherModeFlowState + { + override Crypto::CipherOperationMode getCipherOperationMode() { + result instanceof Crypto::UnknownCipherOperationMode + } + } + + private class InitializedCipherModeFlowState extends CipherModeFlowState, + TInitializedCipherModeFlowState + { + CipherInitCall call; + DataFlow::Node node1; + DataFlow::Node node2; + Crypto::CipherOperationMode mode; + + InitializedCipherModeFlowState() { + this = TInitializedCipherModeFlowState(call) and + DataFlow::localFlowStep(node1, node2) and + node2.asExpr() = call.getQualifier() and + // I would imagine this would make this predicate horribly horribly inefficient + // it now binds with anything + not node1.asExpr() = call.getQualifier() and + mode = call.getCipherOperationModeType() + } + + CipherInitCall getCall() { result = call } + + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } + + override Crypto::CipherOperationMode getCipherOperationMode() { result = mode } + } + + /** + * Trace to a cryptographic operation, + * specifically `Cipher.doFinal()`, `Cipher.wrap()`, or `Cipher.unwrap()`. + */ + private module CipherGetInstanceToCipherOperationConfig implements DataFlow::StateConfigSig { + class FlowState = TCipherModeFlowState; predicate isSource(DataFlow::Node src, FlowState state) { - state = Crypto::UnknownCipherOperationMode() and + state instanceof UninitializedCipherModeFlowState and src.asExpr() instanceof CipherGetInstanceCall } - predicate isSink(DataFlow::Node sink, FlowState state) { - exists(CipherDoFinalCall c | c.getQualifier() = sink.asExpr()) + predicate isSink(DataFlow::Node sink, FlowState state) { none() } + + predicate isSink(DataFlow::Node sink) { + exists(JCACipherOperationCall c | c.getQualifier() = sink.asExpr()) } predicate isAdditionalFlowStep( DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 ) { - exists(CipherInitCall c | - c.getQualifier() = node1.asExpr() and - // TODO: not taking into consideration if the mode traces to this arg - exists(FieldAccess fa | - c.getModeArg() = fa and - ( - if fa.getField().getName() in ["ENCRYPT_MODE", "WRAP_MODE"] - then state2 = Crypto::EncryptionMode() - else ( - if fa.getField().getName() in ["DECRYPT_MODE", "UNWRAP_MODE"] - then state2 = Crypto::DecryptionMode() - else state2 = Crypto::UnknownCipherOperationMode() - ) - ) - ) - ) and - node2 = node1 + node1 = state2.(InitializedCipherModeFlowState).getFstNode() and + node2 = state2.(InitializedCipherModeFlowState).getSndNode() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { + exists(CipherInitCall call | node.asExpr() = call.getQualifier() | + state instanceof UninitializedCipherModeFlowState + or + state.(InitializedCipherModeFlowState).getCall() != call + ) } } - module CipherGetInstanceToFinalizeFlow = - DataFlow::GlobalWithState; + module CipherGetInstanceToCipherOperationFlow = + DataFlow::GlobalWithState; class CipherEncryptionOperation extends Crypto::CipherOperationInstance instanceof Call { - Crypto::TCipherOperationMode mode; + Crypto::CipherOperationMode mode; Crypto::EncryptionAlgorithmInstance algorithm; CipherEncryptionOperation() { exists( - CipherGetInstanceToFinalizeFlow::PathNode sink, - CipherGetInstanceToFinalizeFlow::PathNode src, CipherGetInstanceCall getCipher, - CipherDoFinalCall doFinalize, CipherGetInstanceAlgorithmArg arg + CipherGetInstanceToCipherOperationFlow::PathNode sink, + CipherGetInstanceToCipherOperationFlow::PathNode src, CipherGetInstanceCall getCipher, + JCACipherOperationCall doFinalize, CipherGetInstanceAlgorithmArg arg | - CipherGetInstanceToFinalizeFlow::flowPath(src, sink) and + CipherGetInstanceToCipherOperationFlow::flowPath(src, sink) and src.getNode().asExpr() = getCipher and sink.getNode().asExpr() = doFinalize.getQualifier() and - sink.getState() = mode and + sink.getState().(CipherModeFlowState).getCipherOperationMode() = mode and this = doFinalize and - arg.getCall() = getCipher and + arg.getCall() = getCipher and algorithm = arg ) } override Crypto::EncryptionAlgorithmInstance getAlgorithm() { result = algorithm } - override Crypto::TCipherOperationMode getCipherOperationMode() { result = mode } + override Crypto::CipherOperationMode getCipherOperationMode() { result = mode } } /** @@ -177,7 +249,7 @@ module JCAModel { CipherGetInstanceAlgorithmArg instance; ModeOfOperation() { - this = Crypto::TModeOfOperationAlgorithm(instance) and + this = Crypto::TBlockCipherModeOfOperationAlgorithm(instance) and // TODO: this currently only holds for explicitly defined modes in a string literal. // Cases with defaults, e.g., "AES", are not yet modelled. // For these cases, in a CBOM, the AES node would have an unknown edge to its mode child. @@ -190,7 +262,7 @@ module JCAModel { // TODO: handle defaults override string getRawAlgorithmName() { result = instance.getOrigin().getMode() } - private predicate modeToNameMappingKnown(Crypto::TModeOperationType type, string name) { + private predicate modeToNameMappingKnown(Crypto::TBlockCipherModeOperationType type, string name) { type instanceof Crypto::ECB and name = "ECB" or type instanceof Crypto::CBC and name = "CBC" @@ -208,7 +280,7 @@ module JCAModel { type instanceof Crypto::OCB and name = "OCB" } - override Crypto::TModeOperationType getModeType() { + override Crypto::TBlockCipherModeOperationType getModeType() { if this.modeToNameMappingKnown(_, instance.getOrigin().getMode()) then this.modeToNameMappingKnown(result, instance.getOrigin().getMode()) else result instanceof Crypto::OtherMode @@ -339,14 +411,51 @@ module JCAModel { override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(1) } } + private module JavaxCipherModeAccessToInitConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node src) { + src.asExpr() instanceof JavaxCryptoCipherOperationModeAccess + } + + predicate isSink(DataFlow::Node sink) { + exists(CipherInitCall c | c.getModeArg() = sink.asExpr()) + } + } + + module JavaxCipherModeAccessToInitFlow = DataFlow::Global; + class CipherInitCall extends MethodCall { CipherInitCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "init") } - // TODO: this doesn't account for tracing the mode to this arg if expending this arg to have - // the actual mode directly + /** + * Returns the mode argument to the `init` method + * that is used to determine the cipher operation mode. + * Note this is the raw expr and not necessarily a direct access + * of a mode. Use `getModeOrigin()` to get the field access origin + * flowing to this argument, if one exists (is known). + */ Expr getModeArg() { result = this.getArgument(0) } - // TODO: need a getModeOrigin + JavaxCryptoCipherOperationModeAccess getModeOrigin() { + exists(DataFlow::Node src, DataFlow::Node sink | + JavaxCipherModeAccessToInitFlow::flow(src, sink) and + src.asExpr() = result and + this.getModeArg() = sink.asExpr() + ) + } + + Crypto::CipherOperationMode getCipherOperationModeType() { + if not exists(this.getModeOrigin()) + then result instanceof Crypto::UnknownCipherOperationMode + else + if this.getModeOrigin().getField().getName() in ["ENCRYPT_MODE", "WRAP_MODE"] + then result instanceof Crypto::EncryptionMode + else + if this.getModeOrigin().getField().getName() in ["DECRYPT_MODE", "UNWRAP_MODE"] + then result instanceof Crypto::DecryptionMode + else + // TODO/Question: distinguish between unknown vs unspecified? (the field access is not recognized, vs no field access is found) + result instanceof Crypto::UnknownCipherOperationMode + } Expr getKey() { result = this.getArgument(1) and this.getMethod().getParameterType(1).hasName("Key") diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index 17834343e6d5..a0f22d0229b6 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -82,7 +82,7 @@ module CryptographyBase Input> { abstract class CipherOperationInstance extends LocatableElement { abstract EncryptionAlgorithmInstance getAlgorithm(); - abstract TCipherOperationMode getCipherOperationMode(); + abstract CipherOperationMode getCipherOperationMode(); } abstract class EncryptionAlgorithmInstance extends LocatableElement { } @@ -94,7 +94,7 @@ module CryptographyBase Input> { abstract class EllipticCurveAlgorithmInstance extends LocatableElement { } // Non-standalone algorithms - abstract class ModeOfOperationAlgorithmInstance extends LocatableElement { } + abstract class BlockCipherModeOfOperationAlgorithmInstance extends LocatableElement { } abstract class PaddingAlgorithmInstance extends LocatableElement { } @@ -128,7 +128,8 @@ module CryptographyBase Input> { TKeyDerivationAlgorithm(KeyDerivationAlgorithmInstance e) or TKeyEncapsulationAlgorithm(KeyEncapsulationAlgorithmInstance e) or // Non-standalone Algorithms (e.g., Mode, Padding) - TModeOfOperationAlgorithm(ModeOfOperationAlgorithmInstance e) or + // TODO: need to rename this, as "mode" is getting reused in different contexts, be precise + TBlockCipherModeOfOperationAlgorithm(BlockCipherModeOfOperationAlgorithmInstance e) or TPaddingAlgorithm(PaddingAlgorithmInstance e) or // Composite and hybrid cryptosystems (e.g., RSA-OAEP used with AES, post-quantum hybrid cryptosystems) // These nodes are always parent nodes and are not modeled but rather defined via library-agnostic patterns. @@ -685,9 +686,25 @@ module CryptographyBase Input> { } newtype TCipherOperationMode = - EncryptionMode() or - DecryptionMode() or - UnknownCipherOperationMode() + TEncryptionMode() or + TDecryptionMode() or + TUnknownCipherOperationMode() + + abstract class CipherOperationMode extends TCipherOperationMode { + abstract string toString(); + } + + class EncryptionMode extends CipherOperationMode, TEncryptionMode { + override string toString() { result = "Encryption" } + } + + class DecryptionMode extends CipherOperationMode, TDecryptionMode { + override string toString() { result = "Decryption" } + } + + class UnknownCipherOperationMode extends CipherOperationMode, TUnknownCipherOperationMode { + override string toString() { result = "Unknown" } + } /** * An encryption operation that processes plaintext to generate a ciphertext. @@ -706,7 +723,9 @@ module CryptographyBase Input> { result = instance.getCipherOperationMode() } - final override EncryptionAlgorithm getAlgorithm() { result.getInstance() = instance.getAlgorithm() } + final override EncryptionAlgorithm getAlgorithm() { + result.getInstance() = instance.getAlgorithm() + } override string getInternalType() { result = "CipherOperation" } // /** @@ -721,7 +740,7 @@ module CryptographyBase Input> { /** * Block cipher modes of operation algorithms */ - newtype TModeOperationType = + newtype TBlockCipherModeOperationType = ECB() or // Not secure, widely used CBC() or // Vulnerable to padding oracle attacks GCM() or // Widely used AEAD mode (TLS 1.3, SSH, IPsec) @@ -732,7 +751,7 @@ module CryptographyBase Input> { OCB() or // Efficient AEAD mode OtherMode() - abstract class ModeOfOperationAlgorithm extends Algorithm, TModeOfOperationAlgorithm { + abstract class ModeOfOperationAlgorithm extends Algorithm, TBlockCipherModeOfOperationAlgorithm { override string getAlgorithmType() { result = "ModeOfOperation" } /** @@ -742,10 +761,10 @@ module CryptographyBase Input> { * * If a type cannot be determined, the result is `OtherMode`. */ - abstract TModeOperationType getModeType(); + abstract TBlockCipherModeOperationType getModeType(); bindingset[type] - final private predicate modeToNameMapping(TModeOperationType type, string name) { + final private predicate modeToNameMapping(TBlockCipherModeOperationType type, string name) { type instanceof ECB and name = "ECB" or type instanceof CBC and name = "CBC" From 2b0b927b0b14ad819f2e07588d2b75042cbd2545 Mon Sep 17 00:00:00 2001 From: Nicolas Will Date: Mon, 24 Feb 2025 17:37:41 +0100 Subject: [PATCH 27/28] Add Nonce association to Operation, update graph --- java/ql/lib/experimental/Quantum/JCA.qll | 176 ++++++++----- java/ql/lib/experimental/Quantum/Language.qll | 32 +-- .../src/experimental/Quantum/ReusedNonce.ql | 23 ++ java/ql/src/experimental/Quantum/Test.ql | 9 - .../ql/src/experimental/Quantum/TestCipher.ql | 16 ++ misc/scripts/cryptography/cbom.sh | 6 +- misc/scripts/cryptography/generate_cbom.py | 10 +- .../codeql/cryptography/Model.qll | 233 ++++++++++-------- 8 files changed, 297 insertions(+), 208 deletions(-) create mode 100644 java/ql/src/experimental/Quantum/ReusedNonce.ql delete mode 100644 java/ql/src/experimental/Quantum/Test.ql create mode 100644 java/ql/src/experimental/Quantum/TestCipher.ql diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index acbe6c67888f..9892b445312a 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -1,5 +1,6 @@ import java import semmle.code.java.dataflow.DataFlow +import semmle.code.java.controlflow.Dominance module JCAModel { import Language @@ -64,6 +65,8 @@ module JCAModel { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", s) ) } + + DataFlow::Node getInputData() { result.asExpr() = this.getArgument(0) } } /** @@ -84,7 +87,7 @@ module JCAModel { * * For example, in `Cipher.getInstance(algorithm)`, this class represents `algorithm`. */ - class CipherGetInstanceAlgorithmArg extends Crypto::EncryptionAlgorithmInstance, + class CipherGetInstanceAlgorithmArg extends Crypto::CipherAlgorithmInstance, Crypto::BlockCipherModeOfOperationAlgorithmInstance, Crypto::PaddingAlgorithmInstance instanceof Expr { CipherGetInstanceCall call; @@ -116,13 +119,22 @@ module JCAModel { private class JavaxCryptoCipherOperationModeAccess extends FieldAccess { JavaxCryptoCipherOperationModeAccess() { this.getQualifier() instanceof CipherAccess and - this.getField().getName() in ["ENCRYPT_MODE", "DECRYPT_MODE", "WRAP_MODE", "UNWRAP_MODE"] + this.getField().getName().toUpperCase() in [ + "ENCRYPT_MODE", "DECRYPT_MODE", "WRAP_MODE", "UNWRAP_MODE" + ] } } + class CipherUpdateCall extends MethodCall { + CipherUpdateCall() { this.getMethod().hasQualifiedName("javax.crypto", "Cipher", "update") } + + DataFlow::Node getInputData() { result.asExpr() = this.getArgument(0) } + } + private newtype TCipherModeFlowState = TUninitializedCipherModeFlowState() or - TInitializedCipherModeFlowState(CipherInitCall call) + TInitializedCipherModeFlowState(CipherInitCall call) or + TUsedCipherModeFlowState(CipherInitCall init, CipherUpdateCall update) abstract private class CipherModeFlowState extends TCipherModeFlowState { string toString() { @@ -131,13 +143,13 @@ module JCAModel { this = TInitializedCipherModeFlowState(_) and result = "initialized" } - abstract Crypto::CipherOperationMode getCipherOperationMode(); + abstract Crypto::CipherOperationSubtype getCipherOperationMode(); } private class UninitializedCipherModeFlowState extends CipherModeFlowState, TUninitializedCipherModeFlowState { - override Crypto::CipherOperationMode getCipherOperationMode() { + override Crypto::CipherOperationSubtype getCipherOperationMode() { result instanceof Crypto::UnknownCipherOperationMode } } @@ -148,19 +160,18 @@ module JCAModel { CipherInitCall call; DataFlow::Node node1; DataFlow::Node node2; - Crypto::CipherOperationMode mode; + Crypto::CipherOperationSubtype mode; InitializedCipherModeFlowState() { this = TInitializedCipherModeFlowState(call) and DataFlow::localFlowStep(node1, node2) and node2.asExpr() = call.getQualifier() and - // I would imagine this would make this predicate horribly horribly inefficient - // it now binds with anything + // TODO: does this make this predicate inefficient as it binds with anything? not node1.asExpr() = call.getQualifier() and mode = call.getCipherOperationModeType() } - CipherInitCall getCall() { result = call } + CipherInitCall getInitCall() { result = call } DataFlow::Node getFstNode() { result = node1 } @@ -169,12 +180,14 @@ module JCAModel { */ DataFlow::Node getSndNode() { result = node2 } - override Crypto::CipherOperationMode getCipherOperationMode() { result = mode } + override Crypto::CipherOperationSubtype getCipherOperationMode() { result = mode } } /** - * Trace to a cryptographic operation, + * Trace from cipher initialization to a cryptographic operation, * specifically `Cipher.doFinal()`, `Cipher.wrap()`, or `Cipher.unwrap()`. + * + * TODO: handle `Cipher.update()` */ private module CipherGetInstanceToCipherOperationConfig implements DataFlow::StateConfigSig { class FlowState = TCipherModeFlowState; @@ -201,7 +214,7 @@ module JCAModel { exists(CipherInitCall call | node.asExpr() = call.getQualifier() | state instanceof UninitializedCipherModeFlowState or - state.(InitializedCipherModeFlowState).getCall() != call + state.(InitializedCipherModeFlowState).getInitCall() != call ) } } @@ -209,15 +222,16 @@ module JCAModel { module CipherGetInstanceToCipherOperationFlow = DataFlow::GlobalWithState; - class CipherEncryptionOperation extends Crypto::CipherOperationInstance instanceof Call { - Crypto::CipherOperationMode mode; - Crypto::EncryptionAlgorithmInstance algorithm; + class CipherOperationInstance extends Crypto::CipherOperationInstance instanceof Call { + Crypto::CipherOperationSubtype mode; + Crypto::CipherAlgorithmInstance algorithm; + CipherGetInstanceToCipherOperationFlow::PathNode sink; + JCACipherOperationCall doFinalize; - CipherEncryptionOperation() { + CipherOperationInstance() { exists( - CipherGetInstanceToCipherOperationFlow::PathNode sink, CipherGetInstanceToCipherOperationFlow::PathNode src, CipherGetInstanceCall getCipher, - JCACipherOperationCall doFinalize, CipherGetInstanceAlgorithmArg arg + CipherGetInstanceAlgorithmArg arg | CipherGetInstanceToCipherOperationFlow::flowPath(src, sink) and src.getNode().asExpr() = getCipher and @@ -229,9 +243,19 @@ module JCAModel { ) } - override Crypto::EncryptionAlgorithmInstance getAlgorithm() { result = algorithm } + override Crypto::CipherAlgorithmInstance getAlgorithm() { result = algorithm } - override Crypto::CipherOperationMode getCipherOperationMode() { result = mode } + override Crypto::CipherOperationSubtype getCipherOperationSubtype() { result = mode } + + override Crypto::NonceArtifactInstance getNonce() { + NonceArtifactToCipherInitCallFlow::flow(result.asOutputData(), + DataFlow::exprNode(sink.getState() + .(InitializedCipherModeFlowState) + .getInitCall() + .getNonceArg())) + } + + override DataFlow::Node getInputData() { result = doFinalize.getInputData() } } /** @@ -319,12 +343,12 @@ module JCAModel { CipherStringLiteral getInstance() { result = instance } } - class EncryptionAlgorithm extends Crypto::EncryptionAlgorithm { + class EncryptionAlgorithm extends Crypto::CipherAlgorithm { CipherStringLiteral origin; CipherGetInstanceAlgorithmArg instance; EncryptionAlgorithm() { - this = Crypto::TEncryptionAlgorithm(instance) and + this = Crypto::TCipherAlgorithm(instance) and instance.getOrigin() = origin } @@ -347,7 +371,7 @@ module JCAModel { override Crypto::TCipherType getCipherFamily() { if this.cipherNameMappingKnown(_, origin.getAlgorithmName()) then this.cipherNameMappingKnown(result, origin.getAlgorithmName()) - else result instanceof Crypto::OtherSymmetricCipherType + else result instanceof Crypto::OtherCipherType } override string getKeySize(Location location) { none() } @@ -384,33 +408,71 @@ module JCAModel { } /** - * Initialiation vectors + * Initialization vectors and other nonce artifacts */ - abstract class IVParameterInstantiation extends Crypto::InitializationVectorArtifactInstance instanceof ClassInstanceExpr + abstract class NonceParameterInstantiation extends Crypto::NonceArtifactInstance instanceof ClassInstanceExpr { - abstract Expr getInput(); + override DataFlow::Node asOutputData() { result.asExpr() = this } } - class IvParameterSpecInstance extends IVParameterInstantiation { + class IvParameterSpecInstance extends NonceParameterInstantiation { IvParameterSpecInstance() { this.(ClassInstanceExpr) .getConstructedType() .hasQualifiedName("javax.crypto.spec", "IvParameterSpec") } - override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(0) } + override DataFlow::Node getInput() { result.asExpr() = this.(ClassInstanceExpr).getArgument(0) } } - class GCMParameterSpecInstance extends IVParameterInstantiation { + // TODO: this also specifies the tag length for GCM + class GCMParameterSpecInstance extends NonceParameterInstantiation { GCMParameterSpecInstance() { this.(ClassInstanceExpr) .getConstructedType() .hasQualifiedName("javax.crypto.spec", "GCMParameterSpec") } - override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(1) } + override DataFlow::Node getInput() { result.asExpr() = this.(ClassInstanceExpr).getArgument(1) } + } + + class IvParameterSpecGetIvCall extends MethodCall { + IvParameterSpecGetIvCall() { + this.getMethod().hasQualifiedName("javax.crypto.spec", "IvParameterSpec", "getIV") + } } + module NonceArtifactToCipherInitCallConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node src) { + exists(NonceParameterInstantiation n | + src = n.asOutputData() and + not exists(IvParameterSpecGetIvCall m | n.getInput().asExpr() = m) + ) + } + + predicate isSink(DataFlow::Node sink) { + exists(CipherInitCall c | c.getNonceArg() = sink.asExpr()) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(IvParameterSpecGetIvCall m | + node1.asExpr() = m.getQualifier() and + node2.asExpr() = m + ) + or + exists(NonceParameterInstantiation n | + node1 = n.getInput() and + node2.asExpr() = n + ) + } + } + + module NonceArtifactToCipherInitCallFlow = DataFlow::Global; + + /** + * A data-flow configuration to track flow from a mode field access to + * the mode argument of the `init` method of the `javax.crypto.Cipher` class. + */ private module JavaxCipherModeAccessToInitConfig implements DataFlow::ConfigSig { predicate isSource(DataFlow::Node src) { src.asExpr() instanceof JavaxCryptoCipherOperationModeAccess @@ -423,6 +485,18 @@ module JCAModel { module JavaxCipherModeAccessToInitFlow = DataFlow::Global; + private predicate cipher_mode_str_to_cipher_mode_known( + string mode, Crypto::CipherOperationSubtype cipher_mode + ) { + mode = "ENCRYPT_MODE" and cipher_mode instanceof Crypto::EncryptionMode + or + mode = "WRAP_MODE" and cipher_mode instanceof Crypto::WrapMode + or + mode = "DECRYPT_MODE" and cipher_mode instanceof Crypto::DecryptionMode + or + mode = "UNWRAP_MODE" and cipher_mode instanceof Crypto::UnwrapMode + } + class CipherInitCall extends MethodCall { CipherInitCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "init") } @@ -443,49 +517,19 @@ module JCAModel { ) } - Crypto::CipherOperationMode getCipherOperationModeType() { - if not exists(this.getModeOrigin()) - then result instanceof Crypto::UnknownCipherOperationMode - else - if this.getModeOrigin().getField().getName() in ["ENCRYPT_MODE", "WRAP_MODE"] - then result instanceof Crypto::EncryptionMode - else - if this.getModeOrigin().getField().getName() in ["DECRYPT_MODE", "UNWRAP_MODE"] - then result instanceof Crypto::DecryptionMode - else - // TODO/Question: distinguish between unknown vs unspecified? (the field access is not recognized, vs no field access is found) - result instanceof Crypto::UnknownCipherOperationMode + Crypto::CipherOperationSubtype getCipherOperationModeType() { + if cipher_mode_str_to_cipher_mode_known(this.getModeOrigin().getField().getName(), _) + then cipher_mode_str_to_cipher_mode_known(this.getModeOrigin().getField().getName(), result) + else result instanceof Crypto::UnknownCipherOperationMode } - Expr getKey() { + Expr getKeyArg() { result = this.getArgument(1) and this.getMethod().getParameterType(1).hasName("Key") } - Expr getIV() { + Expr getNonceArg() { result = this.getArgument(2) and this.getMethod().getParameterType(2).hasName("AlgorithmParameterSpec") } } - - // TODO: cipher.getParameters().getParameterSpec(GCMParameterSpec.class); - /* - * class InitializationVectorArg extends Crypto::InitializationVectorArtifactInstance instanceof Expr - * { - * IVParameterInstantiation creation; - * - * InitializationVectorArg() { this = creation.getInput() } - * } - */ - - class InitializationVector extends Crypto::InitializationVector { - IVParameterInstantiation instance; - - InitializationVector() { this = Crypto::TInitializationVector(instance) } - - override Location getLocation() { result = instance.getLocation() } - - override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance } - - override Crypto::DataFlowNode getInputData() { result.asExpr() = instance.getInput() } - } } diff --git a/java/ql/lib/experimental/Quantum/Language.qll b/java/ql/lib/experimental/Quantum/Language.qll index 5801815109b0..e88bce6d9959 100644 --- a/java/ql/lib/experimental/Quantum/Language.qll +++ b/java/ql/lib/experimental/Quantum/Language.qll @@ -23,8 +23,6 @@ module CryptoInput implements InputSig { class LocatableElement = Language::Element; class UnknownLocation = UnknownDefaultLocation; - - predicate rngToIvFlow(DataFlowNode rng, DataFlowNode iv) { none() } } /** @@ -37,9 +35,7 @@ module Crypto = CryptographyBase; * tied to an output node (i.e., the result of the source of randomness) */ abstract class RandomnessInstance extends Crypto::RandomNumberGenerationInstance { - abstract Crypto::RNGSourceSecurity getSourceSecurity(); - - Crypto::TRNGSeedSecurity getSeedSecurity(Location location) { none() } + override DataFlow::Node asOutputData() { result.asExpr() = this } } class SecureRandomnessInstance extends RandomnessInstance { @@ -48,36 +44,10 @@ class SecureRandomnessInstance extends RandomnessInstance { s.getSourceOfRandomness() instanceof SecureRandomNumberGenerator ) } - - override Crypto::RNGSourceSecurity getSourceSecurity() { - result instanceof Crypto::RNGSourceSecure - } } class InsecureRandomnessInstance extends RandomnessInstance { InsecureRandomnessInstance() { exists(InsecureRandomnessSource node | this = node.asExpr()) } - - override Crypto::RNGSourceSecurity getSourceSecurity() { - result instanceof Crypto::RNGSourceInsecure - } -} - -class RandomnessArtifact extends Crypto::RandomNumberGeneration { - RandomnessInstance instance; - - RandomnessArtifact() { this = Crypto::TRandomNumberGeneration(instance) } - - override Location getLocation() { result = instance.getLocation() } - - override Crypto::RNGSourceSecurity getSourceSecurity() { result = instance.getSourceSecurity() } - - override Crypto::TRNGSeedSecurity getSeedSecurity(Location location) { - result = instance.getSeedSecurity(location) - } - - override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance } - - override Crypto::DataFlowNode getInputData() { none() } } // Import library-specific modeling diff --git a/java/ql/src/experimental/Quantum/ReusedNonce.ql b/java/ql/src/experimental/Quantum/ReusedNonce.ql new file mode 100644 index 000000000000..cb0d6ff9d610 --- /dev/null +++ b/java/ql/src/experimental/Quantum/ReusedNonce.ql @@ -0,0 +1,23 @@ +/** + * @name Unsafe nonce source or reuse + * @id java/unsafe-nonce-source-or-reuse + */ + +import experimental.Quantum.Language +import semmle.code.java.dataflow.DataFlow + +Element getNonceOrigin(Crypto::NonceArtifactInstance nonce) { + // TODO: this check is currently ultra hacky just for demoing + result = nonce.getInput().asExpr().(VarAccess).getVariable() +} + +from + Crypto::CipherOperationInstance op, Crypto::NonceArtifactInstance nonce1, + Crypto::NonceArtifactInstance nonce2 +where + op.(Expr).getEnclosingCallable().getName() = "encrypt" and + nonce1 = op.getNonce() and + nonce2 = op.getNonce() and + not nonce1 = nonce2 and + getNonceOrigin(nonce1) = getNonceOrigin(nonce2) +select op, nonce1, nonce2 diff --git a/java/ql/src/experimental/Quantum/Test.ql b/java/ql/src/experimental/Quantum/Test.ql deleted file mode 100644 index ba76213132c3..000000000000 --- a/java/ql/src/experimental/Quantum/Test.ql +++ /dev/null @@ -1,9 +0,0 @@ -/** - * @name "PQC Test" - */ - -import experimental.Quantum.Language - -from Crypto::EncryptionAlgorithm a, Crypto::ModeOfOperationAlgorithm m, Crypto::PaddingAlgorithm p -where m = a.getModeOfOperation() and p = a.getPadding() -select a, a.getRawAlgorithmName(), m, m.getRawAlgorithmName(), p, p.getRawAlgorithmName() diff --git a/java/ql/src/experimental/Quantum/TestCipher.ql b/java/ql/src/experimental/Quantum/TestCipher.ql new file mode 100644 index 000000000000..6be308c25606 --- /dev/null +++ b/java/ql/src/experimental/Quantum/TestCipher.ql @@ -0,0 +1,16 @@ +/** + * @name "PQC Test" + */ + +import experimental.Quantum.Language + +from + Crypto::CipherOperation op, Crypto::CipherAlgorithm a, Crypto::ModeOfOperationAlgorithm m, + Crypto::PaddingAlgorithm p, Crypto::Nonce nonce +where + a = op.getAlgorithm() and + m = a.getModeOfOperation() and + p = a.getPadding() and + nonce = op.getNonce() +select op, op.getCipherOperationMode(), a, a.getRawAlgorithmName(), m, m.getRawAlgorithmName(), p, + p.getRawAlgorithmName(), nonce, nonce.getInputData() diff --git a/misc/scripts/cryptography/cbom.sh b/misc/scripts/cryptography/cbom.sh index 9cbef951bbf4..ef558ccf432e 100755 --- a/misc/scripts/cryptography/cbom.sh +++ b/misc/scripts/cryptography/cbom.sh @@ -1,8 +1,8 @@ #!/bin/bash -CODEQL_PATH="/Users/nicolaswill/Library/Application Support/Code/User/globalStorage/github.vscode-codeql/distribution5/codeql/codeql" -DATABASE_PATH="/Users/nicolaswill/openssl_codeql/openssl/openssl_db" -QUERY_FILE="/Users/nicolaswill/pqc/codeql/cpp/ql/src/experimental/Quantum/CBOMGraph.ql" +CODEQL_PATH="/Users/nicolaswill/.local/share/gh/extensions/gh-codeql/dist/release/v2.20.4/codeql" +DATABASE_PATH="/Users/nicolaswill/pqc/gpt-crypto-test-cases/gpt_ai_gen_jca_test_cases_db" +QUERY_FILE="/Users/nicolaswill/pqc/codeql/java/ql/src/experimental/Quantum/PrintCBOMGraph.ql" OUTPUT_DIR="graph_output" python3 generate_cbom.py -c "$CODEQL_PATH" -d "$DATABASE_PATH" -q "$QUERY_FILE" -o "$OUTPUT_DIR" diff --git a/misc/scripts/cryptography/generate_cbom.py b/misc/scripts/cryptography/generate_cbom.py index 10ec895dc629..07400d6cd6a3 100644 --- a/misc/scripts/cryptography/generate_cbom.py +++ b/misc/scripts/cryptography/generate_cbom.py @@ -56,6 +56,9 @@ def convert_dgml_to_dot(dgml_file, dot_file): else: label_parts.append(f"{key}={value}") label = "\\n".join(label_parts) + # Escape forward slashes and double quotes + label = label.replace("/", "\\/") + label = label.replace("\"", "\\\"") prop_l = [f'label="{label}"'] node_s = f'nd_{node_id} [{", ".join(prop_l)}];' body_l.append(node_s) @@ -63,8 +66,11 @@ def convert_dgml_to_dot(dgml_file, dot_file): # Process edges for edge in root.find("{http://schemas.microsoft.com/vs/2009/dgml}Links"): att = edge.attrib + edge_label = att.get("Label", "") + edge_label = edge_label.replace("/", "\\/") + edge_label = edge_label.replace("\"", "\\\"") edge_s = 'nd_{} -> nd_{} [label="{}"];'.format( - att["Source"], att["Target"], att.get("Label", "")) + att["Source"], att["Target"], edge_label) body_l.append(edge_s) body_l.append("}") @@ -89,7 +95,7 @@ def main(): run_codeql_analysis(args.codeql, args.database, args.query, args.output) # Locate DGML file - dgml_file = os.path.join(args.output, "cbomgraph.dgml") + dgml_file = os.path.join(args.output, "java", "print-cbom-graph.dgml") dot_file = dgml_file.replace(".dgml", ".dot") if os.path.exists(dgml_file): diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index a0f22d0229b6..e5b91e198eaf 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -19,8 +19,6 @@ signature module InputSig { } class UnknownLocation instanceof Location; - - predicate rngToIvFlow(DataFlowNode rng, DataFlowNode iv); } module CryptographyBase Input> { @@ -34,11 +32,13 @@ module CryptographyBase Input> { UnknownPropertyValue() { this = "" } } - private string getPropertyAsGraphString(NodeBase node, string key) { + private string getPropertyAsGraphString(NodeBase node, string key, Location root) { result = strictconcat(any(string value, Location location, string parsed | node.properties(key, value, location) and - parsed = "(" + value + "," + location.toString() + ")" + if location = root or location instanceof UnknownLocation + then parsed = value + else parsed = "(" + value + "," + location.toString() + ")" | parsed ), "," @@ -46,19 +46,26 @@ module CryptographyBase Input> { } predicate nodes_graph_impl(NodeBase node, string key, string value) { - key = "semmle.label" and - value = node.toString() - or - // CodeQL's DGML output does not include a location - key = "Location" and - value = node.getLocation().toString() - or - // Known unknown edges should be reported as properties rather than edges - node = node.getChild(key) and - value = "" - or - // Report properties - value = getPropertyAsGraphString(node, key) + not ( + // exclude Artifact nodes with no edges to or from them + node instanceof Artifact and + not (edges_graph_impl(node, _, _, _) or edges_graph_impl(_, node, _, _)) + ) and + ( + key = "semmle.label" and + value = node.toString() + or + // CodeQL's DGML output does not include a location + key = "Location" and + value = node.getLocation().toString() + or + // Known unknown edges should be reported as properties rather than edges + node = node.getChild(key) and + value = "" + or + // Report properties + value = getPropertyAsGraphString(node, key, node.getLocation()) + ) } predicate edges_graph_impl(NodeBase source, NodeBase target, string key, string value) { @@ -80,12 +87,16 @@ module CryptographyBase Input> { abstract class KeyDerivationAlgorithmInstance extends LocatableElement { } abstract class CipherOperationInstance extends LocatableElement { - abstract EncryptionAlgorithmInstance getAlgorithm(); + abstract CipherAlgorithmInstance getAlgorithm(); + + abstract CipherOperationSubtype getCipherOperationSubtype(); - abstract CipherOperationMode getCipherOperationMode(); + abstract NonceArtifactInstance getNonce(); + + abstract DataFlowNode getInputData(); } - abstract class EncryptionAlgorithmInstance extends LocatableElement { } + abstract class CipherAlgorithmInstance extends LocatableElement { } abstract class KeyEncapsulationOperationInstance extends LocatableElement { } @@ -99,21 +110,26 @@ module CryptographyBase Input> { abstract class PaddingAlgorithmInstance extends LocatableElement { } // Artifacts - abstract class DigestArtifactInstance extends LocatableElement { } + abstract private class ArtifactLocatableElement extends LocatableElement { + abstract DataFlowNode asOutputData(); - abstract class KeyArtifactInstance extends LocatableElement { } + abstract DataFlowNode getInput(); + } - abstract class InitializationVectorArtifactInstance extends LocatableElement { } + abstract class DigestArtifactInstance extends ArtifactLocatableElement { } - abstract class NonceArtifactInstance extends LocatableElement { } + abstract class KeyArtifactInstance extends ArtifactLocatableElement { } - abstract class RandomNumberGenerationInstance extends LocatableElement { } + abstract class NonceArtifactInstance extends ArtifactLocatableElement { } + + abstract class RandomNumberGenerationInstance extends ArtifactLocatableElement { + final override DataFlowNode getInput() { none() } + } newtype TNode = // Artifacts (data that is not an operation or algorithm, e.g., a key) TDigest(DigestArtifactInstance e) or TKey(KeyArtifactInstance e) or - TInitializationVector(InitializationVectorArtifactInstance e) or TNonce(NonceArtifactInstance e) or TRandomNumberGeneration(RandomNumberGenerationInstance e) or // Operations (e.g., hashing, encryption) @@ -122,7 +138,7 @@ module CryptographyBase Input> { TCipherOperation(CipherOperationInstance e) or TKeyEncapsulationOperation(KeyEncapsulationOperationInstance e) or // Algorithms (e.g., SHA-256, AES) - TEncryptionAlgorithm(EncryptionAlgorithmInstance e) or + TCipherAlgorithm(CipherAlgorithmInstance e) or TEllipticCurveAlgorithm(EllipticCurveAlgorithmInstance e) or THashAlgorithm(HashAlgorithmInstance e) or TKeyDerivationAlgorithm(KeyDerivationAlgorithmInstance e) or @@ -133,10 +149,10 @@ module CryptographyBase Input> { TPaddingAlgorithm(PaddingAlgorithmInstance e) or // Composite and hybrid cryptosystems (e.g., RSA-OAEP used with AES, post-quantum hybrid cryptosystems) // These nodes are always parent nodes and are not modeled but rather defined via library-agnostic patterns. - TKemDemHybridCryptosystem(EncryptionAlgorithm dem) or // TODO, change this relation and the below ones - TKeyAgreementHybridCryptosystem(EncryptionAlgorithmInstance ka) or - TAsymmetricEncryptionMacHybridCryptosystem(EncryptionAlgorithmInstance enc) or - TPostQuantumHybridCryptosystem(EncryptionAlgorithmInstance enc) + TKemDemHybridCryptosystem(CipherAlgorithm dem) or // TODO, change this relation and the below ones + TKeyAgreementHybridCryptosystem(CipherAlgorithmInstance ka) or + TAsymmetricEncryptionMacHybridCryptosystem(CipherAlgorithmInstance enc) or + TPostQuantumHybridCryptosystem(CipherAlgorithmInstance enc) /** * The base class for all cryptographic assets, such as operations and algorithms. @@ -183,7 +199,7 @@ module CryptographyBase Input> { } /** - * Returns the parent of this node. + * Returns a parent of this node. */ final NodeBase getAParent() { result.getChild(_) = this } } @@ -197,43 +213,43 @@ module CryptographyBase Input> { } /** - * An initialization vector + * A nonce or initialization vector */ - abstract class InitializationVector extends Artifact, TInitializationVector { - final override string getInternalType() { result = "InitializationVector" } + private class NonceImpl extends Artifact, TNonce { + NonceArtifactInstance instance; - RandomNumberGeneration getRNGSource() { - Input::rngToIvFlow(result.asOutputData(), this.getInputData()) - } - } + NonceImpl() { this = TNonce(instance) } - newtype TRNGSourceSecurity = - RNGSourceSecure() or // Secure RNG source (unrelated to seed) - RNGSourceInsecure() // Insecure RNG source (unrelated to seed) + final override string getInternalType() { result = "Nonce" } - class RNGSourceSecurity extends TRNGSourceSecurity { - string toString() { - this instanceof RNGSourceSecure and result = "Secure RNG Source" - or - this instanceof RNGSourceInsecure and result = "Insecure RNG Source" - } + override Location getLocation() { result = instance.getLocation() } + + override DataFlowNode asOutputData() { result = instance.asOutputData() } + + override DataFlowNode getInputData() { result = instance.getInput() } } - newtype TRNGSeedSecurity = - RNGSeedSecure() or - RNGSeedInsecure() + final class Nonce = NonceImpl; /** * A source of random number generation */ - abstract class RandomNumberGeneration extends Artifact, TRandomNumberGeneration { + final private class RandomNumberGenerationImpl extends Artifact, TRandomNumberGeneration { + RandomNumberGenerationInstance instance; + + RandomNumberGenerationImpl() { this = TRandomNumberGeneration(instance) } + final override string getInternalType() { result = "RandomNumberGeneration" } - abstract RNGSourceSecurity getSourceSecurity(); + override Location getLocation() { result = instance.getLocation() } + + override DataFlowNode asOutputData() { result = instance.asOutputData() } - abstract TRNGSeedSecurity getSeedSecurity(Location location); + override DataFlowNode getInputData() { result = instance.getInput() } } + final class RandomNumberGeneration = RandomNumberGenerationImpl; + /** * A cryptographic operation, such as hashing or encryption. */ @@ -243,14 +259,6 @@ module CryptographyBase Input> { */ abstract Algorithm getAlgorithm(); - // TODO: I only removed this because I want the operation type to be non-string - // since for CipherOperations the user will have to pick the right type, - // and I want to force them to use a type that is restricted. In this case to a TCipherOperationType - // /** - // * Gets the name of this operation, e.g., "hash" or "encrypt". - // */ - // abstract string getOperationType(); - // final override string getInternalType() { result = this.getOperationType() } override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or @@ -685,24 +693,34 @@ module CryptographyBase Input> { abstract override string getRawAlgorithmName(); } - newtype TCipherOperationMode = + newtype TCipherOperationSubtype = TEncryptionMode() or TDecryptionMode() or + TWrapMode() or + TUnwrapMode() or TUnknownCipherOperationMode() - abstract class CipherOperationMode extends TCipherOperationMode { + abstract class CipherOperationSubtype extends TCipherOperationSubtype { abstract string toString(); } - class EncryptionMode extends CipherOperationMode, TEncryptionMode { - override string toString() { result = "Encryption" } + class EncryptionMode extends CipherOperationSubtype, TEncryptionMode { + override string toString() { result = "Encrypt" } } - class DecryptionMode extends CipherOperationMode, TDecryptionMode { - override string toString() { result = "Decryption" } + class DecryptionMode extends CipherOperationSubtype, TDecryptionMode { + override string toString() { result = "Decrypt" } } - class UnknownCipherOperationMode extends CipherOperationMode, TUnknownCipherOperationMode { + class WrapMode extends CipherOperationSubtype, TWrapMode { + override string toString() { result = "Wrap" } + } + + class UnwrapMode extends CipherOperationSubtype, TUnwrapMode { + override string toString() { result = "Unwrap" } + } + + class UnknownCipherOperationMode extends CipherOperationSubtype, TUnknownCipherOperationMode { override string toString() { result = "Unknown" } } @@ -711,32 +729,51 @@ module CryptographyBase Input> { * This operation takes an input message (plaintext) of arbitrary content and length * and produces a ciphertext as the output using a specified encryption algorithm (with a mode and padding). */ - // NOTE FOR NICK: making this concrete here as I don't think users need to worry about making/extending these operations, just instances - class CipherOperation extends Operation, TCipherOperation { + class CipherOperationImpl extends Operation, TCipherOperation { CipherOperationInstance instance; - CipherOperation() { this = TCipherOperation(instance) } + CipherOperationImpl() { this = TCipherOperation(instance) } + + override string getInternalType() { result = "CipherOperation" } override Location getLocation() { result = instance.getLocation() } - final TCipherOperationMode getCipherOperationMode() { - result = instance.getCipherOperationMode() + CipherOperationSubtype getCipherOperationMode() { + result = instance.getCipherOperationSubtype() } - final override EncryptionAlgorithm getAlgorithm() { - result.getInstance() = instance.getAlgorithm() + final override CipherAlgorithm getAlgorithm() { result.getInstance() = instance.getAlgorithm() } + + override NodeBase getChild(string key) { + result = super.getChild(key) + or + // [KNOWN_OR_UNKNOWN] + key = "nonce" and + if exists(this.getNonce()) then result = this.getNonce() else result = this } - override string getInternalType() { result = "CipherOperation" } - // /** - // * Gets the initialization vector associated with this encryption operation. - // * - // * This predicate does not need to hold for all encryption operations, - // * as the initialization vector is not always required. - // */ - // abstract InitializationVector getInitializationVector(); + override predicate properties(string key, string value, Location location) { + super.properties(key, value, location) + or + // [ALWAYS_KNOWN] - Unknown is handled in getCipherOperationMode() + key = "operation" and + value = this.getCipherOperationMode().toString() and + location = this.getLocation() + } + + /** + * Gets the initialization vector associated with this encryption operation. + * + * This predicate does not need to hold for all encryption operations, + * as the initialization vector is not always required. + */ + Nonce getNonce() { result = TNonce(instance.getNonce()) } + + DataFlowNode getInputData() { result = instance.getInputData() } } + final class CipherOperation = CipherOperationImpl; + /** * Block cipher modes of operation algorithms */ @@ -858,10 +895,10 @@ module CryptographyBase Input> { RC4() or RC5() or RSA() or - OtherSymmetricCipherType() + OtherCipherType() - abstract class EncryptionAlgorithm extends Algorithm, TEncryptionAlgorithm { - final LocatableElement getInstance() { this = TEncryptionAlgorithm(result) } + abstract class CipherAlgorithm extends Algorithm, TCipherAlgorithm { + final LocatableElement getInstance() { this = TCipherAlgorithm(result) } final TCipherStructureType getCipherStructure() { this.cipherFamilyToNameAndStructure(this.getCipherFamily(), _, result) @@ -871,7 +908,7 @@ module CryptographyBase Input> { this.cipherFamilyToNameAndStructure(this.getCipherFamily(), result, _) } - final override string getAlgorithmType() { result = "EncryptionAlgorithm" } + override string getAlgorithmType() { result = "CipherAlgorithm" } /** * Gets the key size of this cipher, e.g., "128" or "256". @@ -917,7 +954,7 @@ module CryptographyBase Input> { or type instanceof RSA and name = "RSA" and s = Asymmetric() or - type instanceof OtherSymmetricCipherType and + type instanceof OtherCipherType and name = this.getRawAlgorithmName() and s = UnknownCipherStructureType() } @@ -929,19 +966,21 @@ module CryptographyBase Input> { override NodeBase getChild(string edgeName) { result = super.getChild(edgeName) or - ( - // [KNOWN_OR_UNKNOWN] - edgeName = "mode" and - if exists(this.getModeOfOperation()) - then result = this.getModeOfOperation() - else result = this - ) + // [KNOWN_OR_UNKNOWN] + edgeName = "mode" and + if exists(this.getModeOfOperation()) + then result = this.getModeOfOperation() + else result = this + or + // [KNOWN_OR_UNKNOWN] + edgeName = "padding" and + if exists(this.getPadding()) then result = this.getPadding() else result = this } override predicate properties(string key, string value, Location location) { super.properties(key, value, location) or - // [ALWAYS_KNOWN]: unknown case is handled in `getCipherStructureTypeString` + // [ALWAYS_KNOWN] - unknown case is handled in `getCipherStructureTypeString` key = "structure" and getCipherStructureTypeString(this.getCipherStructure()) = value and location instanceof UnknownLocation From 95544e20b2715e7cc108f4ec16fbeecee3fce160 Mon Sep 17 00:00:00 2001 From: Kristen Newbury Date: Mon, 24 Feb 2025 13:09:38 -0500 Subject: [PATCH 28/28] Add model and sample query for constants used in key specs --- java/ql/lib/experimental/Quantum/JCA.qll | 27 +++++++++++++ .../experimental/Quantum/ConstantPassword.ql | 38 +++++++++++++++++++ .../codeql/cryptography/Model.qll | 22 +++++++++++ 3 files changed, 87 insertions(+) create mode 100644 java/ql/src/experimental/Quantum/ConstantPassword.ql diff --git a/java/ql/lib/experimental/Quantum/JCA.qll b/java/ql/lib/experimental/Quantum/JCA.qll index 9892b445312a..3e2d6b53d944 100644 --- a/java/ql/lib/experimental/Quantum/JCA.qll +++ b/java/ql/lib/experimental/Quantum/JCA.qll @@ -532,4 +532,31 @@ module JCAModel { this.getMethod().getParameterType(2).hasName("AlgorithmParameterSpec") } } + + /** + * Key Material Concept + * any class that implements `java.security.spec.KeySpec` + */ + class KeyMaterialObject extends Class { + KeyMaterialObject() { + exists(RefType t | + this.extendsOrImplements*(t) and + t.hasQualifiedName("java.security.spec", "KeySpec") + ) + } + } + + /** + * KeyMaterial + * ie some plain material that gets used to generate a Key + */ + class KeyMaterialInstantiation extends Crypto::KeyMaterialInstance instanceof ClassInstanceExpr { + KeyMaterialInstantiation() { + this.(ClassInstanceExpr).getConstructedType() instanceof KeyMaterialObject + } + + override DataFlow::Node asOutputData() { result.asExpr() = this } + + override DataFlow::Node getInput() { result.asExpr() = this.(ClassInstanceExpr).getArgument(0) } + } } diff --git a/java/ql/src/experimental/Quantum/ConstantPassword.ql b/java/ql/src/experimental/Quantum/ConstantPassword.ql new file mode 100644 index 000000000000..4d895ac8c0f8 --- /dev/null +++ b/java/ql/src/experimental/Quantum/ConstantPassword.ql @@ -0,0 +1,38 @@ +/** + * @name Constant password + * @description Using constant passwords is not secure, because potential attackers can easily recover them from the source code. + * @kind problem + * @problem.severity error + * @security-severity 6.8 + * @precision high + * @id java/constant-password-new-model + * @tags security + * external/cwe/cwe-259 + */ + +//this query is a replica of the concept in: https://github.com/github/codeql/blob/main/swift/ql/src/queries/Security/CWE-259/ConstantPassword.ql +//but uses the **NEW MODELLING** +import experimental.Quantum.Language +import semmle.code.java.dataflow.TaintTracking + +/** + * A constant password is created through either a byte array or string literals. + */ +class ConstantPasswordSource extends Expr { + ConstantPasswordSource() { + this instanceof CharacterLiteral or + this instanceof StringLiteral + } +} + +module ConstantToKeyDerivationFlow implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { source.asExpr() instanceof ConstantPasswordSource } + + predicate isSink(DataFlow::Node sink) { any(Crypto::KeyMaterialInstance i).getInput() = sink } +} + +module ConstantToKeyDerivationFlowInit = TaintTracking::Global; + +from DataFlow::Node source, DataFlow::Node sink +where ConstantToKeyDerivationFlowInit::flow(source, sink) +select sink, "Constant password $@ is used.", source, source.toString() diff --git a/shared/cryptography/codeql/cryptography/Model.qll b/shared/cryptography/codeql/cryptography/Model.qll index e5b91e198eaf..1b96ba4cf3f4 100644 --- a/shared/cryptography/codeql/cryptography/Model.qll +++ b/shared/cryptography/codeql/cryptography/Model.qll @@ -118,6 +118,8 @@ module CryptographyBase Input> { abstract class DigestArtifactInstance extends ArtifactLocatableElement { } + abstract class KeyMaterialInstance extends ArtifactLocatableElement { } + abstract class KeyArtifactInstance extends ArtifactLocatableElement { } abstract class NonceArtifactInstance extends ArtifactLocatableElement { } @@ -130,6 +132,7 @@ module CryptographyBase Input> { // Artifacts (data that is not an operation or algorithm, e.g., a key) TDigest(DigestArtifactInstance e) or TKey(KeyArtifactInstance e) or + TKeyMaterial(KeyMaterialInstance e) or TNonce(NonceArtifactInstance e) or TRandomNumberGeneration(RandomNumberGenerationInstance e) or // Operations (e.g., hashing, encryption) @@ -1000,4 +1003,23 @@ module CryptographyBase Input> { abstract class KEMAlgorithm extends TKeyEncapsulationAlgorithm, Algorithm { final override string getAlgorithmType() { result = "KeyEncapsulationAlgorithm" } } + + /** + * A Key Material Object + */ + private class KeyMaterialImpl extends Artifact, TKeyMaterial { + KeyMaterialInstance instance; + + KeyMaterialImpl() { this = TKeyMaterial(instance) } + + final override string getInternalType() { result = "KeyMaterial" } + + override Location getLocation() { result = instance.getLocation() } + + override DataFlowNode asOutputData() { result = instance.asOutputData() } + + override DataFlowNode getInputData() { result = instance.getInput() } + } + + final class KeyMaterial = KeyMaterialImpl; }