@@ -601,16 +601,22 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
601
601
* observed in a similarly synthesized post-update node for this read of `v`.
602
602
*/
603
603
private predicate synthRead (
604
- CapturedVariable v , BasicBlock bb , int i , boolean topScope , Expr closure
604
+ CapturedVariable v , BasicBlock bb , int i , boolean topScope , Expr closure , boolean alias
605
605
) {
606
606
exists ( ClosureExpr ce | closureCaptures ( ce , v ) |
607
- ce .hasCfgNode ( bb , i ) and ce = closure
607
+ ce .hasCfgNode ( bb , i ) and ce = closure and alias = false
608
608
or
609
- localOrNestedClosureAccess ( ce , closure , bb , i )
609
+ localOrNestedClosureAccess ( ce , closure , bb , i ) and alias = true
610
610
) and
611
611
if v .getCallable ( ) != bb .getEnclosingCallable ( ) then topScope = false else topScope = true
612
612
}
613
613
614
+ private predicate synthRead (
615
+ CapturedVariable v , BasicBlock bb , int i , boolean topScope , Expr closure
616
+ ) {
617
+ synthRead ( v , bb , i , topScope , closure , _)
618
+ }
619
+
614
620
/**
615
621
* Holds if there is an access of a captured variable inside a closure in the
616
622
* `i`th node of `bb`, such that we need to synthesize a `this.` qualifier.
@@ -919,16 +925,22 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
919
925
)
920
926
}
921
927
922
- predicate storeStep ( ClosureNode node1 , CapturedVariable v , ClosureNode node2 ) {
923
- // store v in the closure or in the malloc in case of a relevant constructor call
928
+ private predicate storeStepClosure (
929
+ ClosureNode node1 , CapturedVariable v , ClosureNode node2 , boolean alias
930
+ ) {
924
931
exists ( BasicBlock bb , int i , Expr closure |
925
- synthRead ( v , bb , i , _, closure ) and
932
+ synthRead ( v , bb , i , _, closure , alias ) and
926
933
node1 = TSynthRead ( v , bb , i , false )
927
934
|
928
935
node2 = TExprNode ( closure , false )
929
936
or
930
937
node2 = TMallocNode ( closure ) and hasConstructorCapture ( closure , v )
931
938
)
939
+ }
940
+
941
+ predicate storeStep ( ClosureNode node1 , CapturedVariable v , ClosureNode node2 ) {
942
+ // store v in the closure or in the malloc in case of a relevant constructor call
943
+ storeStepClosure ( node1 , v , node2 , _)
932
944
or
933
945
// write to v inside the closure body
934
946
exists ( BasicBlock bb , int i , VariableWrite vw |
@@ -964,6 +976,62 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
964
976
}
965
977
966
978
predicate clearsContent ( ClosureNode node , CapturedVariable v ) {
979
+ /*
980
+ * Stores into closure aliases block flow from previous stores, both to
981
+ * avoid overlapping data flow paths, but also to avoid false positive
982
+ * flow.
983
+ *
984
+ * Example 1 (overlapping paths):
985
+ *
986
+ * ```rb
987
+ * def m
988
+ * x = taint
989
+ *
990
+ * fn = -> { # (1)
991
+ * sink x
992
+ * }
993
+ *
994
+ * fn.call # (2)
995
+ * ```
996
+ *
997
+ * If we don't clear `x` at `fn` (2), we will have two overlapping paths:
998
+ *
999
+ * ```
1000
+ * taint -> fn (2) [captured x]
1001
+ * taint -> fn (1) [captured x] -> fn (2) [captured x]
1002
+ * ```
1003
+ *
1004
+ * where the step `fn (1) [captured x] -> fn [captured x]` arises from normal
1005
+ * use-use flow for `fn`. Clearing `x` at `fn` (2) removes the second path above.
1006
+ *
1007
+ * Example 2 (false positive flow):
1008
+ *
1009
+ * ```rb
1010
+ * def m
1011
+ * x = taint
1012
+ *
1013
+ * fn = -> { # (1)
1014
+ * sink x
1015
+ * }
1016
+ *
1017
+ * x = nil # (2)
1018
+ *
1019
+ * fn.call # (3)
1020
+ * end
1021
+ * ```
1022
+ *
1023
+ * If we don't clear `x` at `fn` (3), we will have the following false positive
1024
+ * flow path:
1025
+ *
1026
+ * ```
1027
+ * taint -> fn (1) [captured x] -> fn (3) [captured x]
1028
+ * ```
1029
+ *
1030
+ * since normal use-use flow for `fn` does not take the overwrite at (2) into account.
1031
+ */
1032
+
1033
+ storeStepClosure ( _, v , node , true )
1034
+ or
967
1035
exists ( BasicBlock bb , int i |
968
1036
captureWrite ( v , bb , i , false , _) and
969
1037
node = TSynthThisQualifier ( bb , i , false )
0 commit comments