Java: Static initialization vector

java/ql/src/experimental/Security/CWE/CWE-1204/BadStaticInitializationVector.java

@@ -0,0 +1,4 @@
+byte[] iv = new byte[16]; // all zeroes
+GCMParameterSpec params = new GCMParameterSpec(128, iv);
+Cipher cipher = Cipher.getInstance("AES/GCM/PKCS5PADDING");
+cipher.init(Cipher.ENCRYPT_MODE, key, params);

java/ql/src/experimental/Security/CWE/CWE-1204/GoodRandomInitializationVector.java

@@ -0,0 +1,6 @@
+byte[] iv = new byte[16];
+SecureRandom random = SecureRandom.getInstanceStrong();
+random.nextBytes(iv);
+GCMParameterSpec params = new GCMParameterSpec(128, iv);
+Cipher cipher = Cipher.getInstance("AES/GCM/PKCS5PADDING");
+cipher.init(Cipher.ENCRYPT_MODE, key, params);

java/ql/src/experimental/Security/CWE/CWE-1204/StaticInitializationVector.qhelp

@@ -0,0 +1,46 @@
+<!DOCTYPE qhelp PUBLIC "-//Semmle//qhelp//EN" "qhelp.dtd">
+<qhelp>
+
+<overview>
+<p>
+A cipher needs an initialization vector (IV) when it is used in certain modes
+such as CBC or GCM. Under the same secret key, IVs should be unique and ideally unpredictable.
+Given a secret key, if the same IV is used for encryption, the same plaintexts result in the same ciphertexts.
+This lets an attacker learn if the same data pieces are transferred or stored,
+or this can help the attacker run a dictionary attack.
+</p>
+</overview>
+
+<recommendation>
+<p>
+Use a random IV generated by <code>SecureRandom</code>.
+</p>
+</recommendation>
+
+<example>
+<p>
+The following example initializes a cipher with a static IV which is unsafe:
+</p>
+<sample src="BadStaticInitializationVector.java" />
+
+<p>
+The next example initializes a cipher with a random IV:
+</p>
+<sample src="GoodRandomInitializationVector.java" />
+</example>
+
+<references>
+<li>
+  Wikipedia:
+  <a href="https://en.wikipedia.org/wiki/Initialization_vector">Initialization vector</a>.
+</li>
+<li>
+  National Institute of Standards and Technology:
+  <a href="https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38a.pdf">Recommendation for Block Cipher Modes of Operation</a>.
+</li>
+<li>
+  National Institute of Standards and Technology:
+  <a href="https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.140-2.pdf">FIPS 140-2: Security Requirements for Cryptographic Modules</a>.
+</li>
+</references>
+</qhelp>

java/ql/src/experimental/Security/CWE/CWE-1204/StaticInitializationVector.ql

@@ -0,0 +1,26 @@
+/**
+ * @name Using a static initialization vector for encryption
+ * @description A cipher needs an initialization vector (IV) in some cases,
+ *              for example, when CBC or GCM modes are used. IVs are used to randomize the encryption,
+ *              therefore they should be unique and ideally unpredictable.
+ *              Otherwise, the same plaintexts result in same ciphertexts under a given secret key.
+ *              If a static IV is used for encryption, this lets an attacker learn
+ *              if the same data pieces are transferred or stored,
+ *              or this can help the attacker run a dictionary attack.
+ * @kind path-problem
+ * @problem.severity warning
+ * @precision high
+ * @id java/static-initialization-vector
+ * @tags security
+ *       external/cwe/cwe-329
+ *       external/cwe/cwe-1204
+ */
+
+import java
+import experimental.semmle.code.java.security.StaticInitializationVectorQuery
+import DataFlow::PathGraph
+
+from DataFlow::PathNode source, DataFlow::PathNode sink, StaticInitializationVectorConfig conf
+where conf.hasFlowPath(source, sink)
+select sink.getNode(), source, sink, "A $@ should not be used for encryption.", source.getNode(),
+  "static initialization vector"

java/ql/src/experimental/semmle/code/java/security/StaticInitializationVectorQuery.qll

