Skip to content

Commit 5f355c7

Browse files
knewbury01knewbury01
committed
Add first sample JCA encryption model
1 parent e027b0e commit 5f355c7

File tree

4 files changed

+383
-0
lines changed

4 files changed

+383
-0
lines changed

‎java/ql/lib/experimental/Quantum/Base.qll‎

Lines changed: 235 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,235 @@
1+
/**
2+
* A language-independent library for reasoning about cryptography.
3+
*/
4+
5+
import codeql.util.Location
6+
import codeql.util.Option
7+
8+
signature module InputSig<LocationSig Location> {
9+
class LocatableElement {
10+
Location getLocation();
11+
}
12+
13+
class UnknownLocation instanceof Location;
14+
}
15+
16+
module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
17+
final class LocatableElement = Input::LocatableElement;
18+
19+
final class UnknownLocation = Input::UnknownLocation;
20+
21+
final class UnknownPropertyValue extends string {
22+
UnknownPropertyValue() { this = "<unknown>" }
23+
}
24+
25+
abstract class NodeBase instanceof LocatableElement {
26+
/**
27+
* Returns a string representation of this node, usually the name of the operation/algorithm/property.
28+
*/
29+
abstract string toString();
30+
31+
/**
32+
* Returns the location of this node in the code.
33+
*/
34+
Location getLocation() { result = super.getLocation() }
35+
36+
/**
37+
* Gets the origin of this node, e.g., a string literal in source describing it.
38+
*/
39+
LocatableElement getOrigin(string value) { none() }
40+
41+
/**
42+
* Returns the child of this node with the given edge name.
43+
*
44+
* This predicate is used by derived classes to construct the graph of cryptographic operations.
45+
*/
46+
NodeBase getChild(string edgeName) { none() }
47+
48+
/**
49+
* Defines properties of this node by name and either a value or location or both.
50+
*
51+
* This predicate is used by derived classes to construct the graph of cryptographic operations.
52+
*/
53+
predicate properties(string key, string value, Location location) {
54+
key = "origin" and location = this.getOrigin(value).getLocation()
55+
}
56+
57+
/**
58+
* Returns the parent of this node.
59+
*/
60+
final NodeBase getAParent() { result.getChild(_) = this }
61+
}
62+
63+
class Asset = NodeBase;
64+
65+
/**
66+
* A cryptographic operation, such as hashing or encryption.
67+
*/
68+
abstract class Operation extends Asset {
69+
/**
70+
* Gets the algorithm associated with this operation.
71+
*/
72+
abstract Algorithm getAlgorithm();
73+
74+
/**
75+
* Gets the name of this operation, e.g., "hash" or "encrypt".
76+
*/
77+
abstract string getOperationName();
78+
79+
final override string toString() { result = this.getOperationName() }
80+
81+
override NodeBase getChild(string edgeName) {
82+
result = super.getChild(edgeName)
83+
or
84+
edgeName = "uses" and
85+
if exists(this.getAlgorithm()) then result = this.getAlgorithm() else result = this
86+
}
87+
}
88+
89+
abstract class Algorithm extends Asset {
90+
/**
91+
* Gets the name of this algorithm, e.g., "AES" or "SHA".
92+
*/
93+
abstract string getAlgorithmName();
94+
95+
final override string toString() { result = this.getAlgorithmName() }
96+
}
97+
98+
/**
99+
* A hashing operation that processes data to generate a hash value.
100+
* This operation takes an input message of arbitrary content and length and produces a fixed-size
101+
* hash value as the output using a specified hashing algorithm.
102+
*/
103+
abstract class HashOperation extends Operation {
104+
abstract override HashAlgorithm getAlgorithm();
105+
106+
override string getOperationName() { result = "HASH" }
107+
}
108+
109+
// Rule: no newtype representing a type of algorithm should be modelled with multiple interfaces
110+
//
111+
// Example: HKDF and PKCS12KDF are both key derivation algorithms.
112+
// However, PKCS12KDF also has a property: the iteration count.
113+
//
114+
// If we have HKDF and PKCS12KDF under TKeyDerivationType,
115+
// someone modelling a library might try to make a generic identification of both of those algorithms.
116+
//
117+
// They will therefore not use the specialized type for PKCS12KDF,
118+
// meaning "from PKCS12KDF algo select algo" will have no results.
119+
//
120+
newtype THashType =
121+
// We're saying by this that all of these have an identical interface / properties / edges
122+
MD5() or
123+
SHA1() or
124+
SHA256() or
125+
SHA512() or
126+
OtherHashType()
127+
128+
/**
129+
* A hashing algorithm that transforms variable-length input into a fixed-size hash value.
130+
*/
131+
abstract class HashAlgorithm extends Algorithm {
132+
final predicate hashTypeToNameMapping(THashType type, string name) {
133+
type instanceof MD5 and name = "MD5"
134+
or
135+
type instanceof SHA1 and name = "SHA-1"
136+
or
137+
type instanceof SHA256 and name = "SHA-256"
138+
or
139+
type instanceof SHA512 and name = "SHA-512"
140+
or
141+
type instanceof OtherHashType and name = this.getRawAlgorithmName()
142+
}
143+
144+
abstract THashType getHashType();
145+
146+
override string getAlgorithmName() { this.hashTypeToNameMapping(this.getHashType(), result) }
147+
148+
/**
149+
* Gets the raw name of this hash algorithm from source.
150+
*/
151+
abstract string getRawAlgorithmName();
152+
}
153+
154+
/**
155+
* An operation that derives one or more keys from an input value.
156+
*/
157+
abstract class KeyDerivationOperation extends Operation {
158+
override string getOperationName() { result = "KEY_DERIVATION" }
159+
}
160+
161+
/**
162+
* An algorithm that derives one or more keys from an input value.
163+
*/
164+
abstract class KeyDerivationAlgorithm extends Algorithm {
165+
abstract override string getAlgorithmName();
166+
}
167+
168+
/**
169+
* HKDF key derivation function
170+
*/
171+
abstract class HKDF extends KeyDerivationAlgorithm {
172+
final override string getAlgorithmName() { result = "HKDF" }
173+
174+
abstract HashAlgorithm getHashAlgorithm();
175+
176+
override NodeBase getChild(string edgeName) {
177+
result = super.getChild(edgeName)
178+
or
179+
edgeName = "digest" and result = this.getHashAlgorithm()
180+
}
181+
}
182+
183+
/**
184+
* PKCS #12 key derivation function
185+
*/
186+
abstract class PKCS12KDF extends KeyDerivationAlgorithm {
187+
final override string getAlgorithmName() { result = "PKCS12KDF" }
188+
189+
abstract HashAlgorithm getHashAlgorithm();
190+
191+
override NodeBase getChild(string edgeName) {
192+
result = super.getChild(edgeName)
193+
or
194+
edgeName = "digest" and result = this.getHashAlgorithm()
195+
}
196+
}
197+
198+
/**
199+
* Elliptic curve algorithm
200+
*/
201+
abstract class EllipticCurve extends Algorithm {
202+
abstract string getVersion(Location location);
203+
204+
abstract string getKeySize(Location location);
205+
206+
override predicate properties(string key, string value, Location location) {
207+
super.properties(key, value, location)
208+
or
209+
key = "version" and
210+
if exists(this.getVersion(location))
211+
then value = this.getVersion(location)
212+
else (
213+
value instanceof UnknownPropertyValue and location instanceof UnknownLocation
214+
)
215+
or
216+
key = "key_size" and
217+
if exists(this.getKeySize(location))
218+
then value = this.getKeySize(location)
219+
else (
220+
value instanceof UnknownPropertyValue and location instanceof UnknownLocation
221+
)
222+
}
223+
}
224+
225+
/**
226+
* An encryption operation that processes plaintext to generate a ciphertext.
227+
* 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).
228+
*/
229+
abstract class EncryptionOperation extends Operation {
230+
abstract override Algorithm getAlgorithm();
231+
232+
override string getOperationName() { result = "ENCRYPTION" }
233+
}
234+
}
235+

