Java: Extend neutrals with a kind column and introduce validation.

This commit is contained in:
Michael Nebel
2023-04-26 11:22:45 +02:00
parent 4ac0396b67
commit bcbda9046f
4 changed files with 17 additions and 10 deletions

View File

@@ -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
}
/**

View File

@@ -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
);
/**

View File

@@ -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.

View File

@@ -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, "")
)
}