Merge pull request #6006 from artem-smotrakov/timing-attacks

Java: Timing attacks while comparing results of cryptographic operations
This commit is contained in:
Chris Smowton
2021-08-09 15:30:47 +01:00
committed by GitHub
15 changed files with 814 additions and 0 deletions

View File

@@ -0,0 +1,323 @@
/**
* Provides classes and predicates for queries that detect timing attacks.
*/
import semmle.code.java.controlflow.Guards
import semmle.code.java.dataflow.TaintTracking
import semmle.code.java.dataflow.TaintTracking2
import semmle.code.java.dataflow.DataFlow3
import semmle.code.java.dataflow.FlowSources
/** A method call that produces cryptographic result. */
abstract private class ProduceCryptoCall extends MethodAccess {
Expr output;
/** Gets the result of cryptographic operation. */
Expr output() { result = output }
/** Gets a type of cryptographic operation such as MAC, signature or ciphertext. */
abstract string getResultType();
}
/** A method call that produces a MAC. */
private class ProduceMacCall extends ProduceCryptoCall {
ProduceMacCall() {
getMethod().getDeclaringType().hasQualifiedName("javax.crypto", "Mac") and
(
getMethod().hasStringSignature(["doFinal()", "doFinal(byte[])"]) and this = output
or
getMethod().hasStringSignature("doFinal(byte[], int)") and getArgument(0) = output
)
}
override string getResultType() { result = "MAC" }
}
/** A method call that produces a signature. */
private class ProduceSignatureCall extends ProduceCryptoCall {
ProduceSignatureCall() {
getMethod().getDeclaringType().hasQualifiedName("java.security", "Signature") and
(
getMethod().hasStringSignature("sign()") and this = output
or
getMethod().hasStringSignature("sign(byte[], int, int)") and getArgument(0) = output
)
}
override string getResultType() { result = "signature" }
}
/**
* A config that tracks data flow from initializing a cipher for encryption
* to producing a ciphertext using this cipher.
*/
private class InitializeEncryptorConfig extends DataFlow3::Configuration {
InitializeEncryptorConfig() { this = "InitializeEncryptorConfig" }
override predicate isSource(DataFlow::Node source) {
exists(MethodAccess ma |
ma.getMethod().hasQualifiedName("javax.crypto", "Cipher", "init") and
ma.getArgument(0).(VarAccess).getVariable().hasName("ENCRYPT_MODE") and
ma.getQualifier() = source.asExpr()
)
}
override predicate isSink(DataFlow::Node sink) {
exists(MethodAccess ma |
ma.getMethod().hasQualifiedName("javax.crypto", "Cipher", "doFinal") and
ma.getQualifier() = sink.asExpr()
)
}
}
/** A method call that produces a ciphertext. */
private class ProduceCiphertextCall extends ProduceCryptoCall {
ProduceCiphertextCall() {
exists(Method m | m = this.getMethod() |
m.getDeclaringType().hasQualifiedName("javax.crypto", "Cipher") and
(
m.hasStringSignature(["doFinal()", "doFinal(byte[])", "doFinal(byte[], int, int)"]) and
this = output
or
m.hasStringSignature("doFinal(byte[], int)") and getArgument(0) = output
or
m.hasStringSignature([
"doFinal(byte[], int, int, byte[])", "doFinal(byte[], int, int, byte[], int)"
]) and
getArgument(3) = output
or
m.hasStringSignature("doFinal(ByteBuffer, ByteBuffer)") and
getArgument(1) = output
)
) and
exists(InitializeEncryptorConfig config |
config.hasFlowTo(DataFlow3::exprNode(this.getQualifier()))
)
}
override string getResultType() { result = "ciphertext" }
}
/** Holds if `fromNode` to `toNode` is a dataflow step that updates a cryptographic operation. */
private predicate updateCryptoOperationStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
exists(MethodAccess call, Method m |
m = call.getMethod() and
call.getQualifier() = toNode.asExpr() and
call.getArgument(0) = fromNode.asExpr()
|
m.hasQualifiedName("java.security", "Signature", "update")
or
m.hasQualifiedName("javax.crypto", ["Mac", "Cipher"], "update")
or
m.hasQualifiedName("javax.crypto", ["Mac", "Cipher"], "doFinal") and
not m.hasStringSignature("doFinal(byte[], int)")
)
}
/** Holds if `fromNode` to `toNode` is a dataflow step that creates a hash. */
private predicate createMessageDigestStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
exists(MethodAccess ma, Method m | m = ma.getMethod() |
m.getDeclaringType().hasQualifiedName("java.security", "MessageDigest") and
m.hasStringSignature("digest()") and
ma.getQualifier() = fromNode.asExpr() and
ma = toNode.asExpr()
)
or
exists(MethodAccess ma, Method m | m = ma.getMethod() |
m.getDeclaringType().hasQualifiedName("java.security", "MessageDigest") and
m.hasStringSignature("digest(byte[], int, int)") and
ma.getQualifier() = fromNode.asExpr() and
ma.getArgument(0) = toNode.asExpr()
)
or
exists(MethodAccess ma, Method m | m = ma.getMethod() |
m.getDeclaringType().hasQualifiedName("java.security", "MessageDigest") and
m.hasStringSignature("digest(byte[])") and
ma.getArgument(0) = fromNode.asExpr() and
ma = toNode.asExpr()
)
}
/** Holds if `fromNode` to `toNode` is a dataflow step that updates a hash. */
private predicate updateMessageDigestStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
exists(MethodAccess ma, Method m | m = ma.getMethod() |
m.hasQualifiedName("java.security", "MessageDigest", "update") and
ma.getArgument(0) = fromNode.asExpr() and
ma.getQualifier() = toNode.asExpr()
)
}
/**
* A config that tracks data flow from remote user input to a cryptographic operation
* such as cipher, MAC or signature.
*/
private class UserInputInCryptoOperationConfig extends TaintTracking2::Configuration {
UserInputInCryptoOperationConfig() { this = "UserInputInCryptoOperationConfig" }
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
override predicate isSink(DataFlow::Node sink) {
exists(ProduceCryptoCall call | call.getQualifier() = sink.asExpr())
}
override predicate isAdditionalTaintStep(DataFlow2::Node fromNode, DataFlow2::Node toNode) {
updateCryptoOperationStep(fromNode, toNode)
or
createMessageDigestStep(fromNode, toNode)
or
updateMessageDigestStep(fromNode, toNode)
}
}
/** A source that produces result of cryptographic operation. */
class CryptoOperationSource extends DataFlow::Node {
ProduceCryptoCall call;
CryptoOperationSource() { call.output() = this.asExpr() }
/** Holds if remote user input was used in the cryptographic operation. */
predicate includesUserInput() {
exists(
DataFlow2::PathNode source, DataFlow2::PathNode sink, UserInputInCryptoOperationConfig config
|
config.hasFlowPath(source, sink)
|
sink.getNode().asExpr() = call.getQualifier()
)
}
/** Gets a method call that produces cryptographic result. */
ProduceCryptoCall getCall() { result = call }
}
/** Methods that use a non-constant-time algorithm for comparing inputs. */
private class NonConstantTimeEqualsCall extends MethodAccess {
NonConstantTimeEqualsCall() {
getMethod()
.hasQualifiedName("java.lang", "String", ["equals", "contentEquals", "equalsIgnoreCase"]) or
getMethod().hasQualifiedName("java.nio", "ByteBuffer", ["equals", "compareTo"])
}
}
/** A static method that uses a non-constant-time algorithm for comparing inputs. */
private class NonConstantTimeComparisonCall extends StaticMethodAccess {
NonConstantTimeComparisonCall() {
getMethod().hasQualifiedName("java.util", "Arrays", ["equals", "deepEquals"]) or
getMethod().hasQualifiedName("java.util", "Objects", "deepEquals") or
getMethod()
.hasQualifiedName("org.apache.commons.lang3", "StringUtils",
["equals", "equalsAny", "equalsAnyIgnoreCase", "equalsIgnoreCase"])
}
}
/**
* A config that tracks data flow from remote user input to methods
* that compare inputs using a non-constant-time algorithm.
*/
private class UserInputInComparisonConfig extends TaintTracking2::Configuration {
UserInputInComparisonConfig() { this = "UserInputInComparisonConfig" }
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
override predicate isSink(DataFlow::Node sink) {
exists(NonConstantTimeEqualsCall call |
sink.asExpr() = [call.getAnArgument(), call.getQualifier()]
)
or
exists(NonConstantTimeComparisonCall call | sink.asExpr() = call.getAnArgument())
}
}
/** Holds if `expr` looks like a constant. */
private predicate looksLikeConstant(Expr expr) {
expr.isCompileTimeConstant()
or
expr.(VarAccess).getVariable().isFinal() and expr.getType() instanceof TypeString
}
/**
* Holds if `firstObject` and `secondObject` are compared using a method
* that does not use a constant-time algorithm, for example, `String.equals()`.
*/
private predicate isNonConstantTimeEqualsCall(Expr firstObject, Expr secondObject) {
exists(NonConstantTimeEqualsCall call |
firstObject = call.getQualifier() and
secondObject = call.getAnArgument()
or
firstObject = call.getAnArgument() and
secondObject = call.getQualifier()
)
}
/**
* Holds if `firstInput` and `secondInput` are compared using a static method
* that does not use a constant-time algorithm, for example, `Arrays.equals()`.
*/
private predicate isNonConstantTimeComparisonCall(Expr firstInput, Expr secondInput) {
exists(NonConstantTimeComparisonCall call |
firstInput = call.getArgument(0) and secondInput = call.getArgument(1)
or
firstInput = call.getArgument(1) and secondInput = call.getArgument(0)
)
}
/**
* Holds if there is a fast-fail check while comparing `firstArray` and `secondArray`.
*/
private predicate existsFailFastCheck(Expr firstArray, Expr secondArray) {
exists(
Guard guard, EqualityTest eqTest, boolean branch, Stmt fastFailingStmt,
ArrayAccess firstArrayAccess, ArrayAccess secondArrayAccess
|
guard = eqTest and
// For `==` false branch is fail fast; for `!=` true branch is fail fast
branch = eqTest.polarity().booleanNot() and
(
fastFailingStmt instanceof ReturnStmt or
fastFailingStmt instanceof BreakStmt or
fastFailingStmt instanceof ThrowStmt
) and
guard.controls(fastFailingStmt.getBasicBlock(), branch) and
DataFlow::localExprFlow(firstArrayAccess, eqTest.getLeftOperand()) and
DataFlow::localExprFlow(secondArrayAccess, eqTest.getRightOperand())
|
firstArrayAccess.getArray() = firstArray and secondArray = secondArrayAccess
or
secondArrayAccess.getArray() = firstArray and secondArray = firstArrayAccess
)
}
/** A sink that compares input using a non-constant-time algorithm. */
class NonConstantTimeComparisonSink extends DataFlow::Node {
Expr anotherParameter;
NonConstantTimeComparisonSink() {
(
isNonConstantTimeEqualsCall(this.asExpr(), anotherParameter)
or
isNonConstantTimeComparisonCall(this.asExpr(), anotherParameter)
or
existsFailFastCheck(this.asExpr(), anotherParameter)
) and
not looksLikeConstant(anotherParameter)
}
/** Holds if remote user input was used in the comparison. */
predicate includesUserInput() {
exists(UserInputInComparisonConfig config |
config.hasFlowTo(DataFlow2::exprNode(anotherParameter))
)
}
}
/**
* A configuration that tracks data flow from cryptographic operations
* to methods that compare data using a non-constant-time algorithm.
*/
class NonConstantTimeCryptoComparisonConfig extends TaintTracking::Configuration {
NonConstantTimeCryptoComparisonConfig() { this = "NonConstantTimeCryptoComparisonConfig" }
override predicate isSource(DataFlow::Node source) { source instanceof CryptoOperationSource }
override predicate isSink(DataFlow::Node sink) { sink instanceof NonConstantTimeComparisonSink }
}

