Merge pull request github#12595 from michaelnebel/enhanceprovenance

Java/C# : Enhance provenance.

Author: michaelnebel

config/identical-files.json

@@ -123,6 +123,10 @@
     "java/ql/src/utils/modelgenerator/internal/CaptureModels.qll",
     "csharp/ql/src/utils/modelgenerator/internal/CaptureModels.qll"
   ],
+  "Model as Data Generation Java/C# - CaptureModelsPrinting": [
+    "java/ql/src/utils/modelgenerator/internal/CaptureModelsPrinting.qll",
+    "csharp/ql/src/utils/modelgenerator/internal/CaptureModelsPrinting.qll"
+  ],
   "Sign Java/C#": [
     "java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll"
@@ -596,4 +600,4 @@
     "python/ql/lib/semmle/python/security/internal/EncryptionKeySizes.qll",
     "java/ql/lib/semmle/code/java/security/internal/EncryptionKeySizes.qll"
   ]
-}
+}

csharp/ql/lib/ext/generated/dotnet_runtime.model.yml

@@ -73,12 +73,15 @@
  *    sources "remote" indicates a default remote flow source, and for summaries
  *    "taint" indicates a default additional taint step and "value" indicates a
  *    globally applicable value-preserving step.
- * 9. The `provenance` column is a tag to indicate the origin of the summary.
- *    There are two supported values: "generated" and "manual". "generated" means that
- *    the model has been emitted by the model generator tool and "manual" means
- *    that the model has been written by hand. This information is used in a heuristic
- *    for dataflow analysis to determine, if a model or source code should be used for
- *    determining flow.
+ * 9. The `provenance` column is a tag to indicate the origin and verification of a model.
+ *    The format is {origin}-{verification} or just "manual" where the origin describes
+ *    the origin of the model and verification describes how the model has been verified.
+ *    Some examples are:
+ *    - "df-generated": The model has been generated by the model generator tool.
+ *    - "df-manual": The model has been generated by the model generator and verified by a human.
+ *    - "manual": The model has been written by hand.
+ *    This information is used in a heuristic for dataflow analysis to determine, if a
+ *    model or source code should be used for determining flow.
  */
 
 import csharp
@@ -248,7 +251,7 @@ module ModelValidation {
       not ext.regexpMatch("|Attribute") and
       result = "Unrecognized extra API graph element \"" + ext + "\" in " + pred + " model."
       or
-      not provenance = ["manual", "generated"] and
+      invalidProvenance(provenance) and
       result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
     )
   }

csharp/ql/lib/semmle/code/csharp/dataflow/ExternalFlow.qll

@@ -137,8 +137,6 @@ private class RecordConstructorFlow extends SummarizedCallable {
       preservesValue = true
     )
   }
-
-  override predicate hasProvenance(string provenance) { provenance = "manual" }
 }
 
 class RequiredSummaryComponentStack = Impl::Public::RequiredSummaryComponentStack;

csharp/ql/lib/semmle/code/csharp/dataflow/FlowSummary.qll

