Shared: Provenance-based filtering of flow summaries

This commit is contained in:
Tom Hvitved
2025-12-16 13:50:06 +01:00
parent 793d2c79de
commit 4ce04e4749

View File

@@ -21,6 +21,10 @@ signature module InputSig<LocationSig Location, DF::InputSig<Location> Lang> {
string toString();
}
/** Holds if `c` is defined in source code. */
bindingset[c]
predicate callableFromSource(SummarizedCallableBase c);
/**
* A base class of elements that are candidates for flow source modeling.
*/
@@ -268,6 +272,9 @@ module Make<
this = verification and verification = "manual"
}
/** Gets the verification part of this provenance. */
string getVerification() { result = verification }
/**
* Holds if this is a valid generated provenance value.
*/
@@ -289,55 +296,42 @@ module Make<
*
* `preservesValue` indicates whether this is a value-preserving step or a taint-step.
*
* If `model` is non-empty then it indicates the provenance of the model
* defining this flow.
* `p` indicates the provenance of the flow.
*
* `isExact` indicates whether there exists a model for which this callable is an exact
* match, that is, no overriding was used to identify this callable from the model.
*
* If `model` is non-empty then it indicates the origin of the model defining this flow.
*/
pragma[nomagic]
abstract predicate propagatesFlow(
string input, string output, boolean preservesValue, string model
string input, string output, boolean preservesValue, Provenance p, boolean isExact,
string model
);
/**
* Holds if there exists a generated summary that applies to this callable.
*/
final predicate hasGeneratedModel() {
exists(Provenance p | p.isGenerated() and this.hasProvenance(p))
}
/**
* 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 applyGeneratedModel() {
this.hasGeneratedModel() and
not this.hasManualModel()
}
/**
* Holds if there exists a manual summary that applies to this callable.
*/
final predicate hasManualModel() {
exists(Provenance p | p.isManual() and this.hasProvenance(p))
any(Provenance p | this.propagatesFlow(_, _, _, p, _, _)).isManual()
}
}
/**
* Holds if there exists a manual summary that applies to this callable.
* Always apply manual models if they exist.
*/
final predicate applyManualModel() { this.hasManualModel() }
final private class SummarizedCallableFinal = SummarizedCallable;
/**
* Holds if there exists a summary that applies to this callable
* that has provenance `provenance`.
*/
predicate hasProvenance(Provenance provenance) { provenance = "manual" }
/**
* Holds if there exists a model for which this callable is an exact
* match, that is, no overriding was used to identify this callable from
* the model.
*/
predicate hasExactModel() { none() }
/**
* A callable with a relevant flow summary.
*
* A flow summary is relevant if:
*
* - It is manual exact model, or
* - It is a manual inexact model and there is no exact manual (neutral) model, or
* - It is a generated model and (a) there is no source code available for the modeled
* callable, (b) there is no manual (neutral) model, and (c) the model is inexact
* and there is no generated exact (neutral) model.
*/
final class RelevantSummarizedCallable extends SummarizedCallableFinal {
RelevantSummarizedCallable() { this instanceof SummarizedCallableImpl }
}
/** A source element. */
@@ -476,6 +470,41 @@ module Make<
module Private {
private import Public
/**
* Holds if `c` has a relevant flow summary.
*
* A flow summary is relevant if:
*
* - It is manual exact model, or
* - It is a manual inexact model and there is no exact manual (neutral) model, or
* - It is a generated model and (a) there is no source code available for the modeled
* callable, (b) there is no manual (neutral) model, and (c) the model is inexact
* and there is no generated exact (neutral) model.
*/
predicate relevantSummary(
SummarizedCallable c, string input, string output, boolean preservesValue, Provenance p,
boolean isExact, string model
) {
c.propagatesFlow(input, output, preservesValue, p, isExact, model) and
if p.isGenerated() or isExact = false
then
// Only apply generated models to functions in library code
not (p.isGenerated() and callableFromSource(c)) and
// Only apply generated or inexact models when no strictly better model exists
not exists(Provenance other, boolean isExactOther |
c.propagatesFlow(_, _, _, other, isExactOther, _)
or
neutralElement(c, "summary", other, isExactOther)
|
p.isGenerated() and other.isManual()
or
p.getVerification() = other.getVerification() and
isExact = false and
isExactOther = true
)
else any()
}
/**
* A synthetic global. This represents some form of global state, which
* summaries can read and write individually.
@@ -647,7 +676,7 @@ module Make<
SummarizedCallableImpl callable, SummaryComponentStack input, SummaryComponentStack output,
string whichOne
) {
callable.propagatesFlow(input, output, _, _) and
callable.propagatesFlow(input, output, _, _, _, _) and
(
not isSupportedInputStack(input) and whichOne = "input"
or
@@ -688,9 +717,9 @@ module Make<
private predicate summarySpec(string spec) {
exists(SummarizedCallable c |
c.propagatesFlow(spec, _, _, _)
c.propagatesFlow(spec, _, _, _, _, _)
or
c.propagatesFlow(_, spec, _, _)
c.propagatesFlow(_, spec, _, _, _, _)
)
or
isRelevantSource(_, spec, _, _, _)
@@ -848,7 +877,7 @@ module Make<
}
/**
* A callable with a flow summary.
* A callable with a relevant flow summary.
*
* This interface is not meant to be used directly, instead use the public
* `SummarizedCallable` interface. However, _if_ you need to use this, make
@@ -857,13 +886,9 @@ module Make<
*
* ```ql
* private class CAdapter extends SummarizedCallable instanceof C {
* override predicate propagatesFlow(string input, string output, boolean preservesValue, string model) {
* override predicate propagatesFlow(string input, string output, boolean preservesValue, Provenance p, string model) {
* none()
* }
*
* override predicate hasProvenance(Provenance provenance) {
* C.super.hasProvenance(provenance)
* }
* }
* ```
*/
@@ -897,14 +922,8 @@ module Make<
pragma[nomagic]
abstract predicate propagatesFlow(
SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue,
string model
Provenance p, boolean isExact, string model
);
/**
* Holds if there exists a summary that applies to this callable
* that has provenance `provenance`.
*/
abstract predicate hasProvenance(Provenance provenance);
}
pragma[nomagic]
@@ -912,17 +931,17 @@ module Make<
SummarizedCallableImpl c, SummaryComponentStack input, SummaryComponentStack output,
boolean preservesValue, string model
) {
c.propagatesFlow(input, output, preservesValue, model)
c.propagatesFlow(input, output, preservesValue, _, _, model)
or
// observe side effects of callbacks on input arguments
c.propagatesFlow(output, input, preservesValue, model) and
c.propagatesFlow(output, input, preservesValue, _, _, model) and
preservesValue = true and
isCallbackParameter(input) and
isContentOfArgument(output, _)
or
// flow from the receiver of a callback into the instance-parameter
exists(SummaryComponentStack s, SummaryComponentStack callbackRef |
c.propagatesFlow(s, _, _, model) or c.propagatesFlow(_, s, _, model)
c.propagatesFlow(s, _, _, _, _, model) or c.propagatesFlow(_, s, _, _, _, model)
|
callbackRef = s.drop(_) and
(isCallbackParameter(callbackRef) or callbackRef.head() = TReturnSummaryComponent(_)) and
@@ -948,8 +967,8 @@ module Make<
SummaryComponentStack mid, boolean preservesValue1, boolean preservesValue2, string model1,
string model2
|
c.propagatesFlow(input, mid, preservesValue1, model1) and
c.propagatesFlow(mid, output, preservesValue2, model2) and
c.propagatesFlow(input, mid, preservesValue1, _, _, model1) and
c.propagatesFlow(mid, output, preservesValue2, _, _, model2) and
mid.drop(mid.length() - 2) =
SummaryComponentStack::push(TParameterSummaryComponent(_),
SummaryComponentStack::singleton(TArgumentSummaryComponent(_))) and
@@ -2046,19 +2065,31 @@ module Make<
// adapter class for converting `SummarizedCallable`s to `SummarizedCallableImpl`s
private class SummarizedCallableImplAdapter extends SummarizedCallableImpl instanceof SummarizedCallable
{
override predicate propagatesFlow(
SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue,
string model
) {
private SummaryComponentStack input_;
private SummaryComponentStack output_;
private boolean preservesValue_;
private Provenance p_;
private boolean isExact_;
private string model_;
SummarizedCallableImplAdapter() {
exists(AccessPath inSpec, AccessPath outSpec |
SummarizedCallable.super.propagatesFlow(inSpec, outSpec, preservesValue, model) and
interpretSpec(inSpec, input) and
interpretSpec(outSpec, output)
relevantSummary(this, inSpec, outSpec, preservesValue_, p_, isExact_, model_) and
interpretSpec(inSpec, input_) and
interpretSpec(outSpec, output_)
)
}
override predicate hasProvenance(Provenance provenance) {
SummarizedCallable.super.hasProvenance(provenance)
override predicate propagatesFlow(
SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue,
Provenance p, boolean isExact, string model
) {
input = input_ and
output = output_ and
preservesValue = preservesValue_ and
p = p_ and
isExact = isExact_ and
model = model_
}
}
@@ -2492,12 +2523,13 @@ module Make<
string getCallableCsv();
predicate relevantSummary(
SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue
SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue,
Provenance p
);
}
/** Provides a query predicate for outputting a set of relevant flow summaries. */
module TestSummaryOutput<RelevantSummarizedCallableSig RelevantSummarizedCallable> {
module TestSummaryOutput<RelevantSummarizedCallableSig RelSummarizedCallable> {
/** Render the kind in the format used in flow summaries. */
private string renderKind(boolean preservesValue) {
preservesValue = true and result = "value"
@@ -2505,13 +2537,6 @@ module Make<
preservesValue = false and result = "taint"
}
private string renderProvenance(SummarizedCallable c) {
exists(Provenance p | p.isManual() and c.hasProvenance(p) and result = p.toString())
or
not c.applyManualModel() and
c.hasProvenance(result)
}
/**
* Holds if there exists a relevant summary callable with information roughly corresponding to `csv`.
* Used for testing.
@@ -2520,16 +2545,16 @@ module Make<
*/
query predicate summary(string csv) {
exists(
RelevantSummarizedCallable c, SummaryComponentStack input, SummaryComponentStack output,
boolean preservesValue
RelSummarizedCallable c, SummaryComponentStack input, SummaryComponentStack output,
boolean preservesValue, Provenance p
|
c.relevantSummary(input, output, preservesValue) and
c.relevantSummary(input, output, preservesValue, p) and
csv =
c.getCallableCsv() // Callable information
+ input.getMadRepresentation() + ";" // input
+ output.getMadRepresentation() + ";" // output
+ renderKind(preservesValue) + ";" // kind
+ renderProvenance(c) // provenance
+ p // provenance
)
}
}