@@ -0,0 +1,165 @@
+import java
+import semmle.code.java.dataflow.TaintTracking
+import semmle.code.java.dataflow.TaintTracking2
+
+/**
+ * Holds if `array` is initialized only with constants.
+ */
+private predicate initializedWithConstants(ArrayCreationExpr array) {
+  // creating an array without an initializer, for example `new byte[8]`
+  not exists(array.getInit())
+  or
+  // creating a multidimensional array with an initializer like `{ new byte[8], new byte[16] }`
+  // This works around https://github.com/github/codeql/issues/6552 -- change me once there is
+  // a better way to distinguish nested initializers that create zero-filled arrays
+  // (e.g. `new byte[1]`) from those with an initializer list (`new byte[] { 1 }` or just `{ 1 }`)
+  array.getInit().getAnInit().getAChildExpr() instanceof IntegerLiteral
+  or
+  // creating an array wit an initializer like `new byte[] { 1, 2 }`
+  forex(Expr element | element = array.getInit().getAnInit() |
+    element instanceof CompileTimeConstantExpr
+  )
+}
+
+/**
+ * An expression that creates a byte array that is initialized with constants.
+ */
+private class StaticByteArrayCreation extends ArrayCreationExpr {
+  StaticByteArrayCreation() {
+    this.getType().(Array).getElementType().(PrimitiveType).getName() = "byte" and
+    initializedWithConstants(this)
+  }
+}
+
+/** An expression that updates `array`. */
+private class ArrayUpdate extends Expr {
+  Expr array;
+
+  ArrayUpdate() {
+    exists(Assignment assign |
+      assign = this and
+      assign.getDest().(ArrayAccess).getArray() = array and
+      not assign.getSource() instanceof CompileTimeConstantExpr
+    )
+    or
+    exists(StaticMethodAccess ma |
+      ma.getMethod().hasQualifiedName("java.lang", "System", "arraycopy") and
+      ma = this and
+      ma.getArgument(2) = array
+    )
+    or
+    exists(MethodAccess ma, Method m |
+      m = ma.getMethod() and
+      ma = this and
+      ma.getArgument(0) = array
+    |
+      m.hasQualifiedName("java.io", "InputStream", "read") or
+      m.hasQualifiedName("java.nio", "ByteBuffer", "get") or
+      m.hasQualifiedName("java.security", "SecureRandom", "nextBytes") or
+      m.hasQualifiedName("java.util", "Random", "nextBytes")
+    )
+  }
+
+  /** Returns the updated array. */
+  Expr getArray() { result = array }
+}
+
+/**
+ * A config that tracks dataflow from creating an array to an operation that updates it.
+ */
+private class ArrayUpdateConfig extends TaintTracking2::Configuration {
+  ArrayUpdateConfig() { this = "ArrayUpdateConfig" }
+
+  override predicate isSource(DataFlow::Node source) {
+    source.asExpr() instanceof StaticByteArrayCreation
+  }
+
+  override predicate isSink(DataFlow::Node sink) {
+    exists(ArrayUpdate update | update.getArray() = sink.asExpr())
+  }
+}
+
+/**
+ * A source that defines an array that doesn't get updated.
+ */
+private class StaticInitializationVectorSource extends DataFlow::Node {
+  StaticInitializationVectorSource() {
+    exists(StaticByteArrayCreation array | array = this.asExpr() |
+      not exists(ArrayUpdateConfig config | config.hasFlow(DataFlow2::exprNode(array), _))
+    )
+  }
+}
+
+/**
+ * A config that tracks initialization of a cipher for encryption.
+ */
+private class EncryptionModeConfig extends TaintTracking2::Configuration {
+  EncryptionModeConfig() { this = "EncryptionModeConfig" }
+
+  override predicate isSource(DataFlow::Node source) {
+    source
+        .asExpr()
+        .(FieldRead)
+        .getField()
+        .hasQualifiedName("javax.crypto", "Cipher", "ENCRYPT_MODE")
+  }
+
+  override predicate isSink(DataFlow::Node sink) {
+    exists(MethodAccess ma, Method m | m = ma.getMethod() |
+      m.hasQualifiedName("javax.crypto", "Cipher", "init") and
+      ma.getArgument(0) = sink.asExpr()
+    )
+  }
+}
+
+/**
+ * A sink that initializes a cipher for encryption with unsafe parameters.
+ */
+private class EncryptionInitializationSink extends DataFlow::Node {
+  EncryptionInitializationSink() {
+    exists(MethodAccess ma, Method m, EncryptionModeConfig config | m = ma.getMethod() |
+      m.hasQualifiedName("javax.crypto", "Cipher", "init") and
+      m.getParameterType(2)
+          .(RefType)
+          .hasQualifiedName("java.security.spec", "AlgorithmParameterSpec") and
+      ma.getArgument(2) = this.asExpr() and
+      config.hasFlowToExpr(ma.getArgument(0))
+    )
+  }
+}
+
+/**
+ * Holds if `fromNode` to `toNode` is a dataflow step
+ * that creates cipher's parameters with initialization vector.
+ */
+private predicate createInitializationVectorSpecStep(DataFlow::Node fromNode, DataFlow::Node toNode) {
+  exists(ConstructorCall cc, RefType type |
+    cc = toNode.asExpr() and type = cc.getConstructedType()
+  |
+    type.hasQualifiedName("javax.crypto.spec", "IvParameterSpec") and
+    cc.getArgument(0) = fromNode.asExpr()
+    or
+    type.hasQualifiedName("javax.crypto.spec", ["GCMParameterSpec", "RC2ParameterSpec"]) and
+    cc.getArgument(1) = fromNode.asExpr()
+    or
+    type.hasQualifiedName("javax.crypto.spec", "RC5ParameterSpec") and
+    cc.getArgument(3) = fromNode.asExpr()
+  )
+}
+
+/**
+ * A config that tracks dataflow to initializing a cipher with a static initialization vector.
+ */
+class StaticInitializationVectorConfig extends TaintTracking::Configuration {
+  StaticInitializationVectorConfig() { this = "StaticInitializationVectorConfig" }
+
+  override predicate isSource(DataFlow::Node source) {
+    source instanceof StaticInitializationVectorSource
+  }
+
+  override predicate isSink(DataFlow::Node sink) { sink instanceof EncryptionInitializationSink }
+
+  override predicate isAdditionalTaintStep(DataFlow::Node fromNode, DataFlow::Node toNode) {
+    createInitializationVectorSpecStep(fromNode, toNode)
+  }
+}