@@ -95,7 +95,7 @@ class DataFlowSummarizedCallable instanceof FlowSummary::SummarizedCallable {
   DataFlowSummarizedCallable() {
     not this.fromSource()
     or
-    this.fromSource() and not this.isAutoGenerated()
+    this.fromSource() and not this.applyGeneratedModel()
   }
 
   string toString() { result = super.toString() }

csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowDispatch.qll

@@ -215,6 +215,54 @@ module Public {
     abstract predicate required(SummaryComponent head, SummaryComponentStack tail);
   }
 
+  /**
+   * Gets the valid model origin values.
+   */
+  private string getValidModelOrigin() {
+    result =
+      [
+        "ai", // AI (machine learning)
+        "df", // Dataflow (model generator)
+        "tb", // Type based (model generator)
+        "hq", // Heuristic query
+      ]
+  }
+
+  /**
+   * A class used to represent provenance values for MaD models.
+   *
+   * The provenance value is a string of the form `origin-verification`
+   * (or just `manual`), where `origin` is a value indicating the
+   * origin of the model, and `verification` is a value indicating, how
+   * the model was verified.
+   *
+   * Examples could be:
+   * - `df-generated`: A model produced by the model generator, but not verified by a human.
+   * - `ai-manual`: A model produced by AI, but verified by a human.
+   */
+  class Provenance extends string {
+    private string verification;
+
+    Provenance() {
+      exists(string origin | origin = getValidModelOrigin() |
+        this = origin + "-" + verification and
+        verification = ["manual", "generated"]
+      )
+      or
+      this = verification and verification = "manual"
+    }
+
+    /**
+     * Holds if this is a valid generated provenance value.
+     */
+    predicate isGenerated() { verification = "generated" }
+
+    /**
+     * Holds if this is a valid manual provenance value.
+     */
+    predicate isManual() { verification = "manual" }
+  }
+
   /** A callable with a flow summary. */
   abstract class SummarizedCallable extends SummarizedCallableBase {
     bindingset[this]
@@ -248,41 +296,61 @@ module Public {
     }
 
     /**
-     * Holds if all the summaries that apply to `this` are auto generated and not manually created.
+     * Holds if there exists a generated summary that applies to this callable.
      */
-    final predicate isAutoGenerated() {
-      this.hasProvenance(["generated", "ai-generated"]) and not this.isManual()
+    final predicate hasGeneratedModel() {
+      exists(Provenance p | p.isGenerated() and this.hasProvenance(p))
     }
 
     /**
-     * Holds if there exists a manual summary that applies to `this`.
+     * Holds if all the summaries that apply to this callable are auto generated and not manually created.
+     * That is, only apply generated models, when there are no manual models.
      */
-    final predicate isManual() { this.hasProvenance("manual") }
+    final predicate applyGeneratedModel() {
+      this.hasGeneratedModel() and
+      not this.hasManualModel()
+    }
 
     /**
-     * Holds if there exists a summary that applies to `this` that has provenance `provenance`.
+     * Holds if there exists a manual summary that applies to this callable.
      */
-    predicate hasProvenance(string provenance) { none() }
+    final predicate hasManualModel() {
+      exists(Provenance p | p.isManual() and this.hasProvenance(p))
+    }
+
+    /**
+     * Holds if there exists a manual summary that applies to this callable.
+     * Always apply manual models if they exist.
+     */
+    final predicate applyManualModel() { this.hasManualModel() }
+
+    /**
+     * Holds if there exists a summary that applies to this callable
+     * that has provenance `provenance`.
+     */
+    predicate hasProvenance(Provenance provenance) { provenance = "manual" }
   }
 
   /** A callable where there is no flow via the callable. */
   class NeutralCallable extends SummarizedCallableBase {
-    NeutralCallable() { neutralElement(this, _) }
+    private Provenance provenance;
+
+    NeutralCallable() { neutralElement(this, provenance) }
 
     /**
      * Holds if the neutral is auto generated.
      */
-    predicate isAutoGenerated() { neutralElement(this, ["generated", "ai-generated"]) }
+    final predicate hasGeneratedModel() { provenance.isGenerated() }
 
     /**
-     * Holds if there exists a manual neutral that applies to `this`.
+     * Holds if there exists a manual neutral that applies to this callable.
      */
-    final predicate isManual() { this.hasProvenance("manual") }
+    final predicate hasManualModel() { provenance.isManual() }
 
     /**
-     * Holds if the neutral has provenance `provenance`.
+     * Holds if the neutral has provenance `p`.
      */
-    predicate hasProvenance(string provenance) { neutralElement(this, provenance) }
+    predicate hasProvenance(Provenance p) { p = provenance }
   }
 }
 
@@ -1017,12 +1085,18 @@ module Private {
       private predicate relevantSummaryElementGenerated(
         AccessPath inSpec, AccessPath outSpec, string kind
       ) {
-        summaryElement(this, inSpec, outSpec, kind, ["generated", "ai-generated"]) and
-        not summaryElement(this, _, _, _, "manual")
+        exists(Provenance provenance |
+          provenance.isGenerated() and
+          summaryElement(this, inSpec, outSpec, kind, provenance)
+        ) and
+        not this.applyManualModel()
       }
 
       private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) {
-        summaryElement(this, inSpec, outSpec, kind, "manual")
+        exists(Provenance provenance |
+          provenance.isManual() and
+          summaryElement(this, inSpec, outSpec, kind, provenance)
+        )
         or
         this.relevantSummaryElementGenerated(inSpec, outSpec, kind)
       }
@@ -1041,7 +1115,7 @@ module Private {
         )
       }
 
-      override predicate hasProvenance(string provenance) {
+      override predicate hasProvenance(Provenance provenance) {
         summaryElement(this, _, _, _, provenance)
       }
     }
@@ -1052,6 +1126,10 @@ module Private {
       not exists(interpretComponent(c))
     }
 
+    /** Holds if `provenance` is not a valid provenance value. */
+    bindingset[provenance]
+    predicate invalidProvenance(string provenance) { not provenance instanceof Provenance }
+
     /**
      * Holds if token `part` of specification `spec` has an invalid index.
      * E.g., `Argument[-1]`.
@@ -1219,11 +1297,11 @@ module Private {
     }
 
     private string renderProvenance(SummarizedCallable c) {
-      if c.isManual() then result = "manual" else c.hasProvenance(result)
+      if c.applyManualModel() then result = "manual" else c.hasProvenance(result)
     }
 
     private string renderProvenanceNeutral(NeutralCallable c) {
-      if c.isManual() then result = "manual" else c.hasProvenance(result)
+      if c.hasManualModel() then result = "manual" else c.hasProvenance(result)
     }
 
     /**

csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll

@@ -86,8 +86,6 @@ module EntityFramework {
   abstract class EFSummarizedCallable extends SummarizedCallable {
     bindingset[this]
     EFSummarizedCallable() { any() }
-
-    override predicate hasProvenance(string provenance) { provenance = "manual" }
   }
 
   private class DbSetAddOrUpdateRequiredSummaryComponentStack extends RequiredSummaryComponentStack {

csharp/ql/lib/semmle/code/csharp/frameworks/EntityFramework.qll

@@ -10,5 +10,5 @@ import semmle.code.csharp.dataflow.ExternalFlow
 from string package, string type, string name, string signature, string provenance
 where
   neutralModel(package, type, name, signature, provenance) and
-  provenance != "generated"
+  not provenance.matches("%generated")
 select package, type, name, signature, provenance order by package, type, name, signature

csharp/ql/src/utils/modelconverter/ExtractNeutrals.ql

@@ -12,6 +12,6 @@ from
   string input, string kind, string provenance
 where
   sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance) and
-  provenance != "generated"
+  not provenance.matches("%generated")
 select namespace, type, subtypes, name, signature, ext, input, kind, provenance order by
     namespace, type, name, signature, input, kind

csharp/ql/src/utils/modelconverter/ExtractSinks.ql

@@ -12,6 +12,6 @@ from
   string output, string kind, string provenance
 where
   sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance) and
-  provenance != "generated"
+  not provenance.matches("%generated")
 select namespace, type, subtypes, name, signature, ext, output, kind, provenance order by
     namespace, type, name, signature, output, kind