View File

@@ -0,0 +1,4 @@
<!DOCTYPE qhelp PUBLIC "-//Semmle//qhelp//EN" "qhelp.dtd">
<qhelp>
<include src="TimingAttackAgainstSignature.qhelp" />
</qhelp>

View File

@@ -0,0 +1,22 @@
/**
* @name Possible timing attack against signature validation
* @description When checking a signature over a message, a constant-time algorithm should be used.
* Otherwise, there is a risk of a timing attack that allows an attacker
* to forge a valid signature for an arbitrary message. For a successful attack,
* the attacker has to be able to send to the validation procedure both the message and the signature.
* @kind path-problem
* @problem.severity warning
* @precision medium
* @id java/possible-timing-attack-against-signature
* @tags security
* external/cwe/cwe-208
*/
import java
import NonConstantTimeCheckOnSignatureQuery
import DataFlow::PathGraph
from DataFlow::PathNode source, DataFlow::PathNode sink, NonConstantTimeCryptoComparisonConfig conf
where conf.hasFlowPath(source, sink)
select sink.getNode(), source, sink, "Possible timing attack against $@ validation.", source,
source.getNode().(CryptoOperationSource).getCall().getResultType()

View File

@@ -0,0 +1,9 @@
public boolean validate(HttpRequest request, SecretKey key) throws Exception {
byte[] message = getMessageFrom(request);
byte[] signature = getSignatureFrom(request);
Mac mac = Mac.getInstance("HmacSHA256");
mac.init(new SecretKeySpec(key.getEncoded(), "HmacSHA256"));
byte[] actual = mac.doFinal(message);
return MessageDigest.isEqual(signature, actual);
}

