Merge pull request #9867 from michaelnebel/csharp/nosummary

C#: Negative summaries (ie. no flow through)

Author: michaelnebel

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

@@ -5,12 +5,13 @@
  *
  * The CSV specification has the following columns:
  * - Sources:
- *   `namespace; type; subtypes; name; signature; ext; output; kind`
+ *   `namespace; type; subtypes; name; signature; ext; output; kind; provenance`
  * - Sinks:
- *   `namespace; type; subtypes; name; signature; ext; input; kind`
+ *   `namespace; type; subtypes; name; signature; ext; input; kind; provenance`
  * - Summaries:
- *   `namespace; type; subtypes; name; signature; ext; input; output; kind`
- *
+ *   `namespace; type; subtypes; name; signature; ext; input; output; kind; provenance`
+ * - Negative Summaries:
+ *   `namespace; type; name; signature; provenance`
  * The interpretation of a row is similar to API-graphs with a left-to-right
  * reading.
  * 1. The `namespace` column selects a namespace.
@@ -163,11 +164,27 @@ class SummaryModelCsv extends Unit {
   abstract predicate row(string row);
 }
 
-private predicate sourceModel(string row) { any(SourceModelCsv s).row(row) }
+/**
+ * A unit class for adding negative summary model rows.
+ *
+ * Extend this class to add additional flow summary definitions.
+ */
+class NegativeSummaryModelCsv extends Unit {
+  /** Holds if `row` specifies a negative summary definition. */
+  abstract predicate row(string row);
+}
+
+/** Holds if `row` is a source model. */
+predicate sourceModel(string row) { any(SourceModelCsv s).row(row) }
 
-private predicate sinkModel(string row) { any(SinkModelCsv s).row(row) }
+/** Holds if `row` is a sink model. */
+predicate sinkModel(string row) { any(SinkModelCsv s).row(row) }
 
-private predicate summaryModel(string row) { any(SummaryModelCsv s).row(row) }
+/** Holds if `row` is a summary model. */
+predicate summaryModel(string row) { any(SummaryModelCsv s).row(row) }
+
+/** Holds if `row` is a negative summary model. */
+predicate negativeSummaryModel(string row) { any(NegativeSummaryModelCsv s).row(row) }
 
 /** Holds if a source model exists for the given parameters. */
 predicate sourceModel(
@@ -230,6 +247,20 @@ predicate summaryModel(
   )
 }
 