‎java/ql/lib/experimental/Quantum/JCA.qll‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
import java
2+
import semmle.code.java.dataflow.DataFlow
3+
4+
module JCAModel {
5+
import Language
6+
7+
abstract class EncryptionOperation extends Crypto::EncryptionOperation { }
8+
9+
//TODO PBEWith can have suffixes. how to do? enumerate? or match a pattern?
10+
predicate cipher_names(string algo) { algo = ["AES", "AESWrap", "AESWrapPad", "ARCFOUR", "Blowfish", "ChaCha20", "ChaCha20-Poly1305", "DES", "DESede", "DESedeWrap", "ECIES", "PBEWith", "RC2", "RC4", "RC5", "RSA"] }
11+
//TODO solve the fact that x is an int of various values. same as above... enumerate?
12+
predicate cipher_modes(string mode) {mode = ["NONE", "CBC", "CCM", "CFB", "CFBx", "CTR", "CTS", "ECB", "GCM", "KW", "KWP", "OFB", "OFBx", "PCBC"]}
13+
//todo same as above, OAEPWith has asuffix type
14+
predicate cipher_padding(string padding) {padding = ["NoPadding", "ISO10126Padding", "OAEPPadding", "OAEPWith", "PKCS1Padding", "PKCS5Padding", "SSL3Padding"]}
15+
16+
/**
17+
* Symmetric algorithms
18+
*/
19+
abstract class SymmetricAlgorithm extends Crypto::Algorithm {
20+
21+
22+
//TODO figure out how to get this from the Cipher interface, is it explicit?
23+
//abstract string getKeySize(Location location);
24+
25+
// override predicate properties(string key, string value, Location location) {
26+
// super.properties(key, value, location)
27+
// or
28+
// key = "key_size" and
29+
// if exists(this.getKeySize(location))
30+
// then value = this.getKeySize(location)
31+
// else (
32+
// value instanceof Crypto::UnknownPropertyValue and location instanceof UnknownLocation
33+
// )
34+
// // other properties, like field type are possible, but not modeled until considered necessary
35+
// }
36+
37+
abstract override string getAlgorithmName();
38+
}
39+
40+
////cipher specifics ----------------------------------------
41+
42+
class CipherInstance extends Call {
43+
CipherInstance() { this.getCallee().hasQualifiedName("javax.crypto","Cipher", "getInstance") }
44+
45+
Expr getAlgorithmArg() { result = this.getArgument(0) }
46+
}
47+
48+
class CipherAlgorithmStringLiteral extends Crypto::NodeBase instanceof StringLiteral {
49+
CipherAlgorithmStringLiteral() { cipher_names(this.getValue().splitAt("/"))}
50+
51+
override string toString() { result = this.(StringLiteral).toString() }
52+
53+
string getValue() { result = this.(StringLiteral).getValue() }
54+
}
55+
56+
class CipherAlgorithmModeStringLiteral extends Crypto::NodeBase instanceof StringLiteral {
57+
CipherAlgorithmModeStringLiteral() { cipher_modes(this.getValue().splitAt("/"))}
58+
59+
override string toString() { result = this.(StringLiteral).toString() }
60+
61+
string getValue() { result = this.(StringLiteral).getValue() }
62+
}
63+
64+
class CipherAlgorithmPaddingStringLiteral extends Crypto::NodeBase instanceof StringLiteral {
65+
CipherAlgorithmPaddingStringLiteral() { cipher_padding(this.getValue().splitAt("/"))}
66+
67+
override string toString() { result = this.(StringLiteral).toString() }
68+
69+
string getValue() { result = this.(StringLiteral).getValue() }
70+
}
71+
72+
private module AlgorithmStringToFetchConfig implements DataFlow::ConfigSig {
73+
predicate isSource(DataFlow::Node src) { src.asExpr() instanceof CipherAlgorithmStringLiteral }
74+
75+
predicate isSink(DataFlow::Node sink) {
76+
exists(CipherInstance call | sink.asExpr() = call.getAlgorithmArg())
77+
}
78+
}
79+
80+
module AlgorithmStringToFetchFlow = DataFlow::Global<AlgorithmStringToFetchConfig>;
81+
82+
predicate algorithmStringToCipherInstanceArgFlow(string name, CipherAlgorithmStringLiteral origin, Expr arg) {
83+
exists(CipherInstance sinkCall |
84+
origin.getValue().toUpperCase() = name and
85+
arg = sinkCall.getAlgorithmArg() and
86+
AlgorithmStringToFetchFlow::flow(DataFlow::exprNode(origin), DataFlow::exprNode(arg))
87+
)
88+
}
89+
90+
class AES extends SymmetricAlgorithm instanceof Expr {
91+
CipherAlgorithmStringLiteral origin;
92+
93+
AES() { algorithmStringToCipherInstanceArgFlow("AES", origin, this) }
94+
95+
override Crypto::LocatableElement getOrigin(string name) {
96+
result = origin and name = origin.toString()
97+
}
98+
99+
override string getAlgorithmName(){ result = "AES"}
100+
}
101+
102+
103+
104+
105+
}