View File

@@ -0,0 +1,55 @@
<!DOCTYPE qhelp PUBLIC "-//Semmle//qhelp//EN" "qhelp.dtd">
<qhelp>
<overview>
<p>
A constant-time algorithm should be used for checking a MAC or a digital signature.
In other words, the comparison time should not depend on the content of the input.
Otherwise, an attacker may be able to forge a valid signature for an arbitrary message
by running a timing attack if they can send to the validation procedure
both the message and the signature. A successful attack can result in authentication bypass.
</p>
</overview>
<recommendation>
<p>
Use <code>MessageDigest.isEqual()</code> method to check MACs and signatures.
If this method is used, then the calculation time depends only on the length of input byte arrays,
and does not depend on the contents of the arrays.
</p>
</recommendation>
<example>
<p>
The following example uses <code>Arrays.equals()</code> method for validating a MAC over a message.
This method implements a non-constant-time algorithm.
Both the message and the signature come from an untrusted HTTP request:
</p>
<sample src="UnsafeMacComparison.java" />
<p>
The next example uses a safe constant-time algorithm for validating a MAC:
</p>
<sample src="SafeMacComparison.java" />
</example>
<references>
<li>
Wikipedia:
<a href="https://en.wikipedia.org/wiki/Timing_attack">Timing attack</a>.
</li>
<li>
Coursera:
<a href="https://www.coursera.org/lecture/crypto/timing-attacks-on-mac-verification-FHGW1">Timing attacks on MAC verification</a>
</li>
<li>
NCC Group:
<a href="https://www.nccgroup.trust/globalassets/our-research/us/whitepapers/TimeTrial.pdf">Time Trial: Racing Towards Practical Remote Timing Attacks</a>
</li>
<li>
Java API Specification:
<a href="https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/security/MessageDigest.html#isEqual(byte[],byte[])">MessageDigest.isEqual() method</a>
</li>
</references>
</qhelp>

