@@ -83,11 +83,9 @@ class AdditionalTaintStep extends Unit {
8383 abstract predicate step ( DataFlow:: Node node1 , DataFlow:: Node node2 ) ;
8484}
8585
86- /**
87- * Holds if the additional step from `pred` to `succ` should be included in all
88- * global taint flow configurations.
89- */
90- predicate localAdditionalTaintStep ( DataFlow:: Node pred , DataFlow:: Node succ , string model ) {
86+ private predicate localAdditionalForwardTaintStep (
87+ DataFlow:: Node pred , DataFlow:: Node succ , string model
88+ ) {
9189 exists ( DataFlow:: Node pred2 |
9290 pred2 = pred
9391 or
@@ -103,14 +101,45 @@ predicate localAdditionalTaintStep(DataFlow::Node pred, DataFlow::Node succ, str
103101 ) and
104102 model = ""
105103 or
106- any ( FunctionModel fm ) .taintStep ( pred , succ ) and model = "FunctionModel"
104+ any ( FunctionModel fm ) .forwardTaintStep ( pred , succ ) and model = "FunctionModel"
107105 or
108106 any ( AdditionalTaintStep a ) .step ( pred , succ ) and model = "AdditionalTaintStep"
109107 or
110108 FlowSummaryImpl:: Private:: Steps:: summaryLocalStep ( pred .( DataFlowPrivate:: FlowSummaryNode )
111109 .getSummaryNode ( ) , succ .( DataFlowPrivate:: FlowSummaryNode ) .getSummaryNode ( ) , false , model )
112110}
113111
112+ private predicate localForwardTaintStep ( DataFlow:: Node pred , DataFlow:: Node succ ) {
113+ DataFlow:: localFlow ( pred , succ ) or
114+ localAdditionalForwardTaintStep ( pred , succ , _) or
115+ // Simple flow through library code is included in the exposed local
116+ // step relation, even though flow is technically inter-procedural
117+ FlowSummaryImpl:: Private:: Steps:: summaryThroughStepTaint ( pred , succ , _)
118+ }
119+
120+ /**
121+ * Holds if taint flows backwards from `pred` to `succ` via a function model.
122+ */
123+ private predicate localAdditionalBackwardTaintStep (
124+ DataFlow:: Node pred , DataFlow:: Node succ , string model
125+ ) {
126+ // backward step through function model
127+ exists ( FunctionModel m , DataFlow:: Node resultNode |
128+ m .backwardTaintStep ( resultNode , succ ) and
129+ localForwardTaintStep + ( resultNode , pred .( DataFlow:: PostUpdateNode ) .getPreUpdateNode ( ) )
130+ ) and
131+ model = "FunctionModel"
132+ }
133+
134+ /**
135+ * Holds if the additional step from `pred` to `succ` should be included in all
136+ * global taint flow configurations.
137+ */
138+ predicate localAdditionalTaintStep ( DataFlow:: Node pred , DataFlow:: Node succ , string model ) {
139+ localAdditionalForwardTaintStep ( pred , succ , model ) or
140+ localAdditionalBackwardTaintStep ( pred , succ , model )
141+ }
142+
114143/**
115144 * Holds if taint flows from `pred` to `succ` via a reference or dereference.
116145 *
@@ -199,23 +228,36 @@ abstract class FunctionModel extends Function {
199228 abstract predicate hasTaintFlow ( FunctionInput input , FunctionOutput output ) ;
200229
201230 /** Gets an input node for this model for the call `c`. */
202- DataFlow:: Node getAnInputNode ( DataFlow:: CallNode c ) { this .taintStepForCall ( result , _, c ) }
231+ DataFlow:: Node getAnInputNode ( DataFlow:: CallNode c ) { this .taintStepForCall ( result , _, c , _ ) }
203232
204233 /** Gets an output node for this model for the call `c`. */
205- DataFlow:: Node getAnOutputNode ( DataFlow:: CallNode c ) { this .taintStepForCall ( _, result , c ) }
234+ DataFlow:: Node getAnOutputNode ( DataFlow:: CallNode c ) { this .taintStepForCall ( _, result , c , _ ) }
206235
207236 /** Holds if this function model causes taint to flow from `pred` to `succ` for the call `c`. */
208- predicate taintStepForCall ( DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: CallNode c ) {
237+ predicate taintStepForCall (
238+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: CallNode c , Boolean forward
239+ ) {
209240 c = this .getACall ( ) and
210241 exists ( FunctionInput inp , FunctionOutput outp | this .hasTaintFlow ( inp , outp ) |
211242 pred = pragma [ only_bind_out ] ( inp ) .getNode ( c ) and
212- succ = pragma [ only_bind_out ] ( outp ) .getNode ( c )
243+ succ = pragma [ only_bind_out ] ( outp ) .getNode ( c ) and
244+ if inp .isResult ( ) or inp .isResult ( _) then forward = false else forward = true
213245 )
214246 }
215247
216248 /** Holds if this function model causes taint to flow from `pred` to `succ`. */
217249 predicate taintStep ( DataFlow:: Node pred , DataFlow:: Node succ ) {
218- this .taintStepForCall ( pred , succ , _)
250+ this .taintStepForCall ( pred , succ , _, _)
251+ }
252+
253+ /** Holds if this function model causes taint to flow forward from `pred` to `succ`. */
254+ predicate forwardTaintStep ( DataFlow:: Node pred , DataFlow:: Node succ ) {
255+ this .taintStepForCall ( pred , succ , _, true )
256+ }
257+
258+ /** Holds if this function model causes taint to flow backwards from `pred` to `succ`. */
259+ predicate backwardTaintStep ( DataFlow:: Node pred , DataFlow:: Node succ ) {
260+ this .taintStepForCall ( pred , succ , _, false )
219261 }
220262}
221263
0 commit comments