Skip to content

Commit ad54c9d

Browse files
Two queries for timing attacks
1 parent e3b6cea commit ad54c9d

16 files changed

+569
-391
lines changed

java/ql/src/experimental/Security/CWE/CWE-208/NonConstantTimeCheckOnSignature.qhelp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
<p>
66
A constant-time algorithm should be used for checking a MAC or a digital signature.
77
In other words, the comparison time should not depend on the content of the input.
8-
Otherwise, attackers may be able to implement a timing attack if they control inputs.
9-
A successful attack may uncover a valid MAC or signature that in turn can result in authentication bypass.
8+
Otherwise, an attacker may be able to implement a timing attack.
9+
A successful attack may uncover a valid signature that in turn can result in authentication bypass.
1010
</p>
1111
</overview>
1212

@@ -20,13 +20,13 @@ and does not depend on the contents of the arrays.
2020

2121
<example>
2222
<p>
23-
The following example uses <code>Arrays.equals()</code> method for comparing MAC.
23+
The following example uses <code>Arrays.equals()</code> method for validating a MAC.
2424
This method implements a non-constant-time algorithm:
2525
</p>
2626
<sample src="UnsafeMacComparison.java" />
2727

2828
<p>
29-
The next example uses a safe constant-time algorithm for comparing MAC:
29+
The next example uses a safe constant-time algorithm for validating a MAC:
3030
</p>
3131
<sample src="SafeMacComparison.java" />
3232

Lines changed: 9 additions & 330 deletions
Original file line numberDiff line numberDiff line change
@@ -1,343 +1,22 @@
11
/**
2-
* @name Using a non-constant-time algorithm for comparing MAC or signature
3-
* @description When checking MAC or signature, a constant-time algorithm should be used.
4-
* Otherwise, attackers may be able to implement a timing attack if they control inputs.
5-
* A successful attack may uncover a valid MAC or signature that in turn can result in authentication bypass.
2+
* @name Using a non-constant-time algorithm for checking a signature
3+
* @description When checking a signature, a constant-time algorithm should be used.
4+
* Otherwise, an attacker may be able to implement a timing attack.
5+
* A successful attack may uncover a valid signature
6+
* that in turn can result in authentication bypass.
67
* @kind path-problem
78
* @problem.severity warning
8-
* @precision high
9+
* @precision medium
910
* @id java/non-constant-time-in-signature-check
1011
* @tags security
1112
* external/cwe/cwe-208
1213
*/
1314

1415
import java
15-
import semmle.code.java.controlflow.Guards
16-
import semmle.code.java.dataflow.TaintTracking
17-
import semmle.code.java.dataflow.TaintTracking2
18-
import semmle.code.java.dataflow.DataFlow3
19-
import semmle.code.java.dataflow.FlowSources
16+
import NonConstantTimeCheckOnSignatureQuery
2017
import DataFlow::PathGraph
2118

