diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll b/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll index 125f2107bce..662db9e9721 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll @@ -20,7 +20,8 @@ module ProductFlow { * `source1` and `source2` must belong to the same callable. */ predicate isSourcePair( - DataFlow::Node source1, string state1, DataFlow::Node source2, string state2 + DataFlow::Node source1, DataFlow::FlowState state1, DataFlow::Node source2, + DataFlow::FlowState state2 ) { state1 = "" and state2 = "" and @@ -89,6 +90,49 @@ module ProductFlow { */ predicate isBarrierOut2(DataFlow::Node node) { none() } + /* + * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in + * the first projection of the product dataflow graph. + */ + + predicate isAdditionalFlowStep1(DataFlow::Node node1, DataFlow::Node node2) { none() } + + /** + * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in + * the first projection of the product dataflow graph. + * + * This step is only applicable in `state1` and updates the flow state to `state2`. + */ + predicate isAdditionalFlowStep1( + DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, + DataFlow::FlowState state2 + ) { + state1 instanceof DataFlow::FlowStateEmpty and + state2 instanceof DataFlow::FlowStateEmpty and + this.isAdditionalFlowStep1(node1, node2) + } + + /** + * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in + * the second projection of the product dataflow graph. + */ + predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() } + + /** + * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in + * the second projection of the product dataflow graph. + * + * This step is only applicable in `state1` and updates the flow state to `state2`. + */ + predicate isAdditionalFlowStep2( + DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, + DataFlow::FlowState state2 + ) { + state1 instanceof DataFlow::FlowStateEmpty and + state2 instanceof DataFlow::FlowStateEmpty and + this.isAdditionalFlowStep2(node1, node2) + } + predicate hasFlowPath( DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1, DataFlow2::PathNode sink2 @@ -103,46 +147,61 @@ module ProductFlow { class Conf1 extends DataFlow::Configuration { Conf1() { this = "Conf1" } - override predicate isSource(DataFlow::Node source, string state) { + override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { exists(Configuration conf | conf.isSourcePair(source, state, _, _)) } - override predicate isSink(DataFlow::Node sink, string state) { + override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { exists(Configuration conf | conf.isSinkPair(sink, state, _, _)) } - override predicate isBarrier(DataFlow::Node node, string state) { + override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) { exists(Configuration conf | conf.isBarrier1(node, state)) } override predicate isBarrierOut(DataFlow::Node node) { exists(Configuration conf | conf.isBarrierOut1(node)) } + + override predicate isAdditionalFlowStep( + DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, + DataFlow::FlowState state2 + ) { + exists(Configuration conf | conf.isAdditionalFlowStep1(node1, state1, node2, state2)) + } } class Conf2 extends DataFlow2::Configuration { Conf2() { this = "Conf2" } - override predicate isSource(DataFlow::Node source, string state) { - exists(Configuration conf, DataFlow::Node source1 | - conf.isSourcePair(source1, _, source, state) and - any(Conf1 c).hasFlow(source1, _) + override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { + exists(Configuration conf, DataFlow::PathNode source1 | + conf.isSourcePair(source1.getNode(), source1.getState(), source, state) and + any(Conf1 c).hasFlowPath(source1, _) ) } - override predicate isSink(DataFlow::Node sink, string state) { - exists(Configuration conf, DataFlow::Node sink1 | - conf.isSinkPair(sink1, _, sink, state) and any(Conf1 c).hasFlow(_, sink1) + override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { + exists(Configuration conf, DataFlow::PathNode sink1 | + conf.isSinkPair(sink1.getNode(), sink1.getState(), sink, state) and + any(Conf1 c).hasFlowPath(_, sink1) ) } - override predicate isBarrier(DataFlow::Node node, string state) { + override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) { exists(Configuration conf | conf.isBarrier2(node, state)) } override predicate isBarrierOut(DataFlow::Node node) { exists(Configuration conf | conf.isBarrierOut2(node)) } + + override predicate isAdditionalFlowStep( + DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, + DataFlow::FlowState state2 + ) { + exists(Configuration conf | conf.isAdditionalFlowStep2(node1, state1, node2, state2)) + } } } @@ -150,7 +209,7 @@ module ProductFlow { Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode node1, DataFlow2::PathNode node2 ) { - conf.isSourcePair(node1.getNode(), _, node2.getNode(), _) and + conf.isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and node1 = source1 and node2 = source2 or @@ -213,7 +272,7 @@ module ProductFlow { ) { exists(DataFlow::PathNode mid1, DataFlow2::PathNode mid2 | reachableInterprocEntry(conf, source1, source2, mid1, mid2) and - conf.isSinkPair(sink1.getNode(), _, sink2.getNode(), _) and + conf.isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and localPathStep1*(mid1, sink1) and localPathStep2*(mid2, sink2) ) diff --git a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql index 207be4071b9..e9ee074be22 100644 --- a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql +++ b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql @@ -123,6 +123,21 @@ class StringSizeConfiguration extends ProductFlow::Configuration { delta > state2.toInt() ) } + + override predicate isAdditionalFlowStep2( + DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, + DataFlow::FlowState state2 + ) { + exists(AddInstruction add, Operand op, int delta, int s1, int s2 | + s1 = [0 .. 32] and // An arbitrary bound because we need to bound `state` + state1 = s1.toString() and + state2 = s2.toString() and + add.hasOperands(node1.asOperand(), op) and + semBounded(op.getDef(), any(SemZeroBound zero), delta, true, _) and + node2.asInstruction() = add and + s1 = s2 + delta + ) + } } from diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/OverrunWriteProductFlow.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/OverrunWriteProductFlow.expected index f88b102f250..e119d560bfc 100644 --- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/OverrunWriteProductFlow.expected +++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/OverrunWriteProductFlow.expected @@ -95,3 +95,6 @@ subpaths | test.cpp:42:5:42:11 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:42:18:42:23 | Load | This write may overflow $@ by 1 element. | test.cpp:42:18:42:23 | string | string | | test.cpp:72:9:72:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:72:22:72:27 | Load | This write may overflow $@ by 1 element. | test.cpp:72:22:72:27 | string | string | | test.cpp:80:9:80:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:80:22:80:27 | Load | This write may overflow $@ by 2 elements. | test.cpp:80:22:80:27 | string | string | +| test.cpp:99:5:99:11 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:99:18:99:23 | Load | This write may overflow $@ by 1 element. | test.cpp:99:18:99:23 | string | string | +| test.cpp:129:9:129:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:129:22:129:27 | Load | This write may overflow $@ by 1 element. | test.cpp:129:22:129:27 | string | string | +| test.cpp:137:9:137:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:137:22:137:27 | Load | This write may overflow $@ by 2 elements. | test.cpp:137:22:137:27 | string | string | diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/test.cpp b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/test.cpp index d8cca6a39fc..2f370ce09a6 100644 --- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/test.cpp +++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/test.cpp @@ -96,7 +96,7 @@ void test4(unsigned size, char *buf, unsigned anotherSize) { string_t *str = mk_string_t_plus_one(size); strncpy(str->string, buf, str->size); // GOOD - strncpy(str->string, buf, str->size + 1); // BAD [NOT DETECTED] + strncpy(str->string, buf, str->size + 1); // BAD strncpy(str->string, buf, size); // GOOD strncpy(str->string, buf, size + 1); // GOOD @@ -126,7 +126,7 @@ void test4(unsigned size, char *buf, unsigned anotherSize) { } if(anotherSize <= str->size + 1) { - strncpy(str->string, buf, anotherSize); // BAD [NOT DETECTED] + strncpy(str->string, buf, anotherSize); // BAD } if(anotherSize <= size + 1) { @@ -134,7 +134,7 @@ void test4(unsigned size, char *buf, unsigned anotherSize) { } if(anotherSize <= str->size + 2) { - strncpy(str->string, buf, anotherSize); // BAD [NOT DETECTED] + strncpy(str->string, buf, anotherSize); // BAD } if(anotherSize <= size + 2) {