🌐 AI搜索 & 代理 主页
Skip to content
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Java: Add support for boolean MaD barrier guards.
  • Loading branch information
aschackmull committed Dec 11, 2025
commit 6d4a86e533eed3b8738fce83c2e7e923a76f865b
66 changes: 65 additions & 1 deletion java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ module;

import java
private import semmle.code.java.dataflow.DataFlow::DataFlow
private import semmle.code.java.controlflow.Guards
private import FlowSummary as FlowSummary
private import internal.DataFlowPrivate
private import internal.FlowSummaryImpl
Expand Down Expand Up @@ -183,6 +184,15 @@ predicate barrierModel(
madId)
}

/** Holds if a barrier guard model exists for the given parameters. */
predicate barrierGuardModel(
string package, string type, boolean subtypes, string name, string signature, string ext,
string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
) {
Extensions::barrierGuardModel(package, type, subtypes, name, signature, ext, input,
acceptingvalue, kind, provenance, madId)
}

/** Holds if a summary model exists for the given parameters. */
predicate summaryModel(
string package, string type, boolean subtypes, string name, string signature, string ext,
Expand Down Expand Up @@ -315,7 +325,8 @@ module ModelValidation {
summaryModel(_, _, _, _, _, _, _, path, _, _, _) or
sinkModel(_, _, _, _, _, _, path, _, _, _) or
sourceModel(_, _, _, _, _, _, path, _, _, _) or
barrierModel(_, _, _, _, _, _, path, _, _, _)
barrierModel(_, _, _, _, _, _, path, _, _, _) or
barrierGuardModel(_, _, _, _, _, _, path, _, _, _, _)
}

private module MkAccessPath = AccessPathSyntax::AccessPath<getRelevantAccessPath/1>;
Expand All @@ -328,6 +339,8 @@ module ModelValidation {
exists(string pred, AccessPath input, AccessPathToken part |
sinkModel(_, _, _, _, _, _, input, _, _, _) and pred = "sink"
or
barrierGuardModel(_, _, _, _, _, _, input, _, _, _, _) and pred = "barrier guard"
or
summaryModel(_, _, _, _, _, _, input, _, _, _, _) and pred = "summary"
|
(
Expand Down Expand Up @@ -373,6 +386,8 @@ module ModelValidation {
sinkModel(_, _, _, _, _, _, _, kind, _, _)
or
barrierModel(_, _, _, _, _, _, _, kind, _, _)
or
barrierGuardModel(_, _, _, _, _, _, _, _, kind, _, _)
}

predicate sourceKind(string kind) { sourceModel(_, _, _, _, _, _, _, kind, _, _) }
Expand All @@ -393,6 +408,9 @@ module ModelValidation {
or
barrierModel(package, type, _, name, signature, ext, _, _, provenance, _) and pred = "barrier"
or
barrierGuardModel(package, type, _, name, signature, ext, _, _, _, provenance, _) and
pred = "barrier guard"
or
summaryModel(package, type, _, name, signature, ext, _, _, _, provenance, _) and
pred = "summary"
or
Expand All @@ -418,6 +436,14 @@ module ModelValidation {
invalidProvenance(provenance) and
result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
)
or
exists(string acceptingvalue |
barrierGuardModel(_, _, _, _, _, _, _, acceptingvalue, _, _, _) and
invalidAcceptingValue(acceptingvalue) and
result =
"Unrecognized accepting value description \"" + acceptingvalue +
"\" in barrier guard model."
)
}

/** Holds if some row in a MaD flow model appears to contain typos. */
Expand All @@ -440,6 +466,8 @@ private predicate elementSpec(
or
barrierModel(package, type, subtypes, name, signature, ext, _, _, _, _)
or
barrierGuardModel(package, type, subtypes, name, signature, ext, _, _, _, _, _)
or
summaryModel(package, type, subtypes, name, signature, ext, _, _, _, _, _)
or
neutralModel(package, type, name, signature, _, _) and ext = "" and subtypes = true
Expand Down Expand Up @@ -601,6 +629,39 @@ private module Cached {
)
}

private newtype TKindModelPair =
TMkPair(string kind, string model) { isBarrierGuardNode(_, _, kind, model) }

private GuardValue convertAcceptingValue(AcceptingValue av) {
av.isTrue() and result.asBooleanValue() = true
or
av.isFalse() and result.asBooleanValue() = false
or
av.isNoException() and result.getDualValue().isThrowsException()
or
av.isZero() and result.asIntValue() = 0
or
av.isNotZero() and result.getDualValue().asIntValue() = 0
or
av.isNull() and result.isNullValue()
or
av.isNotNull() and result.isNonNullValue()
}

private predicate barrierGuardChecks(Guard g, Expr e, GuardValue gv, TKindModelPair kmp) {
exists(
SourceSinkInterpretationInput::InterpretNode n, AcceptingValue acceptingvalue, string kind,
string model
|
isBarrierGuardNode(n, acceptingvalue, kind, model) and
n.asNode().asExpr() = e and
kmp = TMkPair(kind, model) and
gv = convertAcceptingValue(acceptingvalue)
|
g.(Call).getAnArgument() = e or g.(MethodCall).getQualifier() = e
)
}

/**
* Holds if `node` is specified as a barrier with the given kind in a MaD flow
* model.
Expand All @@ -610,6 +671,9 @@ private module Cached {
exists(SourceSinkInterpretationInput::InterpretNode n |
isBarrierNode(n, kind, model) and n.asNode() = node
)
or
ParameterizedBarrierGuard<TKindModelPair, barrierGuardChecks/4>::getABarrierNode(TMkPair(kind,
model)) = node
}
}

Expand Down
28 changes: 28 additions & 0 deletions java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll
Original file line number Diff line number Diff line change
Expand Up @@ -420,3 +420,31 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
/** Gets a node that is safely guarded by the given guard check. */
Node getABarrierNode() { result = BarrierGuardValue<guardChecks0/3>::getABarrierNode() }
}

bindingset[this]
private signature class ParamSig;

private module WithParam<ParamSig P> {
/**
* Holds if the guard `g` validates the expression `e` upon evaluating to `gv`.
*
* The expression `e` is expected to be a syntactic part of the guard `g`.
* For example, the guard `g` might be a call `isSafe(x)` and the expression `e`
* the argument `x`.
*/
signature predicate guardChecksSig(Guard g, Expr e, GuardValue gv, P param);
}

/**
* Provides a set of barrier nodes for a guard that validates an expression.
*
* This is expected to be used in `isBarrier`/`isSanitizer` definitions
* in data flow and taint tracking.
*/
module ParameterizedBarrierGuard<ParamSig P, WithParam<P>::guardChecksSig/4 guardChecks> {
/** Gets a node that is safely guarded by the given guard check. */
Node getABarrierNode(P param) {
SsaFlow::asNode(result) =
SsaImpl::DataFlowIntegration::ParameterizedBarrierGuard<P, guardChecks/4>::getABarrierNode(param)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,14 @@ extensible predicate barrierModel(
string output, string kind, string provenance, QlBuiltins::ExtensionId madId
);

/**
* Holds if a barrier guard model exists for the given parameters.
*/
extensible predicate barrierGuardModel(
string package, string type, boolean subtypes, string name, string signature, string ext,
string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
);

/**
* Holds if a summary model exists for the given parameters.
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,8 @@ private predicate relatedArgSpec(Callable c, string spec) {
summaryModel(namespace, type, subtypes, name, signature, ext, _, spec, _, _, _) or
sourceModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _) or
sinkModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _) or
barrierModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _)
barrierModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _) or
barrierGuardModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _, _)
|
c = interpretElement(namespace, type, subtypes, name, signature, ext, _)
)
Expand Down Expand Up @@ -267,8 +268,28 @@ module SourceSinkInterpretationInput implements
string namespace, string type, boolean subtypes, string name, string signature, string ext,
SourceOrSinkElement baseBarrier, string originalOutput, QlBuiltins::ExtensionId madId
|
barrierModel(namespace, type, subtypes, name, signature, ext, originalOutput, kind, provenance,
madId) and
barrierModel(namespace, type, subtypes, name, signature, ext, originalOutput, kind,
provenance, madId) and
model = "MaD:" + madId.toString() and
baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and
(
e = baseBarrier and output = originalOutput
or
correspondingKotlinParameterDefaultsArgSpec(baseBarrier, e, originalOutput, output)
)
)
}

predicate barrierGuardElement(
Element e, string output, Public::AcceptingValue acceptingvalue, string kind,
Public::Provenance provenance, string model
) {
exists(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
SourceOrSinkElement baseBarrier, string originalOutput, QlBuiltins::ExtensionId madId
|
barrierGuardModel(namespace, type, subtypes, name, signature, ext, originalOutput,
acceptingvalue, kind, provenance, madId) and
model = "MaD:" + madId.toString() and
baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and
(
Expand Down
30 changes: 30 additions & 0 deletions java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -588,6 +588,36 @@ private module Cached {

predicate getABarrierNode = getABarrierNodeImpl/0;
}

bindingset[this]
private signature class ParamSig;

private module WithParam<ParamSig P> {
signature predicate guardChecksSig(Guards::Guard g, Expr e, Guards::GuardValue gv, P param);
}

cached // nothing is actually cached
module ParameterizedBarrierGuard<ParamSig P, WithParam<P>::guardChecksSig/4 guardChecks> {
private predicate guardChecksAdjTypes(
Guards::Guards_v3::Guard g, Expr e, Guards::GuardValue gv, P param
) {
guardChecks(g, e, gv, param)
}

private predicate guardChecksWithWrappers(
DataFlowIntegrationInput::Guard g, Definition def, Guards::GuardValue val, P param
) {
Guards::Guards_v3::ParameterizedValidationWrapper<P, guardChecksAdjTypes/4>::guardChecksDef(g,
def, val, param)
}

private Node getABarrierNodeImpl(P param) {
result =
DataFlowIntegrationImpl::BarrierGuardDefWithState<P, guardChecksWithWrappers/4>::getABarrierNode(param)
}

predicate getABarrierNode = getABarrierNodeImpl/1;
}
}

cached
Expand Down
74 changes: 72 additions & 2 deletions shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -215,6 +215,35 @@ module Make<
]
}

class AcceptingValue extends string {
AcceptingValue() {
this =
[
"true",
"false",
"no-exception",
"zero",
"not-zero",
"null",
"not-null",
]
}

predicate isTrue() { this = "true" }

predicate isFalse() { this = "false" }

predicate isNoException() { this = "no-exception" }

predicate isZero() { this = "zero" }

predicate isNotZero() { this = "not-zero" }

predicate isNull() { this = "null" }

predicate isNotNull() { this = "not-null" }
}

/**
* A class used to represent provenance values for MaD models.
*
Expand Down Expand Up @@ -2015,6 +2044,12 @@ module Make<
not exists(interpretComponent(c))
}

/** Holds if `acceptingvalue` is not a valid barrier guard accepting-value. */
bindingset[acceptingvalue]
predicate invalidAcceptingValue(string acceptingvalue) {
not acceptingvalue instanceof AcceptingValue
}

/** Holds if `provenance` is not a valid provenance value. */
bindingset[provenance]
predicate invalidProvenance(string provenance) { not provenance instanceof Provenance }
Expand Down Expand Up @@ -2060,6 +2095,15 @@ module Make<
Element n, string output, string kind, Provenance provenance, string model
);

/**
* Holds if an external barrier guard specification exists for `n` with input
* specification `input`, accepting value `acceptingvalue`, and kind `kind`.
*/
predicate barrierGuardElement(
Element n, string input, AcceptingValue acceptingvalue, string kind,
Provenance provenance, string model
);

class SourceOrSinkElement extends Element;

/** An entity used to interpret a source/sink specification. */
Expand Down Expand Up @@ -2114,7 +2158,8 @@ module Make<
private predicate sourceSinkSpec(string spec) {
sourceElement(_, spec, _, _, _) or
sinkElement(_, spec, _, _, _) or
barrierElement(_, spec, _, _, _)
barrierElement(_, spec, _, _, _) or
barrierGuardElement(_, spec, _, _, _, _)
}

private module AccessPath = AccessPathSyntax::AccessPath<sourceSinkSpec/1>;
Expand Down Expand Up @@ -2180,6 +2225,18 @@ module Make<
)
}

private predicate barrierGuardElementRef(
InterpretNode ref, SourceSinkAccessPath input, AcceptingValue acceptingvalue, string kind,
string model
) {
exists(SourceOrSinkElement e |
barrierGuardElement(e, input, acceptingvalue, kind, _, model) and
if inputNeedsReferenceExt(input.getToken(0))
then e = ref.getCallTarget()
else e = ref.asElement()
)
}

/** Holds if the first `n` tokens of `output` resolve to the given interpretation. */
private predicate interpretOutput(
SourceSinkAccessPath output, int n, InterpretNode ref, InterpretNode node
Expand Down Expand Up @@ -2240,7 +2297,7 @@ module Make<
private predicate interpretInput(
SourceSinkAccessPath input, int n, InterpretNode ref, InterpretNode node
) {
sinkElementRef(ref, input, _, _) and
(sinkElementRef(ref, input, _, _) or barrierGuardElementRef(ref, input, _, _, _)) and
n = 0 and
(
if input = ""
Expand Down Expand Up @@ -2311,6 +2368,19 @@ module Make<
)
}

/**
* Holds if `node` is specified as a barrier guard argument with the
* given kind in a MaD flow model.
*/
predicate isBarrierGuardNode(
InterpretNode node, AcceptingValue acceptingvalue, string kind, string model
) {
exists(InterpretNode ref, SourceSinkAccessPath input |
barrierGuardElementRef(ref, input, acceptingvalue, kind, model) and
interpretInput(input, input.getNumToken(), ref, node)
)
}

final private class SourceOrSinkElementFinal = SourceOrSinkElement;

signature predicate sourceOrSinkElementSig(
Expand Down