22-
/** A method call that produces cryptographic result. */
23-
abstract private class ProduceCryptoCall extends MethodAccess {
24-
Expr output;
25-
26-
/** Return the result of cryptographic operation. */
27-
Expr output() { result = output }
28-
29-
/** Return a type of the result of cryptographic operation such as MAC, signature or ciphertext. */
30-
abstract string getResultType();
31-
}
32-
33-
/** A method call that produces a MAC. */
34-
private class ProduceMacCall extends ProduceCryptoCall {
35-
ProduceMacCall() {
36-
getMethod().getDeclaringType().hasQualifiedName("javax.crypto", "Mac") and
37-
(
38-
getMethod().hasStringSignature(["doFinal()", "doFinal(byte[])"]) and this = output
39-
or
40-
getMethod().hasStringSignature("doFinal(byte[], int)") and getArgument(0) = output
41-
)
42-
}
43-
44-
override string getResultType() { result = "MAC" }
45-
}
46-
47-
/** A method call that produces a signature. */
48-
private class ProduceSignatureCall extends ProduceCryptoCall {
49-
ProduceSignatureCall() {
50-
getMethod().getDeclaringType().hasQualifiedName("java.security", "Signature") and
51-
(
52-
getMethod().hasStringSignature("sign()") and this = output
53-
or
54-
getMethod().hasStringSignature("sign(byte[], int, int)") and getArgument(0) = output
55-
)
56-
}
57-
58-
override string getResultType() { result = "signature" }
59-
}
60-
61-
/**
62-
* A config that tracks data flow from initializing a cipher for encryption
63-
* to producing a ciphertext using this cipher.
64-
*/
65-
private class InitializeEncryptorConfig extends DataFlow3::Configuration {
66-
InitializeEncryptorConfig() { this = "InitializeEncryptorConfig" }
67-
68-
override predicate isSource(DataFlow::Node source) {
69-
exists(MethodAccess ma |
70-
ma.getMethod().hasQualifiedName("javax.crypto", "Cipher", "init") and
71-
ma.getArgument(0).(VarAccess).getVariable().hasName("ENCRYPT_MODE") and
72-
ma.getQualifier() = source.asExpr()
73-
)
74-
}
75-
76-
override predicate isSink(DataFlow::Node sink) {
77-
exists(MethodAccess ma |
78-
ma.getMethod().hasQualifiedName("javax.crypto", "Cipher", "doFinal") and
79-
ma.getQualifier() = sink.asExpr()
80-
)
81-
}
82-
}
83-
84-
/** A method call that produces a ciphertext. */
85-
private class ProduceCiphertextCall extends ProduceCryptoCall {
86-
ProduceCiphertextCall() {
87-
exists(Method m | m = this.getMethod() |
88-
m.getDeclaringType().hasQualifiedName("javax.crypto", "Cipher") and
89-
(
90-
m.hasStringSignature(["doFinal()", "doFinal(byte[])", "doFinal(byte[], int, int)"]) and
91-
this = output
92-
or
93-
m.hasStringSignature("doFinal(byte[], int)") and getArgument(0) = output
94-
or
95-
m.hasStringSignature([
96-
"doFinal(byte[], int, int, byte[])", "doFinal(byte[], int, int, byte[], int)"
97-
]) and
98-
getArgument(3) = output
99-
or
100-
m.hasStringSignature("doFinal(ByteBuffer, ByteBuffer)") and
101-
getArgument(1) = output
102-
)
103-
) and
104-
exists(InitializeEncryptorConfig config |
105-
config.hasFlowTo(DataFlow3::exprNode(this.getQualifier()))
106-
)
107-
}
108-
109-
override string getResultType() { result = "ciphertext" }
110-
}
111-
112-
/** Holds if `fromNode` to `toNode` is a dataflow step that updates a cryptographic operation. */
113-
private predicate updateCryptoOperationStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
114-
exists(MethodAccess call, Method m |
115-
m = call.getMethod() and
116-
call.getQualifier() = toNode.asExpr() and
117-
call.getArgument(0) = fromNode.asExpr()
118-
|
119-
m.hasQualifiedName("java.security", "Signature", "update")
120-
or
121-
m.hasQualifiedName("javax.crypto", ["Mac", "Cipher"], "update")
122-
or
123-
m.hasQualifiedName("javax.crypto", ["Mac", "Cipher"], "doFinal") and
124-
not m.hasStringSignature("doFinal(byte[], int)")
125-
)
126-
}
127-
128-
/** Holds if `fromNode` to `toNode` is a dataflow step that creates a hash. */
129-
private predicate createMessageDigestStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
130-
exists(MethodAccess ma, Method m | m = ma.getMethod() |
131-
m.getDeclaringType().hasQualifiedName("java.security", "MessageDigest") and
132-
m.hasStringSignature("digest()") and
133-
ma.getQualifier() = fromNode.asExpr() and
134-
ma = toNode.asExpr()
135-
)
136-
or
137-
exists(MethodAccess ma, Method m | m = ma.getMethod() |
138-
m.getDeclaringType().hasQualifiedName("java.security", "MessageDigest") and
139-
m.hasStringSignature("digest(byte[], int, int)") and
140-
ma.getQualifier() = fromNode.asExpr() and
141-
ma.getArgument(0) = toNode.asExpr()
142-
)
143-
or
144-
exists(MethodAccess ma, Method m | m = ma.getMethod() |
145-
m.getDeclaringType().hasQualifiedName("java.security", "MessageDigest") and
146-
m.hasStringSignature("digest(byte[])") and
147-
ma.getArgument(0) = fromNode.asExpr() and
148-
ma = toNode.asExpr()
149-
)
150-
}
151-
152-
/** Holds if `fromNode` to `toNode` is a dataflow step that updates a hash. */
153-
private predicate updateMessageDigestStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
154-
exists(MethodAccess ma, Method m | m = ma.getMethod() |
155-
m.hasQualifiedName("java.security", "MessageDigest", "update") and
156-
ma.getArgument(0) = fromNode.asExpr() and
157-
ma.getQualifier() = toNode.asExpr()
158-
)
159-
}
160-
161-
/**
162-
* A config that tracks data flow from remote user input to a cryptographic operation
163-
* such as cipher, MAC or signature.
164-
*/
165-
private class UserInputInCryptoOperationConfig extends TaintTracking2::Configuration {
166-
UserInputInCryptoOperationConfig() { this = "UserInputInCryptoOperationConfig" }
167-
168-
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
169-
170-
override predicate isSink(DataFlow::Node sink) {
171-
exists(ProduceCryptoCall call | call.getQualifier() = sink.asExpr())
172-
}
173-
174-
override predicate isAdditionalTaintStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
175-
updateCryptoOperationStep(fromNode, toNode)
176-
or
177-
createMessageDigestStep(fromNode, toNode)
178-
or
179-
updateMessageDigestStep(fromNode, toNode)
180-
}
181-
}
182-
183-
/** A source that produces result of cryptographic operation. */
184-
private class CryptoOperationSource extends DataFlow::Node {
185-
ProduceCryptoCall call;
186-
187-
CryptoOperationSource() { call.output() = this.asExpr() }
188-
189-
/** Holds if remote user input was used in the cryptographic operation. */
190-
predicate includesUserInput() {
191-
exists(
192-
DataFlow2::PathNode source, DataFlow2::PathNode sink, UserInputInCryptoOperationConfig config
193-
|
194-
config.hasFlowPath(source, sink)
195-
|
196-
sink.getNode().asExpr() = call.getQualifier()
197-
)
198-
}
199-
200-
ProduceCryptoCall getCall() { result = call }
201-
}
202-
203-
/** Methods that use a non-constant-time algorithm for comparing inputs. */
204-
private class NonConstantTimeEqualsCall extends MethodAccess {
205-
NonConstantTimeEqualsCall() {
206-
getMethod()
207-
.hasQualifiedName("java.lang", "String", ["equals", "contentEquals", "equalsIgnoreCase"]) or
208-
getMethod().hasQualifiedName("java.nio", "ByteBuffer", ["equals", "compareTo"])
209-
}
210-
}
211-
212-
/** Static methods that use a non-constant-time algorithm for comparing inputs. */
213-
private class NonConstantTimeComparisonCall extends StaticMethodAccess {
214-
NonConstantTimeComparisonCall() {
215-
getMethod().hasQualifiedName("java.util", "Arrays", ["equals", "deepEquals"]) or
216-
getMethod().hasQualifiedName("java.util", "Objects", "deepEquals") or
217-
getMethod()
218-
.hasQualifiedName("org.apache.commons.lang3", "StringUtils",
219-
["equals", "equalsAny", "equalsAnyIgnoreCase", "equalsIgnoreCase"])
220-
}
221-
}
222-
223-
/**
224-
* A config that tracks data flow from remote user input to methods
225-
* that compare inputs using a non-constant-time algorithm.
226-
*/
227-
private class UserInputInComparisonConfig extends TaintTracking2::Configuration {
228-
UserInputInComparisonConfig() { this = "UserInputInComparisonConfig" }
229-
230-
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
231-
232-
override predicate isSink(DataFlow::Node sink) {
233-
exists(NonConstantTimeEqualsCall call |
234-
sink.asExpr() = [call.getAnArgument(), call.getQualifier()]
235-
)
236-
or
237-
exists(NonConstantTimeComparisonCall call | sink.asExpr() = call.getAnArgument())
238-
}
239-
}
240-
241-
/** Holds if `expr` looks like a constant. */
242-
private predicate looksLikeConstant(Expr expr) {
243-
expr.isCompileTimeConstant()
244-
or
245-
expr.(VarAccess).getVariable().isFinal() and expr.getType() instanceof TypeString
246-
}
247-
248-
/**
249-
* Holds if `firstObject` and `secondObject` are compared using a method
250-
* that does not use a constant-time algorithm, for example, `String.equals()`.
251-
*/
252-
private predicate isNonConstantEqualsCall(Expr firstObject, Expr secondObject) {
253-
exists(NonConstantTimeEqualsCall call |
254-
firstObject = call.getQualifier() and
255-
secondObject = call.getAnArgument()
256-
or
257-
firstObject = call.getAnArgument() and
258-
secondObject = call.getQualifier()
259-
)
260-
}
261-
262-
/**
263-
* Holds if `firstInput` and `secondInput` are compared using a static method
264-
* that does not use a constant-time algorithm, for example, `Arrays.equals()`.
265-
*/
266-
private predicate isNonConstantTimeComparisonCall(Expr firstInput, Expr secondInput) {
267-
exists(NonConstantTimeComparisonCall call |
268-
firstInput = call.getArgument(0) and secondInput = call.getArgument(1)
269-
or
270-
firstInput = call.getArgument(1) and secondInput = call.getArgument(0)
271-
)
272-
}
273-
274-
/**
275-
* Holds if there is a fast-fail check while comparing `firstArray` and `secondArray`.
276-
*/
277-
private predicate existsFailFastCheck(Expr firstArray, Expr secondArray) {
278-
exists(
279-
Guard guard, EqualityTest eqTest, boolean branch, Stmt fastFailingStmt,
280-
ArrayAccess firstArrayAccess, ArrayAccess secondArrayAccess
281-
|
282-
guard = eqTest and
283-
// For `==` false branch is fail fast; for `!=` true branch is fail fast
284-
branch = eqTest.polarity().booleanNot() and
285-
(
286-
fastFailingStmt instanceof ReturnStmt or
287-
fastFailingStmt instanceof BreakStmt or
288-
fastFailingStmt instanceof ThrowStmt
289-
) and
290-
guard.controls(fastFailingStmt.getBasicBlock(), branch) and
291-
DataFlow::localExprFlow(firstArrayAccess, eqTest.getLeftOperand()) and
292-
DataFlow::localExprFlow(secondArrayAccess, eqTest.getRightOperand())
293-
|
294-
firstArrayAccess.getArray() = firstArray and secondArray = secondArrayAccess
295-
or
296-
secondArrayAccess.getArray() = firstArray and secondArray = firstArrayAccess
297-
)
298-
}
299-
300-
/** A sink that compares input using a non-constant-time algorithm. */
301-
private class NonConstantTimeComparisonSink extends DataFlow::Node {
302-
Expr anotherParameter;
303-
304-
NonConstantTimeComparisonSink() {
305-
(
306-
isNonConstantEqualsCall(this.asExpr(), anotherParameter)
307-
or
308-
isNonConstantTimeComparisonCall(this.asExpr(), anotherParameter)
309-
or
310-
existsFailFastCheck(this.asExpr(), anotherParameter)
311-
) and
312-
not looksLikeConstant(anotherParameter)
313-
}
314-
315-
/** Holds if remote user input was used in the comparison. */
316-
predicate includesUserInput() {
317-
exists(UserInputInComparisonConfig config |
318-
config.hasFlowTo(DataFlow2::exprNode(anotherParameter))
319-
)
320-
}
321-
}
322-
323-
/**
324-
* A configuration that tracks data flow from cryptographic operations
325-
* to methods that compare data using a non-constant-time algorithm.
326-
*/
327-
private class NonConstantTimeCryptoComparisonConfig extends TaintTracking::Configuration {
328-
NonConstantTimeCryptoComparisonConfig() { this = "NonConstantTimeCryptoComparisonConfig" }
329-
330-
override predicate isSource(DataFlow::Node source) { source instanceof CryptoOperationSource }
331-
332-
override predicate isSink(DataFlow::Node sink) { sink instanceof NonConstantTimeComparisonSink }
333-
}
334-
33519
from DataFlow::PathNode source, DataFlow::PathNode sink, NonConstantTimeCryptoComparisonConfig conf
336-
where
337-
conf.hasFlowPath(source, sink) and
338-
(
339-
source.getNode().(CryptoOperationSource).includesUserInput() and
340-
sink.getNode().(NonConstantTimeComparisonSink).includesUserInput()
341-
)
342-
select sink.getNode(), source, sink, "Using a non-constant-time method for cheching a $@.", source,
20+
where conf.hasFlowPath(source, sink)
21+
select sink.getNode(), source, sink, "Using a non-constant-time method for checking a $@.", source,
34322
source.getNode().(CryptoOperationSource).getCall().getResultType()

0 commit comments

Comments
 (0)