C#: Extend neutrals with a kind column and introduce validation.

This commit is contained in:
Michael Nebel
2023-04-25 16:31:33 +02:00
parent 9558522d84
commit 4dcfb4d8cb
4 changed files with 17 additions and 10 deletions

View File

@@ -12,7 +12,7 @@
* - Summaries:
* `namespace; type; subtypes; name; signature; ext; input; output; kind; provenance`
* - Neutrals:
* `namespace; type; name; signature; provenance`
* `namespace; 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
@@ -72,7 +72,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.
@@ -104,7 +106,7 @@ predicate sinkModel = Extensions::sinkModel/9;
predicate summaryModel = Extensions::summaryModel/10;
/** Holds if a model exists indicating there is no flow for the given parameters. */
predicate neutralModel = Extensions::neutralModel/5;
predicate neutralModel = Extensions::neutralModel/6;
private predicate relevantNamespace(string namespace) {
sourceModel(namespace, _, _, _, _, _, _, _, _) or
@@ -218,6 +220,11 @@ module ModelValidation {
not kind = ["local", "remote", "file", "file-write"] 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() {
@@ -232,7 +239,7 @@ module ModelValidation {
summaryModel(namespace, type, _, name, signature, ext, _, _, _, provenance) and
pred = "summary"
or
neutralModel(namespace, type, name, signature, provenance) and
neutralModel(namespace, type, name, signature, _, provenance) and
ext = "" and
pred = "neutral"
|
@@ -275,7 +282,7 @@ private predicate elementSpec(
or
summaryModel(namespace, type, subtypes, name, signature, ext, _, _, _, _)
or
neutralModel(namespace, type, name, signature, _) and ext = "" and subtypes = false
neutralModel(namespace, type, name, signature, _, _) and ext = "" and subtypes = false
}
private predicate elementSpec(

View File

@@ -30,5 +30,5 @@ extensible predicate summaryModel(
* Holds if a model exists indicating there is no flow for the given parameters.
*/
extensible predicate neutralModel(
string namespace, string type, string name, string signature, string provenance
string namespace, 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

@@ -111,12 +111,12 @@ predicate summaryElement(Callable c, string input, string output, string kind, s
}
/**
* Holds if a neutral model exists for `c` with provenance `provenace`,
* Holds if a neutral summary model exists for `c` with provenance `provenace`,
* which means that there is no flow through `c`.
*/
predicate neutralElement(Callable c, string provenance) {
predicate neutralSummaryElement(Callable 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 = interpretElement(namespace, type, false, name, signature, "")
)
}