Continue Artifact data-flow WIP

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

@@ -244,24 +244,29 @@ module JCAModel {
   /**
    * Initialiation vectors
    */
-  abstract class IVParameterInstantiation extends ClassInstanceExpr {
-    abstract Expr getIV();
+  abstract class IVParameterInstantiation extends Crypto::InitializationVectorArtifactInstance instanceof ClassInstanceExpr
+  {
+    abstract Expr getInput();
   }
 
   class IvParameterSpecInstance extends IVParameterInstantiation {
     IvParameterSpecInstance() {
-      this.getConstructedType().hasQualifiedName("javax.crypto.spec", "IvParameterSpec")
+      this.(ClassInstanceExpr)
+          .getConstructedType()
+          .hasQualifiedName("javax.crypto.spec", "IvParameterSpec")
     }
 
-    override Expr getIV() { result = super.getArgument(0) }
+    override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(0) }
   }
 
   class GCMParameterSpecInstance extends IVParameterInstantiation {
     GCMParameterSpecInstance() {
-      this.getConstructedType().hasQualifiedName("javax.crypto.spec", "GCMParameterSpec")
+      this.(ClassInstanceExpr)
+          .getConstructedType()
+          .hasQualifiedName("javax.crypto.spec", "GCMParameterSpec")
     }
 
-    override Expr getIV() { result = super.getArgument(1) }
+    override Expr getInput() { result = this.(ClassInstanceExpr).getArgument(1) }
   }
 
   class CipherInitCall extends MethodCall {
@@ -280,18 +285,24 @@ module JCAModel {
   }
 
   // TODO: cipher.getParameters().getParameterSpec(GCMParameterSpec.class);
-  class InitializationVectorExpr extends Crypto::InitializationVectorArtifactInstance instanceof Expr
-  {
-    CipherInitCall call; // TODO: add origin to known sources (e.g. RNG, etc.)
-
-    InitializationVectorExpr() { this = call.getIV() }
-  }
+  /*
+   *  class InitializationVectorArg extends Crypto::InitializationVectorArtifactInstance instanceof Expr
+   *  {
+   *    IVParameterInstantiation creation;
+   *
+   *    InitializationVectorArg() { this = creation.getInput() }
+   *  }
+   */
 
   class InitializationVector extends Crypto::InitializationVector {
-    InitializationVectorExpr instance;
+    IVParameterInstantiation instance;
 
     InitializationVector() { this = Crypto::TInitializationVector(instance) }
 
     override Location getLocation() { result = instance.getLocation() }
+
+    override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance }
+
+    override Crypto::DataFlowNode getInputData() { result.asExpr() = instance.getInput() }
   }
 }

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

@@ -1,5 +1,11 @@
 private import codeql.cryptography.Model
-private import java as Lang
+private import java as Language
+private import semmle.code.java.security.InsecureRandomnessQuery
+private import semmle.code.java.security.RandomQuery
+
+private class UnknownLocation extends Language::Location {
+  UnknownLocation() { this.getFile().getAbsolutePath() = "" }
+}
 
 /**
  * A dummy location which is used when something doesn't have a location in
@@ -7,24 +13,72 @@ private import java as Lang
  * may be several distinct kinds of unknown locations. For example: one for
  * expressions, one for statements and one for other program elements.
  */
-class UnknownLocation extends Location {
-  UnknownLocation() { this.getFile().getAbsolutePath() = "" }
-}
-
-/**
- * A dummy location which is used when something doesn't have a location in
- * the source code but needs to have a `Location` associated with it.
- */
-class UnknownDefaultLocation extends UnknownLocation {
+private class UnknownDefaultLocation extends UnknownLocation {
   UnknownDefaultLocation() { locations_default(this, _, 0, 0, 0, 0) }
 }
 
-module CryptoInput implements InputSig<Lang::Location> {
-  class LocatableElement = Lang::Element;
+module CryptoInput implements InputSig<Language::Location> {
+  class DataFlowNode = DataFlow::Node;
+
+  class LocatableElement = Language::Element;
 
   class UnknownLocation = UnknownDefaultLocation;
+
+  predicate rngToIvFlow(DataFlowNode rng, DataFlowNode iv) { none() }
 }
 
-module Crypto = CryptographyBase<Lang::Location, CryptoInput>;
+/**
+ * Instantiate the model
+ */
+module Crypto = CryptographyBase<Language::Location, CryptoInput>;
 
+/**
+ * Random number generation, where each instance is modelled as the expression
+ * tied to an output node (i.e., the result of the source of randomness)
+ */
+abstract class RandomnessInstance extends Crypto::RandomNumberGenerationInstance {
+  abstract Crypto::RNGSourceSecurity getSourceSecurity();
+
+  Crypto::TRNGSeedSecurity getSeedSecurity(Location location) { none() }
+}
+
+class SecureRandomnessInstance extends RandomnessInstance {
+  SecureRandomnessInstance() {
+    exists(RandomDataSource s | this = s.getOutput() |
+      s.getSourceOfRandomness() instanceof SecureRandomNumberGenerator
+    )
+  }
+
+  override Crypto::RNGSourceSecurity getSourceSecurity() {
+    result instanceof Crypto::RNGSourceSecure
+  }
+}
+
+class InsecureRandomnessInstance extends RandomnessInstance {
+  InsecureRandomnessInstance() { exists(InsecureRandomnessSource node | this = node.asExpr()) }
+
+  override Crypto::RNGSourceSecurity getSourceSecurity() {
+    result instanceof Crypto::RNGSourceInsecure
+  }
+}
+
+class RandomnessArtifact extends Crypto::RandomNumberGeneration {
+  RandomnessInstance instance;
+
+  RandomnessArtifact() { this = Crypto::TRandomNumberGeneration(instance) }
+
+  override Location getLocation() { result = instance.getLocation() }
+
+  override Crypto::RNGSourceSecurity getSourceSecurity() { result = instance.getSourceSecurity() }
+
+  override Crypto::TRNGSeedSecurity getSeedSecurity(Location location) {
+    result = instance.getSeedSecurity(location)
+  }
+
+  override Crypto::DataFlowNode asOutputData() { result.asExpr() = instance }
+
+  override Crypto::DataFlowNode getInputData() { none() }
+}
+
+// Import library-specific modeling
 import JCA