Merge pull request #4251 from yoff/SharedDataflow_BarrierGuards

Python: Implement `BarrierGuard`

Author: RasmusWL

python/ql/src/experimental/dataflow/internal/DataFlowPrivate.qll

@@ -130,7 +130,7 @@ module EssaFlow {
   }
 
   predicate useToNextUse(NameNode nodeFrom, NameNode nodeTo) {
-    AdjacentUses::adjacentUseUseSameVar(nodeFrom, nodeTo)
+    AdjacentUses::adjacentUseUse(nodeFrom, nodeTo)
   }
 
   predicate defToFirstUse(EssaVariable var, NameNode nodeTo) {

python/ql/src/experimental/dataflow/internal/DataFlowPublic.qll

@@ -5,6 +5,7 @@
 private import python
 private import DataFlowPrivate
 import experimental.dataflow.TypeTracker
+private import semmle.python.essa.SsaCompute
 
 /**
  * IPA type for data flow nodes.
@@ -148,6 +149,18 @@ class ParameterNode extends EssaNode {
   override DataFlowCallable getEnclosingCallable() { this.isParameterOf(result, _) }
 }
 
+/**
+ * A node that controls whether other nodes are evaluated.
+ */
+class GuardNode extends ControlFlowNode {
+  ConditionBlock conditionBlock;
+
+  GuardNode() { this = conditionBlock.getLastNode() }
+
+  /** Holds if this guard controls block `b` upon evaluating to `branch`. */
+  predicate controlsBlock(BasicBlock b, boolean branch) { conditionBlock.controls(b, branch) }
+}
+
 /**
  * A guard that validates some expression.
  *
@@ -157,16 +170,18 @@ class ParameterNode extends EssaNode {
  *
  * It is important that all extending classes in scope are disjoint.
  */
-class BarrierGuard extends Expr {
-  // /** Holds if this guard validates `e` upon evaluating to `v`. */
-  // abstract predicate checks(Expr e, AbstractValue v);
+class BarrierGuard extends GuardNode {
+  /** Holds if this guard validates `node` upon evaluating to `branch`. */
+  abstract predicate checks(ControlFlowNode node, boolean branch);
+
   /** Gets a node guarded by this guard. */
   final ExprNode getAGuardedNode() {
-    none()
-    // exists(Expr e, AbstractValue v |
-    //   this.checks(e, v) and
-    //   this.controlsNode(result.getControlFlowNode(), e, v)
-    // )
+    exists(EssaDefinition def, ControlFlowNode node, boolean branch |
+      AdjacentUses::useOfDef(def, node) and
+      this.checks(node, branch) and
+      AdjacentUses::useOfDef(def, result.asCfgNode()) and
+      this.controlsBlock(result.asCfgNode().getBasicBlock(), branch)
+    )
   }
 }
 

python/ql/src/semmle/python/essa/SsaCompute.qll

@@ -443,9 +443,28 @@ private module SsaComputeImpl {
       )
     }
 
+    /**
+     * Holds if `use1` and `use2` form an adjacent use-use-pair of the same
+     * `SsaSourceVariable`, that is, the value read in `use1` can reach `use2`
+     * without passing through any other use or any SSA definition of the variable
+     * except for phi nodes.
+     */
+    cached
+    predicate adjacentUseUse(ControlFlowNode use1, ControlFlowNode use2) {
+      adjacentUseUseSameVar(use1, use2)
+      or
+      exists(SsaSourceVariable v, EssaDefinition def, BasicBlock b1, int i1, BasicBlock b2, int i2 |
+        adjacentVarRefs(v, b1, i1, b2, i2) and
+        variableUse(v, use1, b1, i1) and
+        definesAt(def, v, b2, i2) and
+        firstUse(def, use2) and
+        def instanceof PhiFunction
+      )
+    }
+
     /**
      * Holds if the value defined at `def` can reach `use` without passing through
-     * any other uses, but possibly through phi nodes and uncertain implicit updates.
+     * any other uses, but possibly through phi nodes.
      */
     cached
     predicate firstUse(EssaDefinition def, ControlFlowNode use) {
@@ -482,6 +501,17 @@ private module SsaComputeImpl {
       b = def.(PhiFunction).getBasicBlock() and
       i = -1
     }
+
+    /**
+     * Holds if the value defined at `def` can reach `use`, possibly through phi nodes.
+     */
+    cached
+    predicate useOfDef(EssaDefinition def, ControlFlowNode use) {
+      exists(ControlFlowNode firstUse |
+        firstUse(def, firstUse) and
+        adjacentUseUse*(firstUse, use)
+      )
+    }
   }
 }
 