View File

@@ -0,0 +1,28 @@
/**
* @name Timing attack against signature validation
* @description When checking a signature over a message, a constant-time algorithm should be used.
* Otherwise, an attacker may be able to forge a valid signature for an arbitrary message
* by running a timing attack if they can send to the validation procedure
* both the message and the signature.
* A successful attack can result in authentication bypass.
* @kind path-problem
* @problem.severity error
* @precision high
* @id java/timing-attack-against-signature
* @tags security
* external/cwe/cwe-208
*/
import java
import NonConstantTimeCheckOnSignatureQuery
import DataFlow::PathGraph
from DataFlow::PathNode source, DataFlow::PathNode sink, NonConstantTimeCryptoComparisonConfig conf
where
conf.hasFlowPath(source, sink) and
(
source.getNode().(CryptoOperationSource).includesUserInput() and
sink.getNode().(NonConstantTimeComparisonSink).includesUserInput()
)
select sink.getNode(), source, sink, "Timing attack against $@ validation.", source,
source.getNode().(CryptoOperationSource).getCall().getResultType()

View File

@@ -0,0 +1,9 @@
public boolean validate(HttpRequest request, SecretKey key) throws Exception {
byte[] message = getMessageFrom(request);
byte[] signature = getSignatureFrom(request);
Mac mac = Mac.getInstance("HmacSHA256");
mac.init(new SecretKeySpec(key.getEncoded(), "HmacSHA256"));
byte[] actual = mac.doFinal(message);
return Arrays.equals(signature, actual);
}

