From bcbda9046f6f53a3eafcc2b4dceb1972de15ac57 Mon Sep 17 00:00:00 2001 From: Michael Nebel Date: Wed, 26 Apr 2023 11:22:45 +0200 Subject: [PATCH] Java: Extend neutrals with a kind column and introduce validation. --- .../semmle/code/java/dataflow/ExternalFlow.qll | 17 ++++++++++++----- .../java/dataflow/ExternalFlowExtensions.qll | 2 +- .../java/dataflow/internal/FlowSummaryImpl.qll | 2 +- .../internal/FlowSummaryImplSpecific.qll | 6 +++--- 4 files changed, 17 insertions(+), 10 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll index e70df8cab68..1f5d46c5588 100644 --- a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll +++ b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll @@ -12,7 +12,7 @@ * - Summaries: * `package; type; subtypes; name; signature; ext; input; output; kind; provenance` * - Neutrals: - * `package; type; name; signature; provenance` + * `package; type; name; signature; kind; provenance` * A neutral is used to indicate that there is no flow via a callable. * * The interpretation of a row is similar to API-graphs with a left-to-right @@ -65,7 +65,9 @@ * which classes the interpreted elements should be added. For example, for * 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. + * globally applicable value-preserving step. For neutrals the kind can be `summary`, + * `source` or `sink` to indicate that the neutral is neutral with respect to + * flow (no summary), source (is not a source) or sink (is not a sink). * 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. @@ -165,7 +167,7 @@ predicate summaryModel( } /** Holds if a neutral model exists indicating there is no flow for the given parameters. */ -predicate neutralModel = Extensions::neutralModel/5; +predicate neutralModel = Extensions::neutralModel/6; private predicate relevantPackage(string package) { sourceModel(package, _, _, _, _, _, _, _, _) or @@ -288,6 +290,11 @@ module ModelValidation { not kind.matches("qltest%") and result = "Invalid kind \"" + kind + "\" in source model." ) + or + exists(string kind | neutralModel(_, _, _, _, kind, _) | + not kind = ["summary", "source", "sink"] and + result = "Invalid kind \"" + kind + "\" in neutral model." + ) } private string getInvalidModelSignature() { @@ -302,7 +309,7 @@ module ModelValidation { summaryModel(package, type, _, name, signature, ext, _, _, _, provenance) and pred = "summary" or - neutralModel(package, type, name, signature, provenance) and + neutralModel(package, type, name, signature, _, provenance) and ext = "" and pred = "neutral" | @@ -346,7 +353,7 @@ private predicate elementSpec( or summaryModel(package, type, subtypes, name, signature, ext, _, _, _, _) or - neutralModel(package, type, name, signature, _) and ext = "" and subtypes = false + neutralModel(package, type, name, signature, _, _) and ext = "" and subtypes = false } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/ExternalFlowExtensions.qll b/java/ql/lib/semmle/code/java/dataflow/ExternalFlowExtensions.qll index b06dc92c427..904b3ff96f3 100644 --- a/java/ql/lib/semmle/code/java/dataflow/ExternalFlowExtensions.qll +++ b/java/ql/lib/semmle/code/java/dataflow/ExternalFlowExtensions.qll @@ -30,7 +30,7 @@ extensible predicate summaryModel( * Holds if a neutral model exists indicating there is no flow for the given parameters. */ extensible predicate neutralModel( - string package, string type, string name, string signature, string provenance + string package, string type, string name, string signature, string kind, string provenance ); /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll index 890025a9483..034c6101de3 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll @@ -335,7 +335,7 @@ module Public { class NeutralCallable extends SummarizedCallableBase { private Provenance provenance; - NeutralCallable() { neutralElement(this, provenance) } + NeutralCallable() { neutralSummaryElement(this, provenance) } /** * Holds if the neutral is auto generated. diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll index cde591b19b1..1a0e06553d4 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll @@ -154,12 +154,12 @@ predicate summaryElement( } /** - * Holds if a neutral model exists for `c` with provenance `provenance`, + * Holds if a neutral summary model exists for `c` with provenance `provenance`, * which means that there is no flow through `c`. */ -predicate neutralElement(SummarizedCallableBase c, string provenance) { +predicate neutralSummaryElement(SummarizedCallableBase c, string provenance) { exists(string namespace, string type, string name, string signature | - neutralModel(namespace, type, name, signature, provenance) and + neutralModel(namespace, type, name, signature, "summary", provenance) and c.asCallable() = interpretElement(namespace, type, false, name, signature, "") ) }