python/ql/test/experimental/dataflow/tainttracking/customSanitizer/TestTaint.expected

@@ -1,9 +1,11 @@
 test_taint
 | test.py:22 | ok   | test_custom_sanitizer | s |
-| test.py:36 | fail | test_custom_sanitizer_guard | s |
+| test.py:36 | ok   | test_custom_sanitizer_guard | s |
 | test.py:38 | ok   | test_custom_sanitizer_guard | s |
-| test.py:49 | ok   | test_escape | s2 |
+| test.py:40 | ok   | test_custom_sanitizer_guard | s |
+| test.py:51 | ok   | test_escape | s2 |
 isSanitizer
 | TestTaintTrackingConfiguration | test.py:21:39:21:39 | ControlFlowNode for s |
-| TestTaintTrackingConfiguration | test.py:48:10:48:29 | ControlFlowNode for emulated_escaping() |
+| TestTaintTrackingConfiguration | test.py:50:10:50:29 | ControlFlowNode for emulated_escaping() |
 isSanitizerGuard
+| TestTaintTrackingConfiguration | test.py:35:8:35:26 | ControlFlowNode for emulated_is_safe() |

python/ql/test/experimental/dataflow/tainttracking/customSanitizer/TestTaint.ql

@@ -1,5 +1,14 @@
 import experimental.dataflow.tainttracking.TestTaintLib
 
+class IsSafeCheck extends DataFlow::BarrierGuard {
+  IsSafeCheck() { this.(CallNode).getNode().getFunc().(Name).getId() = "emulated_is_safe" }
+
+  override predicate checks(ControlFlowNode node, boolean branch) {
+    node = this.(CallNode).getAnArg() and
+    branch = true
+  }
+}
+
 class CustomSanitizerOverrides extends TestTaintTrackingConfiguration {
   override predicate isSanitizer(DataFlow::Node node) {
     exists(Call call |
@@ -10,13 +19,7 @@ class CustomSanitizerOverrides extends TestTaintTrackingConfiguration {
     node.asExpr().(Call).getFunc().(Name).getId() = "emulated_escaping"
   }
 
-  override predicate isSanitizerGuard(DataFlow::BarrierGuard guard) {
-    // TODO: Future work for when BarrierGuard is implemented properly
-    // exists(Call call |
-    //   call.getFunc().(Name).getId() = "emulated_is_safe" and
-    // )
-    none()
-  }
+  override predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { guard instanceof IsSafeCheck }
 }
 
 query predicate isSanitizer(TestTaintTrackingConfiguration conf, DataFlow::Node node) {

python/ql/test/experimental/dataflow/tainttracking/customSanitizer/test.py

@@ -34,6 +34,8 @@ def test_custom_sanitizer_guard():
 
     if emulated_is_safe(s):
         ensure_not_tainted(s)
+        s = TAINTED_STRING
+        ensure_tainted(s)
     else:
         ensure_tainted(s)
 

python/ql/test/experimental/meta/debug/dataflow.qll

@@ -0,0 +1,18 @@
+import experimental.dataflow.tainttracking.TestTaintLib
+
+query predicate sanitizerGuardControls(
+  TestTaintTrackingConfiguration conf, DataFlow::BarrierGuard guard, ControlFlowNode node,
+  boolean branch
+) {
+  exists(guard.getLocation().getFile().getRelativePath()) and
+  conf.isSanitizerGuard(guard) and
+  guard.controlsBlock(node.getBasicBlock(), branch)
+}
+
+query predicate sanitizerGuardedNode(
+  TestTaintTrackingConfiguration conf, DataFlow::BarrierGuard guard, DataFlow::ExprNode node
+) {
+  exists(guard.getLocation().getFile().getRelativePath()) and
+  conf.isSanitizerGuard(guard) and
+  node = guard.getAGuardedNode()
+}