Skip to content

Commit 2b0b927

Browse files
nicolaswillnicolaswill
committed
Add Nonce association to Operation, update graph
1 parent 86cab46 commit 2b0b927

File tree

8 files changed

+297
-208
lines changed

8 files changed

+297
-208
lines changed

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

Lines changed: 110 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
import java
22
import semmle.code.java.dataflow.DataFlow
3+
import semmle.code.java.controlflow.Dominance
34

45
module JCAModel {
56
import Language
@@ -64,6 +65,8 @@ module JCAModel {
6465
this.getCallee().hasQualifiedName("javax.crypto", "Cipher", s)
6566
)
6667
}
68+
69+
DataFlow::Node getInputData() { result.asExpr() = this.getArgument(0) }
6770
}
6871

6972
/**
@@ -84,7 +87,7 @@ module JCAModel {
8487
*
8588
* For example, in `Cipher.getInstance(algorithm)`, this class represents `algorithm`.
8689
*/
87-
class CipherGetInstanceAlgorithmArg extends Crypto::EncryptionAlgorithmInstance,
90+
class CipherGetInstanceAlgorithmArg extends Crypto::CipherAlgorithmInstance,
8891
Crypto::BlockCipherModeOfOperationAlgorithmInstance, Crypto::PaddingAlgorithmInstance instanceof Expr
8992
{
9093
CipherGetInstanceCall call;
@@ -116,13 +119,22 @@ module JCAModel {
116119
private class JavaxCryptoCipherOperationModeAccess extends FieldAccess {
117120
JavaxCryptoCipherOperationModeAccess() {
118121
this.getQualifier() instanceof CipherAccess and
119-
this.getField().getName() in ["ENCRYPT_MODE", "DECRYPT_MODE", "WRAP_MODE", "UNWRAP_MODE"]
122+
this.getField().getName().toUpperCase() in [
123+
"ENCRYPT_MODE", "DECRYPT_MODE", "WRAP_MODE", "UNWRAP_MODE"
124+
]
120125
}
121126
}
122127

128+
class CipherUpdateCall extends MethodCall {
129+
CipherUpdateCall() { this.getMethod().hasQualifiedName("javax.crypto", "Cipher", "update") }
130+
131+
DataFlow::Node getInputData() { result.asExpr() = this.getArgument(0) }
132+
}
133+
123134
private newtype TCipherModeFlowState =
124135
TUninitializedCipherModeFlowState() or
125-
TInitializedCipherModeFlowState(CipherInitCall call)
136+
TInitializedCipherModeFlowState(CipherInitCall call) or
137+
TUsedCipherModeFlowState(CipherInitCall init, CipherUpdateCall update)
126138

127139
abstract private class CipherModeFlowState extends TCipherModeFlowState {
128140
string toString() {
@@ -131,13 +143,13 @@ module JCAModel {
131143
this = TInitializedCipherModeFlowState(_) and result = "initialized"
132144
}
133145

134-
abstract Crypto::CipherOperationMode getCipherOperationMode();
146+
abstract Crypto::CipherOperationSubtype getCipherOperationMode();
135147
}
136148

137149
private class UninitializedCipherModeFlowState extends CipherModeFlowState,
138150
TUninitializedCipherModeFlowState
139151
{
140-
override Crypto::CipherOperationMode getCipherOperationMode() {
152+
override Crypto::CipherOperationSubtype getCipherOperationMode() {
141153
result instanceof Crypto::UnknownCipherOperationMode
142154
}
143155
}
@@ -148,19 +160,18 @@ module JCAModel {
148160
CipherInitCall call;
149161
DataFlow::Node node1;
150162
DataFlow::Node node2;
151-
Crypto::CipherOperationMode mode;
163+
Crypto::CipherOperationSubtype mode;
152164

153165
InitializedCipherModeFlowState() {
154166
this = TInitializedCipherModeFlowState(call) and
155167
DataFlow::localFlowStep(node1, node2) and
156168
node2.asExpr() = call.getQualifier() and
157-
// I would imagine this would make this predicate horribly horribly inefficient
158-
// it now binds with anything
169+
// TODO: does this make this predicate inefficient as it binds with anything?
159170
not node1.asExpr() = call.getQualifier() and
160171
mode = call.getCipherOperationModeType()
161172
}
162173

163-
CipherInitCall getCall() { result = call }
174+
CipherInitCall getInitCall() { result = call }
164175

165176
DataFlow::Node getFstNode() { result = node1 }
166177

@@ -169,12 +180,14 @@ module JCAModel {
169180
*/
170181
DataFlow::Node getSndNode() { result = node2 }
171182

172-
override Crypto::CipherOperationMode getCipherOperationMode() { result = mode }
183+
override Crypto::CipherOperationSubtype getCipherOperationMode() { result = mode }
173184
}
174185

175186
/**
176-
* Trace to a cryptographic operation,
187+
* Trace from cipher initialization to a cryptographic operation,
177188
* specifically `Cipher.doFinal()`, `Cipher.wrap()`, or `Cipher.unwrap()`.
189+
*
190+
* TODO: handle `Cipher.update()`
178191
*/
179192
private module CipherGetInstanceToCipherOperationConfig implements DataFlow::StateConfigSig {
180193
class FlowState = TCipherModeFlowState;
@@ -201,23 +214,24 @@ module JCAModel {
201214
exists(CipherInitCall call | node.asExpr() = call.getQualifier() |
202215
state instanceof UninitializedCipherModeFlowState
203216
or
204-
state.(InitializedCipherModeFlowState).getCall() != call
217+
state.(InitializedCipherModeFlowState).getInitCall() != call
205218
)
206219
}
207220
}
208221

209222
module CipherGetInstanceToCipherOperationFlow =
210223
DataFlow::GlobalWithState<CipherGetInstanceToCipherOperationConfig>;
211224

212-
class CipherEncryptionOperation extends Crypto::CipherOperationInstance instanceof Call {
213-
Crypto::CipherOperationMode mode;
214-
Crypto::EncryptionAlgorithmInstance algorithm;
225+
class CipherOperationInstance extends Crypto::CipherOperationInstance instanceof Call {
226+
Crypto::CipherOperationSubtype mode;
227+
Crypto::CipherAlgorithmInstance algorithm;
228+
CipherGetInstanceToCipherOperationFlow::PathNode sink;
229+
JCACipherOperationCall doFinalize;
215230

216-
CipherEncryptionOperation() {
231+
CipherOperationInstance() {
217232
exists(
218-
CipherGetInstanceToCipherOperationFlow::PathNode sink,
219233
CipherGetInstanceToCipherOperationFlow::PathNode src, CipherGetInstanceCall getCipher,
220-
JCACipherOperationCall doFinalize, CipherGetInstanceAlgorithmArg arg
234+
CipherGetInstanceAlgorithmArg arg
221235
|
222236
CipherGetInstanceToCipherOperationFlow::flowPath(src, sink) and
223237
src.getNode().asExpr() = getCipher and
@@ -229,9 +243,19 @@ module JCAModel {
229243
)
230244
}
231245

232-
override Crypto::EncryptionAlgorithmInstance getAlgorithm() { result = algorithm }
246+
override Crypto::CipherAlgorithmInstance getAlgorithm() { result = algorithm }
233247

234-
override Crypto::CipherOperationMode getCipherOperationMode() { result = mode }
248+
override Crypto::CipherOperationSubtype getCipherOperationSubtype() { result = mode }
249+
250+
override Crypto::NonceArtifactInstance getNonce() {
251+
NonceArtifactToCipherInitCallFlow::flow(result.asOutputData(),
252+
DataFlow::exprNode(sink.getState()
253+
.(InitializedCipherModeFlowState)
254+
.getInitCall()
255+
.getNonceArg()))
256+
}
257+
258+
override DataFlow::Node getInputData() { result = doFinalize.getInputData() }
235259
}
236260

237261
/**
@@ -319,12 +343,12 @@ module JCAModel {
319343
CipherStringLiteral getInstance() { result = instance }
320344
}
321345

322-
class EncryptionAlgorithm extends Crypto::EncryptionAlgorithm {
346+
class EncryptionAlgorithm extends Crypto::CipherAlgorithm {
323347
CipherStringLiteral origin;
324348
CipherGetInstanceAlgorithmArg instance;
325349

326350
EncryptionAlgorithm() {
327-
this = Crypto::TEncryptionAlgorithm(instance) and
351+
this = Crypto::TCipherAlgorithm(instance) and
328352
instance.getOrigin() = origin
329353
}
330354

@@ -347,7 +371,7 @@ module JCAModel {
347371
override Crypto::TCipherType getCipherFamily() {
348372
if this.cipherNameMappingKnown(_, origin.getAlgorithmName())
349373
then this.cipherNameMappingKnown(result, origin.getAlgorithmName())
350-
else result instanceof Crypto::OtherSymmetricCipherType
374+
else result instanceof Crypto::OtherCipherType
351375
}
352376

353377
override string getKeySize(Location location) { none() }
@@ -384,33 +408,71 @@ module JCAModel {
384408
}
385409

386410
/**
387-
* Initialiation vectors
411+
* Initialization vectors and other nonce artifacts
388412
*/
389-
abstract class IVParameterInstantiation extends Crypto::InitializationVectorArtifactInstance instanceof ClassInstanceExpr
413+
abstract class NonceParameterInstantiation extends Crypto::NonceArtifactInstance instanceof ClassInstanceExpr
390414
{
391-
abstract Expr getInput();
415+
override DataFlow::Node asOutputData() { result.asExpr() = this }
392416
}
393417

394-
class IvParameterSpecInstance extends IVParameterInstantiation {
418+
class IvParameterSpecInstance extends NonceParameterInstantiation {
395419
IvParameterSpecInstance() {
396420
this.(ClassInstanceExpr)
397421
.getConstructedType()
398422
.hasQualifiedName("javax.crypto.spec", "IvParameterSpec")
399423
}
400424

401-
override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(0) }
425+
override DataFlow::Node getInput() { result.asExpr() = this.(ClassInstanceExpr).getArgument(0) }
402426
}
403427

404-
class GCMParameterSpecInstance extends IVParameterInstantiation {
428+
// TODO: this also specifies the tag length for GCM
429+
class GCMParameterSpecInstance extends NonceParameterInstantiation {
405430
GCMParameterSpecInstance() {
406431
this.(ClassInstanceExpr)
407432
.getConstructedType()
408433
.hasQualifiedName("javax.crypto.spec", "GCMParameterSpec")
409434
}
410435

411-
override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(1) }
436+
override DataFlow::Node getInput() { result.asExpr() = this.(ClassInstanceExpr).getArgument(1) }
437+
}
438+
439+
class IvParameterSpecGetIvCall extends MethodCall {
440+
IvParameterSpecGetIvCall() {
441+
this.getMethod().hasQualifiedName("javax.crypto.spec", "IvParameterSpec", "getIV")
442+
}
412443
}
413444

445+
module NonceArtifactToCipherInitCallConfig implements DataFlow::ConfigSig {
446+
predicate isSource(DataFlow::Node src) {
447+
exists(NonceParameterInstantiation n |
448+
src = n.asOutputData() and
449+
not exists(IvParameterSpecGetIvCall m | n.getInput().asExpr() = m)
450+
)
451+
}
452+
453+
predicate isSink(DataFlow::Node sink) {
454+
exists(CipherInitCall c | c.getNonceArg() = sink.asExpr())
455+
}
456+
457+
predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
458+
exists(IvParameterSpecGetIvCall m |
459+
node1.asExpr() = m.getQualifier() and
460+
node2.asExpr() = m
461+
)
462+
or
463+
exists(NonceParameterInstantiation n |
464+
node1 = n.getInput() and
465+
node2.asExpr() = n
466+
)
467+
}
468+
}
469+
470+
module NonceArtifactToCipherInitCallFlow = DataFlow::Global<NonceArtifactToCipherInitCallConfig>;
471+
472+
/**
473+
* A data-flow configuration to track flow from a mode field access to
474+
* the mode argument of the `init` method of the `javax.crypto.Cipher` class.
475+
*/
414476
private module JavaxCipherModeAccessToInitConfig implements DataFlow::ConfigSig {
415477
predicate isSource(DataFlow::Node src) {
416478
src.asExpr() instanceof JavaxCryptoCipherOperationModeAccess
@@ -423,6 +485,18 @@ module JCAModel {
423485

424486
module JavaxCipherModeAccessToInitFlow = DataFlow::Global<JavaxCipherModeAccessToInitConfig>;
425487

488+
private predicate cipher_mode_str_to_cipher_mode_known(
489+
string mode, Crypto::CipherOperationSubtype cipher_mode
490+
) {
491+
mode = "ENCRYPT_MODE" and cipher_mode instanceof Crypto::EncryptionMode
492+
or
493+
mode = "WRAP_MODE" and cipher_mode instanceof Crypto::WrapMode
494+
or
495+
mode = "DECRYPT_MODE" and cipher_mode instanceof Crypto::DecryptionMode
496+
or
497+
mode = "UNWRAP_MODE" and cipher_mode instanceof Crypto::UnwrapMode
498+
}
499+
426500
class CipherInitCall extends MethodCall {
427501
CipherInitCall() { this.getCallee().hasQualifiedName("javax.crypto", "Cipher", "init") }
428502

@@ -443,49 +517,19 @@ module JCAModel {
443517
)
444518
}
445519

446-
Crypto::CipherOperationMode getCipherOperationModeType() {
447-
if not exists(this.getModeOrigin())
448-
then result instanceof Crypto::UnknownCipherOperationMode
449-
else
450-
if this.getModeOrigin().getField().getName() in ["ENCRYPT_MODE", "WRAP_MODE"]
451-
then result instanceof Crypto::EncryptionMode
452-
else
453-
if this.getModeOrigin().getField().getName() in ["DECRYPT_MODE", "UNWRAP_MODE"]
454-
then result instanceof Crypto::DecryptionMode
455-
else
456-
// TODO/Question: distinguish between unknown vs unspecified? (the field access is not recognized, vs no field access is found)
457-
result instanceof Crypto::UnknownCipherOperationMode
520+
Crypto::CipherOperationSubtype getCipherOperationModeType() {
521+
if cipher_mode_str_to_cipher_mode_known(this.getModeOrigin().getField().getName(), _)
522+
then cipher_mode_str_to_cipher_mode_known(this.getModeOrigin().getField().getName(), result)
523+
else result instanceof Crypto::UnknownCipherOperationMode
458524
}
459525

460-
Expr getKey() {
526+
Expr getKeyArg() {
461527
result = this.getArgument(1) and this.getMethod().getParameterType(1).hasName("Key")
462528
}
463529

464-
Expr getIV() {
530+
Expr getNonceArg() {
465531
result = this.getArgument(2) and
466532
this.getMethod().getParameterType(2).hasName("AlgorithmParameterSpec")
467533
}
468534
}
469-
470-
// TODO: cipher.getParameters().getParameterSpec(GCMParameterSpec.class);
471-
/*
472-
* class InitializationVectorArg extends Crypto::InitializationVectorArtifactInstance instanceof Expr
473-
* {
474-
* IVParameterInstantiation creation;
475-
*
476-
* InitializationVectorArg() { this = creation.getInput() }
477-
* }
478-
*/
479-
480-
class InitializationVector extends Crypto::InitializationVector {
481-
IVParameterInstantiation instance;
482-
483-
InitializationVector() { this = Crypto::TInitializationVector(instance) }
484-
485-
override Location getLocation() { result = instance.getLocation() }
486-
487-
override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance }
488-
489-
override Crypto::DataFlowNode getInputData() { result.asExpr() = instance.getInput() }
490-
}
491535
}

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

Lines changed: 1 addition & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ module CryptoInput implements InputSig<Language::Location> {
2323
class LocatableElement = Language::Element;
2424

2525
class UnknownLocation = UnknownDefaultLocation;
26-
27-
predicate rngToIvFlow(DataFlowNode rng, DataFlowNode iv) { none() }
2826
}
2927

3028
/**
@@ -37,9 +35,7 @@ module Crypto = CryptographyBase<Language::Location, CryptoInput>;
3735
* tied to an output node (i.e., the result of the source of randomness)
3836
*/
3937
abstract class RandomnessInstance extends Crypto::RandomNumberGenerationInstance {
40-
abstract Crypto::RNGSourceSecurity getSourceSecurity();
41-
42-
Crypto::TRNGSeedSecurity getSeedSecurity(Location location) { none() }
38+
override DataFlow::Node asOutputData() { result.asExpr() = this }
4339
}
4440

4541
class SecureRandomnessInstance extends RandomnessInstance {
@@ -48,36 +44,10 @@ class SecureRandomnessInstance extends RandomnessInstance {
4844
s.getSourceOfRandomness() instanceof SecureRandomNumberGenerator
4945
)
5046
}
51-
52-
override Crypto::RNGSourceSecurity getSourceSecurity() {
53-
result instanceof Crypto::RNGSourceSecure
54-
}
5547
}
5648

5749
class InsecureRandomnessInstance extends RandomnessInstance {
5850
InsecureRandomnessInstance() { exists(InsecureRandomnessSource node | this = node.asExpr()) }
59-
60-
override Crypto::RNGSourceSecurity getSourceSecurity() {
61-
result instanceof Crypto::RNGSourceInsecure
62-
}
63-
}
64-
65-
class RandomnessArtifact extends Crypto::RandomNumberGeneration {
66-
RandomnessInstance instance;
67-
68-
RandomnessArtifact() { this = Crypto::TRandomNumberGeneration(instance) }
69-
70-
override Location getLocation() { result = instance.getLocation() }
71-
72-
override Crypto::RNGSourceSecurity getSourceSecurity() { result = instance.getSourceSecurity() }
73-
74-
override Crypto::TRNGSeedSecurity getSeedSecurity(Location location) {
75-
result = instance.getSeedSecurity(location)
76-
}
77-
78-
override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance }
79-
80-
override Crypto::DataFlowNode getInputData() { none() }
8151
}
8252

8353
// Import library-specific modeling

0 commit comments

Comments
 (0)