C#: Add BarrierGuard parameterised module.

This commit is contained in:
Anders Schack-Mulligen
2022-06-15 14:51:03 +02:00
parent 6518a01ded
commit 456f02fd82

View File

@@ -173,6 +173,33 @@ abstract class NonLocalJumpNode extends Node {
}
/**
* Holds if the guard `g` validates the expression `e` upon evaluating to `v`.
*
* 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, AbstractValue v);
/**
* 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> {
/** Gets a node that is safely guarded by the given guard check. */
ExprNode getABarrierNode() {
exists(Guard g, Expr e, AbstractValue v |
guardChecks(g, e, v) and
g.controlsNode(result.getControlFlowNode(), e, v)
)
}
}
/**
* DEPRECATED: Use `BarrierGuard` module instead.
*
* A guard that validates some expression.
*
* To use this in a configuration, extend the class and provide a
@@ -181,7 +208,7 @@ abstract class NonLocalJumpNode extends Node {
*
* It is important that all extending classes in scope are disjoint.
*/
class BarrierGuard extends Guard {
deprecated class BarrierGuard extends Guard {
/** Holds if this guard validates `e` upon evaluating to `v`. */
abstract predicate checks(Expr e, AbstractValue v);