+/** Holds if a summary model exists indicating there is no flow for the given parameters. */
+predicate negativeSummaryModel(
+  string namespace, string type, string name, string signature, string provenance
+) {
+  exists(string row |
+    negativeSummaryModel(row) and
+    row.splitAt(";", 0) = namespace and
+    row.splitAt(";", 1) = type and
+    row.splitAt(";", 2) = name and
+    row.splitAt(";", 3) = signature and
+    row.splitAt(";", 4) = provenance
+  )
+}
+
 private predicate relevantNamespace(string namespace) {
   sourceModel(namespace, _, _, _, _, _, _, _, _) or
   sinkModel(namespace, _, _, _, _, _, _, _, _) or
@@ -286,38 +317,7 @@ predicate modelCoverage(string namespace, int namespaces, string kind, string pa
 
 /** Provides a query predicate to check the CSV data for validation errors. */
 module CsvValidation {
-  /** Holds if some row in a CSV-based flow model appears to contain typos. */
-  query predicate invalidModelRow(string msg) {
-    exists(
-      string pred, string namespace, string type, string name, string signature, string ext,
-      string provenance
-    |
-      sourceModel(namespace, type, _, name, signature, ext, _, _, provenance) and pred = "source"
-      or
-      sinkModel(namespace, type, _, name, signature, ext, _, _, provenance) and pred = "sink"
-      or
-      summaryModel(namespace, type, _, name, signature, ext, _, _, _, provenance) and
-      pred = "summary"
-    |
-      not namespace.regexpMatch("[a-zA-Z0-9_\\.]+") and
-      msg = "Dubious namespace \"" + namespace + "\" in " + pred + " model."
-      or
-      not type.regexpMatch("[a-zA-Z0-9_<>,\\+]+") and
-      msg = "Dubious type \"" + type + "\" in " + pred + " model."
-      or
-      not name.regexpMatch("[a-zA-Z0-9_<>,]*") and
-      msg = "Dubious member name \"" + name + "\" in " + pred + " model."
-      or
-      not signature.regexpMatch("|\\([a-zA-Z0-9_<>\\.\\+\\*,\\[\\]]*\\)") and
-      msg = "Dubious signature \"" + signature + "\" in " + pred + " model."
-      or
-      not ext.regexpMatch("|Attribute") and
-      msg = "Unrecognized extra API graph element \"" + ext + "\" in " + pred + " model."
-      or
-      not provenance = ["manual", "generated"] and
-      msg = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
-    )
-    or
+  private string getInvalidModelInput() {
     exists(string pred, AccessPath input, string part |
       sinkModel(_, _, _, _, _, _, input, _, _) and pred = "sink"
       or
@@ -332,9 +332,11 @@ module CsvValidation {
         part = input.getToken(_) and
         parseParam(part, _)
       ) and
-      msg = "Unrecognized input specification \"" + part + "\" in " + pred + " model."
+      result = "Unrecognized input specification \"" + part + "\" in " + pred + " model."
     )
-    or
+  }
+
+  private string getInvalidModelOutput() {
     exists(string pred, string output, string part |
       sourceModel(_, _, _, _, _, _, output, _, _) and pred = "source"
       or
@@ -343,58 +345,123 @@ module CsvValidation {
       invalidSpecComponent(output, part) and
       not part = "" and
       not (part = ["Argument", "Parameter"] and pred = "source") and
-      msg = "Unrecognized output specification \"" + part + "\" in " + pred + " model."
+      result = "Unrecognized output specification \"" + part + "\" in " + pred + " model."
+    )
+  }
+
+  private string getInvalidModelKind() {
+    exists(string row, string kind | summaryModel(row) |
+      kind = row.splitAt(";", 8) and
+      not kind = ["taint", "value"] and
+      result = "Invalid kind \"" + kind + "\" in summary model."
     )
     or
+    exists(string row, string kind | sinkModel(row) |
+      kind = row.splitAt(";", 7) and
+      not kind = ["code", "sql", "xss", "remote", "html"] and
+      not kind.matches("encryption-%") and
+      result = "Invalid kind \"" + kind + "\" in sink model."
+    )
+    or
+    exists(string row, string kind | sourceModel(row) |
+      kind = row.splitAt(";", 7) and
+      not kind = ["local", "file"] and
+      result = "Invalid kind \"" + kind + "\" in source model."
+    )
+  }
+
+  private string getInvalidModelSubtype() {
+    exists(string pred, string row |
+      sourceModel(row) and pred = "source"
+      or
+      sinkModel(row) and pred = "sink"
+      or
+      summaryModel(row) and pred = "summary"
+    |
+      exists(string b |
+        b = row.splitAt(";", 2) and
+        not b = ["true", "false"] and
+        result = "Invalid boolean \"" + b + "\" in " + pred + " model."
+      )
+    )
+  }
+
+  private string getInvalidModelColumnCount() {
     exists(string pred, string row, int expect |
       sourceModel(row) and expect = 9 and pred = "source"
       or
       sinkModel(row) and expect = 9 and pred = "sink"
       or
       summaryModel(row) and expect = 10 and pred = "summary"
+      or
+      negativeSummaryModel(row) and expect = 5 and pred = "negative summary"
     |
       exists(int cols |
         cols = 1 + max(int n | exists(row.splitAt(";", n))) and
         cols != expect and
-        msg =
+        result =
           "Wrong number of columns in " + pred + " model row, expected " + expect + ", got " + cols +
             " in " + row + "."
       )
-      or
-      exists(string b |
-        b = row.splitAt(";", 2) and
-        not b = ["true", "false"] and
-        msg = "Invalid boolean \"" + b + "\" in " + pred + " model."
-      )
     )
-    or
-    exists(string row, string kind | summaryModel(row) |
-      kind = row.splitAt(";", 8) and
-      not kind = ["taint", "value"] and
-      msg = "Invalid kind \"" + kind + "\" in summary model."
-    )
-    or
-    exists(string row, string kind | sinkModel(row) |
-      kind = row.splitAt(";", 7) and
-      not kind = ["code", "sql", "xss", "remote", "html"] and
-      not kind.matches("encryption-%") and
-      msg = "Invalid kind \"" + kind + "\" in sink model."
-    )
-    or
-    exists(string row, string kind | sourceModel(row) |
-      kind = row.splitAt(";", 7) and
-      not kind = ["local", "file"] and
-      msg = "Invalid kind \"" + kind + "\" in source model."
+  }
+
+  private string getInvalidModelSignature() {
+    exists(
+      string pred, string namespace, string type, string name, string signature, string ext,
+      string provenance
+    |
+      sourceModel(namespace, type, _, name, signature, ext, _, _, provenance) and pred = "source"
+      or
+      sinkModel(namespace, type, _, name, signature, ext, _, _, provenance) and pred = "sink"
+      or
+      summaryModel(namespace, type, _, name, signature, ext, _, _, _, provenance) and
+      pred = "summary"
+      or
+      negativeSummaryModel(namespace, type, name, signature, provenance) and
+      ext = "" and
+      pred = "negative summary"
+    |
+      not namespace.regexpMatch("[a-zA-Z0-9_\\.]+") and
+      result = "Dubious namespace \"" + namespace + "\" in " + pred + " model."
+      or
+      not type.regexpMatch("[a-zA-Z0-9_<>,\\+]+") and
+      result = "Dubious type \"" + type + "\" in " + pred + " model."
+      or
+      not name.regexpMatch("[a-zA-Z0-9_<>,]*") and
+      result = "Dubious member name \"" + name + "\" in " + pred + " model."
+      or
+      not signature.regexpMatch("|\\([a-zA-Z0-9_<>\\.\\+\\*,\\[\\]]*\\)") and
+      result = "Dubious signature \"" + signature + "\" in " + pred + " model."
+      or
+      not ext.regexpMatch("|Attribute") and
+      result = "Unrecognized extra API graph element \"" + ext + "\" in " + pred + " model."
+      or
+      not provenance = ["manual", "generated"] and
+      result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
     )
   }
+
+  /** Holds if some row in a CSV-based flow model appears to contain typos. */
+  query predicate invalidModelRow(string msg) {
+    msg =
+      [
+        getInvalidModelSignature(), getInvalidModelInput(), getInvalidModelOutput(),
+        getInvalidModelSubtype(), getInvalidModelColumnCount(), getInvalidModelKind()
+      ]
+  }
 }
 
 private predicate elementSpec(
   string namespace, string type, boolean subtypes, string name, string signature, string ext
 ) {
-  sourceModel(namespace, type, subtypes, name, signature, ext, _, _, _) or
-  sinkModel(namespace, type, subtypes, name, signature, ext, _, _, _) or
+  sourceModel(namespace, type, subtypes, name, signature, ext, _, _, _)
+  or
+  sinkModel(namespace, type, subtypes, name, signature, ext, _, _, _)
+  or
   summaryModel(namespace, type, subtypes, name, signature, ext, _, _, _, _)
+  or
+  negativeSummaryModel(namespace, type, name, signature, _) and ext = "" and subtypes = false
 }
 
 private predicate elementSpec(
@@ -508,7 +575,7 @@ private Element interpretElement0(
   )
 }
 
-/** Gets the source/sink/summary element corresponding to the supplied parameters. */
+/** Gets the source/sink/summary/negativesummary element corresponding to the supplied parameters. */
 Element interpretElement(
   string namespace, string type, boolean subtypes, string name, string signature, string ext
 ) {

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

@@ -173,7 +173,7 @@ module Ssa {
     }
 
     /**
-     * Holds is this SSA definition is live at the end of basic block `bb`.
+     * Holds if this SSA definition is live at the end of basic block `bb`.
      * That is, this definition reaches the end of basic block `bb`, at which
      * point it is still live, without crossing another SSA definition of the
      * same source variable.

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

@@ -2129,18 +2129,37 @@ module Csv {
     if isBaseCallableOrPrototype(c) then result = "true" else result = "false"
   }
 
-  /** Computes the first 6 columns for CSV rows of `c`. */
+  private predicate partialModel(
+    DotNet::Callable c, string namespace, string type, string name, string parameters
+  ) {
+    c.getDeclaringType().hasQualifiedName(namespace, type) and
+    c.hasQualifiedName(_, name) and
+    parameters = "(" + parameterQualifiedTypeNamesToString(c) + ")"
+  }
+
+  /** Computes the first 6 columns for positive CSV rows of `c`. */
   string asPartialModel(DotNet::Callable c) {
-    exists(string namespace, string type, string name |
-      c.getDeclaringType().hasQualifiedName(namespace, type) and
-      c.hasQualifiedName(_, name) and
+    exists(string namespace, string type, string name, string parameters |
+      partialModel(c, namespace, type, name, parameters) and
       result =
         namespace + ";" //
           + type + ";" //
           + getCallableOverride(c) + ";" //
           + name + ";" //
-          + "(" + parameterQualifiedTypeNamesToString(c) + ")" + ";" //
+          + parameters + ";" //
           + /* ext + */ ";" //
     )
   }
+
+  /** Computes the first 4 columns for negative CSV rows of `c`. */
+  string asPartialNegativeModel(DotNet::Callable c) {
+    exists(string namespace, string type, string name, string parameters |
+      partialModel(c, namespace, type, name, parameters) and
+      result =
+        namespace + ";" //
+          + type + ";" //
+          + name + ";" //
+          + parameters + ";" //
+    )
+  }
 }