‎java/ql/lib/experimental/Quantum/Language.qll‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
private import Base
2+
private import java as Lang
3+
4+
/**
5+
* A dummy location which is used when something doesn't have a location in
6+
* the source code but needs to have a `Location` associated with it. There
7+
* may be several distinct kinds of unknown locations. For example: one for
8+
* expressions, one for statements and one for other program elements.
9+
*/
10+
class UnknownLocation extends Location {
11+
UnknownLocation() { this.getFile().getAbsolutePath() = "" }
12+
}
13+
14+
/**
15+
* A dummy location which is used when something doesn't have a location in
16+
* the source code but needs to have a `Location` associated with it.
17+
*/
18+
class UnknownDefaultLocation extends UnknownLocation {
19+
UnknownDefaultLocation() { locations_default(this, _, 0, 0, 0, 0) }
20+
}
21+
22+
module CryptoInput implements InputSig<Lang::Location> {
23+
class LocatableElement = Lang::Element;
24+
25+
class UnknownLocation = UnknownDefaultLocation;
26+
}
27+
28+
module Crypto = CryptographyBase<Lang::Location, CryptoInput>;
29+
30+
import JCA

‎java/ql/src/experimental/Quantum/Test.ql‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
/**
2+
* @name "PQC Test"
3+
*/
4+
5+
import experimental.Quantum.Language
6+
//import java
7+
8+
from Crypto::NodeBase node
9+
select node
10+
11+
// from Class t
12+
// where t.hasQualifiedName("javax.crypto", "CipherSpi")
13+
// select t, t.getADescendant*()

0 commit comments

Comments
 (0)