Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SSA: Add BarrierGuardWithState #17661

Merged
merged 2 commits into from
Oct 8, 2024
Merged
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
48 changes: 44 additions & 4 deletions shared/ssa/codeql/ssa/Ssa.qll
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
*/

private import codeql.util.Location
private import codeql.util.Unit

/** Provides the input specification of the SSA implementation. */
signature module InputSig<LocationSig Location> {
Expand Down Expand Up @@ -1631,23 +1632,62 @@ module Make<LocationSig Location, InputSig<Location> Input> {
)
}

bindingset[this]
signature class StateSig;

module WithState<StateSig State> {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Private

/**
* Holds if the guard `g` validates the expression `e` upon evaluating to `branch`, blocking
* flow in the given `state`.
*
* 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(
DfInput::Guard g, DfInput::Expr e, boolean branch, State state
);
}

/**
* 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 BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksWithState(
DfInput::Guard g, DfInput::Expr e, boolean branch, Unit state
) {
guardChecks(g, e, branch) and exists(state)
}

private module StatefulBarrier = BarrierGuardWithState<Unit, guardChecksWithState/4>;

/** Gets a node that is safely guarded by the given guard check. */
pragma[nomagic]
Node getABarrierNode() { result = StatefulBarrier::getABarrierNode(_) }
}

/**
* 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 BarrierGuardWithState<StateSig State, WithState<State>::guardChecksSig/4 guardChecks> {
pragma[nomagic]
private predicate guardChecksSsaDef(DfInput::Guard g, Definition def, boolean branch) {
guardChecks(g, DfInput::getARead(def), branch)
private predicate guardChecksSsaDef(
DfInput::Guard g, Definition def, boolean branch, State state
) {
guardChecks(g, DfInput::getARead(def), branch, state)
}

/** Gets a node that is safely guarded by the given guard check. */
pragma[nomagic]
Node getABarrierNode() {
Node getABarrierNode(State state) {
exists(DfInput::Guard g, boolean branch, Definition def, BasicBlock bb |
guardChecksSsaDef(g, def, branch)
guardChecksSsaDef(g, def, branch, state)
|
// guard controls a read
exists(DfInput::Expr e |
Expand Down
Loading