View File

@@ -268,11 +268,15 @@ private predicate summaryModelCsv(string row) {
// qualifier to arg
"java.io;InputStream;true;read;(byte[]);;Argument[-1];Argument[0];taint",
"java.io;InputStream;true;read;(byte[],int,int);;Argument[-1];Argument[0];taint",
"java.io;InputStream;true;readNBytes;(byte[],int,int);;Argument[-1];Argument[0];taint",
"java.io;InputStream;true;transferTo;(OutputStream);;Argument[-1];Argument[0];taint",
"java.io;ByteArrayOutputStream;false;writeTo;;;Argument[-1];Argument[0];taint",
"java.io;Reader;true;read;;;Argument[-1];Argument[0];taint",
// qualifier to return
"java.io;ByteArrayOutputStream;false;toByteArray;;;Argument[-1];ReturnValue;taint",
"java.io;ByteArrayOutputStream;false;toString;;;Argument[-1];ReturnValue;taint",
"java.io;InputStream;true;readAllBytes;;;Argument[-1];ReturnValue;taint",
"java.io;InputStream;true;readNBytes;(int);;Argument[-1];ReturnValue;taint",
"java.util;StringTokenizer;false;nextElement;();;Argument[-1];ReturnValue;taint",
"java.util;StringTokenizer;false;nextToken;;;Argument[-1];ReturnValue;taint",
"javax.xml.transform.sax;SAXSource;false;getInputSource;;;Argument[-1];ReturnValue;taint",
@@ -283,10 +287,12 @@ private predicate summaryModelCsv(string row) {
"java.net;URI;false;toAsciiString;;;Argument[-1];ReturnValue;taint",
"java.io;File;false;toURI;;;Argument[-1];ReturnValue;taint",
"java.io;File;false;toPath;;;Argument[-1];ReturnValue;taint",
"java.nio;ByteBuffer;false;array;();;Argument[-1];ReturnValue;taint",
"java.nio.file;Path;false;toFile;;;Argument[-1];ReturnValue;taint",
"java.io;BufferedReader;true;readLine;;;Argument[-1];ReturnValue;taint",
"java.io;Reader;true;read;();;Argument[-1];ReturnValue;taint",
// arg to return
"java.nio;ByteBuffer;false;wrap;(byte[]);;Argument[0];ReturnValue;taint",
"java.util;Base64$Encoder;false;encode;(byte[]);;Argument[0];ReturnValue;taint",
"java.util;Base64$Encoder;false;encode;(ByteBuffer);;Argument[0];ReturnValue;taint",
"java.util;Base64$Encoder;false;encodeToString;(byte[]);;Argument[0];ReturnValue;taint",