Fix backwards flow through TaintTracking::FunctionModel

We only do this for taint models as there isn't any backwards flow
through data flow function models.
This commit is contained in:
Owen Mansel-Chan
2025-09-23 22:06:42 +01:00
parent 3906f2560d
commit 5efc8ac1a4
3 changed files with 71 additions and 32 deletions

View File

@@ -83,11 +83,9 @@ class AdditionalTaintStep extends Unit {
abstract predicate step(DataFlow::Node node1, DataFlow::Node node2);
}
/**
* Holds if the additional step from `pred` to `succ` should be included in all
* global taint flow configurations.
*/
predicate localAdditionalTaintStep(DataFlow::Node pred, DataFlow::Node succ, string model) {
private predicate localAdditionalForwardTaintStep(
DataFlow::Node pred, DataFlow::Node succ, string model
) {
exists(DataFlow::Node pred2 |
pred2 = pred
or
@@ -103,7 +101,7 @@ predicate localAdditionalTaintStep(DataFlow::Node pred, DataFlow::Node succ, str
) and
model = ""
or
any(FunctionModel fm).taintStep(pred, succ) and model = "FunctionModel"
any(FunctionModel fm).forwardTaintStep(pred, succ) and model = "FunctionModel"
or
any(AdditionalTaintStep a).step(pred, succ) and model = "AdditionalTaintStep"
or
@@ -111,6 +109,37 @@ predicate localAdditionalTaintStep(DataFlow::Node pred, DataFlow::Node succ, str
.getSummaryNode(), succ.(DataFlowPrivate::FlowSummaryNode).getSummaryNode(), false, model)
}
private predicate localForwardTaintStep(DataFlow::Node pred, DataFlow::Node succ) {
DataFlow::localFlow(pred, succ) or
localAdditionalForwardTaintStep(pred, succ, _) or
// Simple flow through library code is included in the exposed local
// step relation, even though flow is technically inter-procedural
FlowSummaryImpl::Private::Steps::summaryThroughStepTaint(pred, succ, _)
}
/**
* Holds if taint flows backwards from `pred` to `succ` via a function model.
*/
private predicate localAdditionalBackwardTaintStep(
DataFlow::Node pred, DataFlow::Node succ, string model
) {
// backward step through function model
exists(FunctionModel m, DataFlow::Node resultNode |
m.backwardTaintStep(resultNode, succ) and
localForwardTaintStep+(resultNode, pred.(DataFlow::PostUpdateNode).getPreUpdateNode())
) and
model = "FunctionModel"
}
/**
* Holds if the additional step from `pred` to `succ` should be included in all
* global taint flow configurations.
*/
predicate localAdditionalTaintStep(DataFlow::Node pred, DataFlow::Node succ, string model) {
localAdditionalForwardTaintStep(pred, succ, model) or
localAdditionalBackwardTaintStep(pred, succ, model)
}
/**
* Holds if taint flows from `pred` to `succ` via a reference or dereference.
*
@@ -199,23 +228,36 @@ abstract class FunctionModel extends Function {
abstract predicate hasTaintFlow(FunctionInput input, FunctionOutput output);
/** Gets an input node for this model for the call `c`. */
DataFlow::Node getAnInputNode(DataFlow::CallNode c) { this.taintStepForCall(result, _, c) }
DataFlow::Node getAnInputNode(DataFlow::CallNode c) { this.taintStepForCall(result, _, c, _) }
/** Gets an output node for this model for the call `c`. */
DataFlow::Node getAnOutputNode(DataFlow::CallNode c) { this.taintStepForCall(_, result, c) }
DataFlow::Node getAnOutputNode(DataFlow::CallNode c) { this.taintStepForCall(_, result, c, _) }
/** Holds if this function model causes taint to flow from `pred` to `succ` for the call `c`. */
predicate taintStepForCall(DataFlow::Node pred, DataFlow::Node succ, DataFlow::CallNode c) {
predicate taintStepForCall(
DataFlow::Node pred, DataFlow::Node succ, DataFlow::CallNode c, Boolean forward
) {
c = this.getACall() and
exists(FunctionInput inp, FunctionOutput outp | this.hasTaintFlow(inp, outp) |
pred = pragma[only_bind_out](inp).getNode(c) and
succ = pragma[only_bind_out](outp).getNode(c)
succ = pragma[only_bind_out](outp).getNode(c) and
if inp.isResult() or inp.isResult(_) then forward = false else forward = true
)
}
/** Holds if this function model causes taint to flow from `pred` to `succ`. */
predicate taintStep(DataFlow::Node pred, DataFlow::Node succ) {
this.taintStepForCall(pred, succ, _)
this.taintStepForCall(pred, succ, _, _)
}
/** Holds if this function model causes taint to flow forward from `pred` to `succ`. */
predicate forwardTaintStep(DataFlow::Node pred, DataFlow::Node succ) {
this.taintStepForCall(pred, succ, _, true)
}
/** Holds if this function model causes taint to flow backwards from `pred` to `succ`. */
predicate backwardTaintStep(DataFlow::Node pred, DataFlow::Node succ) {
this.taintStepForCall(pred, succ, _, false)
}
}

View File

@@ -8,8 +8,6 @@ invalidModelRow
| crypto.go:11:18:11:57 | call to Open | crypto.go:11:2:11:57 | ... := ...[1] |
| crypto.go:11:42:11:51 | ciphertext | crypto.go:11:2:11:57 | ... := ...[0] |
| io.go:14:31:14:43 | "some string" | io.go:14:13:14:44 | call to NewReader |
| io.go:16:3:16:3 | definition of w | io.go:16:23:16:27 | &... [postupdate] |
| io.go:16:3:16:3 | definition of w | io.go:16:30:16:34 | &... [postupdate] |
| io.go:16:23:16:27 | &... | io.go:16:24:16:27 | buf1 [postupdate] |
| io.go:16:23:16:27 | &... [postupdate] | io.go:16:24:16:27 | buf1 [postupdate] |
| io.go:16:24:16:27 | buf1 | io.go:16:23:16:27 | &... |
@@ -18,6 +16,8 @@ invalidModelRow
| io.go:16:30:16:34 | &... [postupdate] | io.go:16:31:16:34 | buf2 [postupdate] |
| io.go:16:31:16:34 | buf2 | io.go:16:30:16:34 | &... |
| io.go:16:31:16:34 | buf2 [postupdate] | io.go:16:30:16:34 | &... |
| io.go:18:11:18:11 | w [postupdate] | io.go:16:23:16:27 | &... [postupdate] |
| io.go:18:11:18:11 | w [postupdate] | io.go:16:30:16:34 | &... [postupdate] |
| io.go:18:14:18:19 | reader | io.go:18:11:18:11 | w [postupdate] |
| io.go:22:31:22:43 | "some string" | io.go:22:13:22:44 | call to NewReader |
| io.go:25:19:25:23 | &... | io.go:25:20:25:23 | buf1 [postupdate] |
@@ -31,9 +31,9 @@ invalidModelRow
| io.go:33:20:33:23 | buf1 | io.go:33:19:33:23 | &... |
| io.go:33:20:33:23 | buf1 [postupdate] | io.go:33:19:33:23 | &... |
| io.go:35:16:35:21 | reader | io.go:35:12:35:13 | w2 [postupdate] |
| io.go:39:6:39:6 | definition of w | io.go:39:3:39:19 | ... := ...[0] |
| io.go:39:11:39:19 | call to Pipe | io.go:39:3:39:19 | ... := ...[0] |
| io.go:39:11:39:19 | call to Pipe | io.go:39:3:39:19 | ... := ...[1] |
| io.go:40:14:40:14 | w [postupdate] | io.go:39:3:39:19 | ... := ...[0] |
| io.go:40:17:40:31 | "some string\\n" | io.go:40:14:40:14 | w [postupdate] |
| io.go:43:16:43:16 | r | io.go:43:3:43:5 | buf [postupdate] |
| io.go:44:13:44:15 | buf | io.go:44:13:44:24 | call to String |

View File

@@ -1,7 +1,6 @@
#select
| EmailBad.go:12:56:12:67 | type conversion | EmailBad.go:9:10:9:17 | selection of Header | EmailBad.go:12:56:12:67 | type conversion | Email content may contain $@. | EmailBad.go:9:10:9:17 | selection of Header | untrusted input |
| main.go:33:57:33:78 | type conversion | main.go:31:21:31:31 | call to Referer | main.go:33:57:33:78 | type conversion | Email content may contain $@. | main.go:31:21:31:31 | call to Referer | untrusted input |
| main.go:42:3:42:7 | definition of write | main.go:39:21:39:31 | call to Referer | main.go:42:3:42:7 | definition of write | Email content may contain $@. | main.go:39:21:39:31 | call to Referer | untrusted input |
| main.go:54:46:54:59 | untrustedInput | main.go:48:21:48:31 | call to Referer | main.go:54:46:54:59 | untrustedInput | Email content may contain $@. | main.go:48:21:48:31 | call to Referer | untrusted input |
| main.go:55:52:55:65 | untrustedInput | main.go:48:21:48:31 | call to Referer | main.go:55:52:55:65 | untrustedInput | Email content may contain $@. | main.go:48:21:48:31 | call to Referer | untrusted input |
| main.go:65:16:65:22 | content | main.go:60:21:60:31 | call to Referer | main.go:65:16:65:22 | content | Email content may contain $@. | main.go:60:21:60:31 | call to Referer | untrusted input |
@@ -16,8 +15,6 @@ edges
| EmailBad.go:9:10:9:17 | selection of Header | EmailBad.go:9:10:9:29 | call to Get | provenance | Src:MaD:1 MaD:7 |
| EmailBad.go:9:10:9:29 | call to Get | EmailBad.go:12:56:12:67 | type conversion | provenance | |
| main.go:31:21:31:31 | call to Referer | main.go:33:57:33:78 | type conversion | provenance | Src:MaD:2 |
| main.go:39:21:39:31 | call to Referer | main.go:43:25:43:38 | untrustedInput | provenance | Src:MaD:2 |
| main.go:43:25:43:38 | untrustedInput | main.go:42:3:42:7 | definition of write | provenance | MaD:5 |
| main.go:48:21:48:31 | call to Referer | main.go:54:46:54:59 | untrustedInput | provenance | Src:MaD:2 |
| main.go:48:21:48:31 | call to Referer | main.go:55:52:55:65 | untrustedInput | provenance | Src:MaD:2 |
| main.go:60:21:60:31 | call to Referer | main.go:62:47:62:60 | untrustedInput | provenance | Src:MaD:2 |
@@ -33,15 +30,15 @@ edges
| main.go:93:15:93:62 | call to NewContent | main.go:95:16:95:23 | content2 | provenance | |
| main.go:93:48:93:61 | untrustedInput | main.go:93:15:93:62 | call to NewContent | provenance | MaD:4 |
| main.go:113:21:113:31 | call to Referer | main.go:119:28:119:41 | untrustedInput | provenance | Src:MaD:2 |
| main.go:116:3:116:4 | definition of mw | main.go:116:29:116:30 | &... | provenance | FunctionModel |
| main.go:116:29:116:30 | &... | main.go:124:57:124:57 | b | provenance | |
| main.go:119:28:119:41 | untrustedInput | main.go:116:3:116:4 | definition of mw | provenance | MaD:6 |
| main.go:116:29:116:30 | &... [postupdate] | main.go:124:57:124:57 | b | provenance | |
| main.go:119:3:119:4 | mw [postupdate] | main.go:116:29:116:30 | &... [postupdate] | provenance | FunctionModel |
| main.go:119:28:119:41 | untrustedInput | main.go:119:3:119:4 | mw [postupdate] | provenance | MaD:6 |
| main.go:124:57:124:57 | b | main.go:124:57:124:65 | call to Bytes | provenance | MaD:3 |
| main.go:129:21:129:31 | call to Referer | main.go:136:30:136:43 | untrustedInput | provenance | Src:MaD:2 |
| main.go:132:3:132:4 | definition of mw | main.go:132:29:132:30 | &... | provenance | FunctionModel |
| main.go:132:29:132:30 | &... | main.go:141:57:141:57 | b | provenance | |
| main.go:135:3:135:12 | definition of formWriter | main.go:132:3:132:4 | definition of mw | provenance | FunctionModel |
| main.go:136:30:136:43 | untrustedInput | main.go:135:3:135:12 | definition of formWriter | provenance | MaD:5 |
| main.go:132:29:132:30 | &... [postupdate] | main.go:141:57:141:57 | b | provenance | |
| main.go:135:20:135:21 | mw [postupdate] | main.go:132:29:132:30 | &... [postupdate] | provenance | FunctionModel |
| main.go:136:18:136:27 | formWriter [postupdate] | main.go:135:20:135:21 | mw [postupdate] | provenance | FunctionModel |
| main.go:136:30:136:43 | untrustedInput | main.go:136:18:136:27 | formWriter [postupdate] | provenance | MaD:5 |
| main.go:141:57:141:57 | b | main.go:141:57:141:65 | call to Bytes | provenance | MaD:3 |
models
| 1 | Source: net/http; Request; true; Header; ; ; ; remote; manual |
@@ -57,9 +54,6 @@ nodes
| EmailBad.go:12:56:12:67 | type conversion | semmle.label | type conversion |
| main.go:31:21:31:31 | call to Referer | semmle.label | call to Referer |
| main.go:33:57:33:78 | type conversion | semmle.label | type conversion |
| main.go:39:21:39:31 | call to Referer | semmle.label | call to Referer |
| main.go:42:3:42:7 | definition of write | semmle.label | definition of write |
| main.go:43:25:43:38 | untrustedInput | semmle.label | untrustedInput |
| main.go:48:21:48:31 | call to Referer | semmle.label | call to Referer |
| main.go:54:46:54:59 | untrustedInput | semmle.label | untrustedInput |
| main.go:55:52:55:65 | untrustedInput | semmle.label | untrustedInput |
@@ -79,16 +73,19 @@ nodes
| main.go:93:48:93:61 | untrustedInput | semmle.label | untrustedInput |
| main.go:95:16:95:23 | content2 | semmle.label | content2 |
| main.go:113:21:113:31 | call to Referer | semmle.label | call to Referer |
| main.go:116:3:116:4 | definition of mw | semmle.label | definition of mw |
| main.go:116:29:116:30 | &... | semmle.label | &... |
| main.go:116:29:116:30 | &... [postupdate] | semmle.label | &... [postupdate] |
| main.go:119:3:119:4 | mw [postupdate] | semmle.label | mw [postupdate] |
| main.go:119:28:119:41 | untrustedInput | semmle.label | untrustedInput |
| main.go:124:57:124:57 | b | semmle.label | b |
| main.go:124:57:124:65 | call to Bytes | semmle.label | call to Bytes |
| main.go:129:21:129:31 | call to Referer | semmle.label | call to Referer |
| main.go:132:3:132:4 | definition of mw | semmle.label | definition of mw |
| main.go:132:29:132:30 | &... | semmle.label | &... |
| main.go:135:3:135:12 | definition of formWriter | semmle.label | definition of formWriter |
| main.go:132:29:132:30 | &... [postupdate] | semmle.label | &... [postupdate] |
| main.go:135:20:135:21 | mw [postupdate] | semmle.label | mw [postupdate] |
| main.go:136:18:136:27 | formWriter [postupdate] | semmle.label | formWriter [postupdate] |
| main.go:136:30:136:43 | untrustedInput | semmle.label | untrustedInput |
| main.go:141:57:141:57 | b | semmle.label | b |
| main.go:141:57:141:65 | call to Bytes | semmle.label | call to Bytes |
subpaths
testFailures
| main.go:39:33:39:43 | comment | Missing result: Source |
| main.go:42:24:42:33 | comment | Missing result: Alert |