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 e6e9eeeca58..3ac27fd0e16 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll @@ -1,17 +1,208 @@ import semmle.code.cpp.ir.dataflow.DataFlow -import semmle.code.cpp.ir.dataflow.DataFlow2 module ProductFlow { - abstract class Configuration extends string { - bindingset[this] - Configuration() { any() } - + signature module ConfigSig { /** * Holds if `(source1, source2)` is a relevant data flow source. * * `source1` and `source2` must belong to the same callable. */ - predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) { none() } + predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2); + + /** + * Holds if `(sink1, sink2)` is a relevant data flow sink. + * + * `sink1` and `sink2` must belong to the same callable. + */ + predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2); + + /** + * Holds if data flow through `node` is prohibited through the first projection of the product + * dataflow graph. + */ + default predicate isBarrier1(DataFlow::Node node) { none() } + + /** + * Holds if data flow through `node` is prohibited through the second projection of the product + * dataflow graph. + */ + default predicate isBarrier2(DataFlow::Node node) { none() } + + /** + * Holds if data flow out of `node` is prohibited in the first projection of the product + * dataflow graph. + */ + default predicate isBarrierOut1(DataFlow::Node node) { none() } + + /** + * Holds if data flow out of `node` is prohibited in the second projection of the product + * dataflow graph. + */ + default 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. + */ + + default 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 second projection of the product dataflow graph. + */ + default predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() } + + /** + * Holds if data flow into `node` is prohibited in the first projection of the product + * dataflow graph. + */ + default predicate isBarrierIn1(DataFlow::Node node) { none() } + + /** + * Holds if data flow into `node` is prohibited in the second projection of the product + * dataflow graph. + */ + default predicate isBarrierIn2(DataFlow::Node node) { none() } + } + + module Make { + class PathNode1 = Flow1::PathNode; + + class PathNode2 = Flow2::PathNode; + + module PathGraph1 = Flow1::PathGraph; + + module PathGraph2 = Flow2::PathGraph; + + predicate hasFlowPath(PathNode1 source1, PathNode2 source2, PathNode1 sink1, PathNode2 sink2) { + reachable(source1, source2, sink1, sink2) + } + + private module Config1 implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { Config::isSourcePair(source, _) } + + predicate isSink(DataFlow::Node sink) { Config::isSinkPair(sink, _) } + + predicate isBarrier(DataFlow::Node node) { Config::isBarrier1(node) } + + predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut1(node) } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + Config::isAdditionalFlowStep1(node1, node2) + } + + predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) } + } + + private module Flow1 = DataFlow::Make; + + private module Config2 implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(Flow1::PathNode source1 | + Config::isSourcePair(source1.getNode(), source) and + Flow1::hasFlowPath(source1, _) + ) + } + + predicate isSink(DataFlow::Node sink) { + exists(Flow1::PathNode sink1 | + Config::isSinkPair(sink1.getNode(), sink) and + Flow1::hasFlowPath(_, sink1) + ) + } + + predicate isBarrier(DataFlow::Node node) { Config::isBarrier2(node) } + + predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut2(node) } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + Config::isAdditionalFlowStep2(node1, node2) + } + + predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) } + } + + private module Flow2 = DataFlow::Make; + + pragma[nomagic] + private predicate reachableInterprocEntry( + Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode node1, Flow2::PathNode node2 + ) { + Config::isSourcePair(node1.getNode(), node2.getNode()) and + node1 = source1 and + node2 = source2 + or + exists( + Flow1::PathNode midEntry1, Flow2::PathNode midEntry2, Flow1::PathNode midExit1, + Flow2::PathNode midExit2 + | + reachableInterprocEntry(source1, source2, midEntry1, midEntry2) and + interprocEdgePair(midExit1, midExit2, node1, node2) and + localPathStep1*(midEntry1, midExit1) and + localPathStep2*(midEntry2, midExit2) + ) + } + + private predicate localPathStep1(Flow1::PathNode pred, Flow1::PathNode succ) { + Flow1::PathGraph::edges(pred, succ) and + pragma[only_bind_out](pred.getNode().getEnclosingCallable()) = + pragma[only_bind_out](succ.getNode().getEnclosingCallable()) + } + + private predicate localPathStep2(Flow2::PathNode pred, Flow2::PathNode succ) { + Flow2::PathGraph::edges(pred, succ) and + pragma[only_bind_out](pred.getNode().getEnclosingCallable()) = + pragma[only_bind_out](succ.getNode().getEnclosingCallable()) + } + + pragma[nomagic] + private predicate interprocEdge1( + Declaration predDecl, Declaration succDecl, Flow1::PathNode pred1, Flow1::PathNode succ1 + ) { + Flow1::PathGraph::edges(pred1, succ1) and + predDecl != succDecl and + pred1.getNode().getEnclosingCallable() = predDecl and + succ1.getNode().getEnclosingCallable() = succDecl + } + + pragma[nomagic] + private predicate interprocEdge2( + Declaration predDecl, Declaration succDecl, Flow2::PathNode pred2, Flow2::PathNode succ2 + ) { + Flow2::PathGraph::edges(pred2, succ2) and + predDecl != succDecl and + pred2.getNode().getEnclosingCallable() = predDecl and + succ2.getNode().getEnclosingCallable() = succDecl + } + + private predicate interprocEdgePair( + Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2 + ) { + exists(Declaration predDecl, Declaration succDecl | + interprocEdge1(predDecl, succDecl, pred1, succ1) and + interprocEdge2(predDecl, succDecl, pred2, succ2) + ) + } + + private predicate reachable( + Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2 + ) { + exists(Flow1::PathNode mid1, Flow2::PathNode mid2 | + reachableInterprocEntry(source1, source2, mid1, mid2) and + Config::isSinkPair(sink1.getNode(), sink2.getNode()) and + localPathStep1*(mid1, sink1) and + localPathStep2*(mid2, sink2) + ) + } + } + + signature module StateConfigSig { + bindingset[this] + class FlowState1; + + bindingset[this] + class FlowState2; /** * Holds if `(source1, source2)` is a relevant data flow source with initial states `state1` @@ -20,20 +211,8 @@ module ProductFlow { * `source1` and `source2` must belong to the same callable. */ predicate isSourcePair( - DataFlow::Node source1, DataFlow::FlowState state1, DataFlow::Node source2, - DataFlow::FlowState state2 - ) { - state1 = "" and - state2 = "" and - this.isSourcePair(source1, source2) - } - - /** - * Holds if `(sink1, sink2)` is a relevant data flow sink. - * - * `sink1` and `sink2` must belong to the same callable. - */ - predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) { none() } + DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2 + ); /** * Holds if `(sink1, sink2)` is a relevant data flow sink with final states `state1` @@ -42,60 +221,51 @@ module ProductFlow { * `sink1` and `sink2` must belong to the same callable. */ predicate isSinkPair( - DataFlow::Node sink1, DataFlow::FlowState state1, DataFlow::Node sink2, - DataFlow::FlowState state2 - ) { - state1 = "" and - state2 = "" and - this.isSinkPair(sink1, sink2) - } + DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2 + ); /** * Holds if data flow through `node` is prohibited through the first projection of the product * dataflow graph when the flow state is `state`. */ - predicate isBarrier1(DataFlow::Node node, DataFlow::FlowState state) { - this.isBarrier1(node) and state = "" - } + predicate isBarrier1(DataFlow::Node node, FlowState1 state); /** * Holds if data flow through `node` is prohibited through the second projection of the product * dataflow graph when the flow state is `state`. */ - predicate isBarrier2(DataFlow::Node node, DataFlow::FlowState state) { - this.isBarrier2(node) and state = "" - } + predicate isBarrier2(DataFlow::Node node, FlowState2 state); /** * Holds if data flow through `node` is prohibited through the first projection of the product * dataflow graph. */ - predicate isBarrier1(DataFlow::Node node) { none() } + default predicate isBarrier1(DataFlow::Node node) { none() } /** * Holds if data flow through `node` is prohibited through the second projection of the product * dataflow graph. */ - predicate isBarrier2(DataFlow::Node node) { none() } + default predicate isBarrier2(DataFlow::Node node) { none() } /** * Holds if data flow out of `node` is prohibited in the first projection of the product * dataflow graph. */ - predicate isBarrierOut1(DataFlow::Node node) { none() } + default predicate isBarrierOut1(DataFlow::Node node) { none() } /** * Holds if data flow out of `node` is prohibited in the second projection of the product * dataflow graph. */ - predicate isBarrierOut2(DataFlow::Node node) { none() } + default 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() } + default 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 @@ -104,19 +274,14 @@ module ProductFlow { * 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) - } + DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2 + ); /** * 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() } + default 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 @@ -125,177 +290,168 @@ module ProductFlow { * 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) - } + DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2 + ); /** * Holds if data flow into `node` is prohibited in the first projection of the product * dataflow graph. */ - predicate isBarrierIn1(DataFlow::Node node) { none() } + default predicate isBarrierIn1(DataFlow::Node node) { none() } /** * Holds if data flow into `node` is prohibited in the second projection of the product * dataflow graph. */ - predicate isBarrierIn2(DataFlow::Node node) { none() } + default predicate isBarrierIn2(DataFlow::Node node) { none() } + } + + module MakeWithState { + class PathNode1 = Flow1::PathNode; + + class PathNode2 = Flow2::PathNode; + + module PathGraph1 = Flow1::PathGraph; + + module PathGraph2 = Flow2::PathGraph; + + class FlowState1 = Config::FlowState1; + + class FlowState2 = Config::FlowState2; predicate hasFlowPath( - DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1, - DataFlow2::PathNode sink2 + Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2 ) { - reachable(this, source1, source2, sink1, sink2) + reachable(source1, source2, sink1, sink2) } - } - private import Internal + private module Config1 implements DataFlow::StateConfigSig { + class FlowState = FlowState1; - module Internal { - class Conf1 extends DataFlow::Configuration { - Conf1() { this = "Conf1" } - - override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { - exists(Configuration conf | conf.isSourcePair(source, state, _, _)) + predicate isSource(DataFlow::Node source, FlowState state) { + Config::isSourcePair(source, state, _, _) } - override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { - exists(Configuration conf | conf.isSinkPair(sink, state, _, _)) + predicate isSink(DataFlow::Node sink, FlowState state) { + Config::isSinkPair(sink, state, _, _) } - override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) { - exists(Configuration conf | conf.isBarrier1(node, state)) - } + predicate isBarrier(DataFlow::Node node, FlowState state) { Config::isBarrier1(node, state) } - override predicate isBarrierOut(DataFlow::Node node) { - exists(Configuration conf | conf.isBarrierOut1(node)) - } + predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut1(node) } - override predicate isAdditionalFlowStep( - DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, - DataFlow::FlowState state2 + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState state2 ) { - exists(Configuration conf | conf.isAdditionalFlowStep1(node1, state1, node2, state2)) + Config::isAdditionalFlowStep1(node1, state1, node2, state2) } - override predicate isBarrierIn(DataFlow::Node node) { - exists(Configuration conf | conf.isBarrierIn1(node)) - } + predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) } } - class Conf2 extends DataFlow2::Configuration { - Conf2() { this = "Conf2" } + module Flow1 = DataFlow::MakeWithState; - 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, _) + module Config2 implements DataFlow::StateConfigSig { + class FlowState = FlowState2; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(Flow1::PathNode source1 | + Config::isSourcePair(source1.getNode(), source1.getState(), source, state) and + Flow1::hasFlowPath(source1, _) ) } - 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) + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(Flow1::PathNode sink1 | + Config::isSinkPair(sink1.getNode(), sink1.getState(), sink, state) and + Flow1::hasFlowPath(_, sink1) ) } - override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) { - exists(Configuration conf | conf.isBarrier2(node, state)) - } + predicate isBarrier(DataFlow::Node node, FlowState state) { Config::isBarrier2(node, state) } - override predicate isBarrierOut(DataFlow::Node node) { - exists(Configuration conf | conf.isBarrierOut2(node)) - } + predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut2(node) } - override predicate isAdditionalFlowStep( - DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, - DataFlow::FlowState state2 + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 ) { - exists(Configuration conf | conf.isAdditionalFlowStep2(node1, state1, node2, state2)) + Config::isAdditionalFlowStep2(node1, state1, node2, state2) } - override predicate isBarrierIn(DataFlow::Node node) { - exists(Configuration conf | conf.isBarrierIn2(node)) - } + predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) } } - } - pragma[nomagic] - private predicate reachableInterprocEntry( - Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2, - DataFlow::PathNode node1, DataFlow2::PathNode node2 - ) { - conf.isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and - node1 = source1 and - node2 = source2 - or - exists( - DataFlow::PathNode midEntry1, DataFlow2::PathNode midEntry2, DataFlow::PathNode midExit1, - DataFlow2::PathNode midExit2 - | - reachableInterprocEntry(conf, source1, source2, midEntry1, midEntry2) and - interprocEdgePair(midExit1, midExit2, node1, node2) and - localPathStep1*(midEntry1, midExit1) and - localPathStep2*(midEntry2, midExit2) - ) - } + module Flow2 = DataFlow::MakeWithState; - private predicate localPathStep1(DataFlow::PathNode pred, DataFlow::PathNode succ) { - DataFlow::PathGraph::edges(pred, succ) and - pragma[only_bind_out](pred.getNode().getEnclosingCallable()) = - pragma[only_bind_out](succ.getNode().getEnclosingCallable()) - } + pragma[nomagic] + private predicate reachableInterprocEntry( + Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode node1, Flow2::PathNode node2 + ) { + Config::isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and + node1 = source1 and + node2 = source2 + or + exists( + Flow1::PathNode midEntry1, Flow2::PathNode midEntry2, Flow1::PathNode midExit1, + Flow2::PathNode midExit2 + | + reachableInterprocEntry(source1, source2, midEntry1, midEntry2) and + interprocEdgePair(midExit1, midExit2, node1, node2) and + localPathStep1*(midEntry1, midExit1) and + localPathStep2*(midEntry2, midExit2) + ) + } - private predicate localPathStep2(DataFlow2::PathNode pred, DataFlow2::PathNode succ) { - DataFlow2::PathGraph::edges(pred, succ) and - pragma[only_bind_out](pred.getNode().getEnclosingCallable()) = - pragma[only_bind_out](succ.getNode().getEnclosingCallable()) - } + private predicate localPathStep1(Flow1::PathNode pred, Flow1::PathNode succ) { + Flow1::PathGraph::edges(pred, succ) and + pragma[only_bind_out](pred.getNode().getEnclosingCallable()) = + pragma[only_bind_out](succ.getNode().getEnclosingCallable()) + } - pragma[nomagic] - private predicate interprocEdge1( - Declaration predDecl, Declaration succDecl, DataFlow::PathNode pred1, DataFlow::PathNode succ1 - ) { - DataFlow::PathGraph::edges(pred1, succ1) and - predDecl != succDecl and - pred1.getNode().getEnclosingCallable() = predDecl and - succ1.getNode().getEnclosingCallable() = succDecl - } + private predicate localPathStep2(Flow2::PathNode pred, Flow2::PathNode succ) { + Flow2::PathGraph::edges(pred, succ) and + pragma[only_bind_out](pred.getNode().getEnclosingCallable()) = + pragma[only_bind_out](succ.getNode().getEnclosingCallable()) + } - pragma[nomagic] - private predicate interprocEdge2( - Declaration predDecl, Declaration succDecl, DataFlow2::PathNode pred2, DataFlow2::PathNode succ2 - ) { - DataFlow2::PathGraph::edges(pred2, succ2) and - predDecl != succDecl and - pred2.getNode().getEnclosingCallable() = predDecl and - succ2.getNode().getEnclosingCallable() = succDecl - } + pragma[nomagic] + private predicate interprocEdge1( + Declaration predDecl, Declaration succDecl, Flow1::PathNode pred1, Flow1::PathNode succ1 + ) { + Flow1::PathGraph::edges(pred1, succ1) and + predDecl != succDecl and + pred1.getNode().getEnclosingCallable() = predDecl and + succ1.getNode().getEnclosingCallable() = succDecl + } - private predicate interprocEdgePair( - DataFlow::PathNode pred1, DataFlow2::PathNode pred2, DataFlow::PathNode succ1, - DataFlow2::PathNode succ2 - ) { - exists(Declaration predDecl, Declaration succDecl | - interprocEdge1(predDecl, succDecl, pred1, succ1) and - interprocEdge2(predDecl, succDecl, pred2, succ2) - ) - } + pragma[nomagic] + private predicate interprocEdge2( + Declaration predDecl, Declaration succDecl, Flow2::PathNode pred2, Flow2::PathNode succ2 + ) { + Flow2::PathGraph::edges(pred2, succ2) and + predDecl != succDecl and + pred2.getNode().getEnclosingCallable() = predDecl and + succ2.getNode().getEnclosingCallable() = succDecl + } - private predicate reachable( - Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2, - DataFlow::PathNode sink1, DataFlow2::PathNode sink2 - ) { - exists(DataFlow::PathNode mid1, DataFlow2::PathNode mid2 | - reachableInterprocEntry(conf, source1, source2, mid1, mid2) and - conf.isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and - localPathStep1*(mid1, sink1) and - localPathStep2*(mid2, sink2) - ) + private predicate interprocEdgePair( + Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2 + ) { + exists(Declaration predDecl, Declaration succDecl | + interprocEdge1(predDecl, succDecl, pred1, succ1) and + interprocEdge2(predDecl, succDecl, pred2, succ2) + ) + } + + private predicate reachable( + Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2 + ) { + exists(Flow1::PathNode mid1, Flow2::PathNode mid2 | + reachableInterprocEntry(source1, source2, mid1, mid2) and + Config::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/ArrayAccessProductFlow.ql b/cpp/ql/src/experimental/Likely Bugs/ArrayAccessProductFlow.ql index 39c54573b06..cb81f165ba7 100644 --- a/cpp/ql/src/experimental/Likely Bugs/ArrayAccessProductFlow.ql +++ b/cpp/ql/src/experimental/Likely Bugs/ArrayAccessProductFlow.ql @@ -18,7 +18,7 @@ import semmle.code.cpp.ir.IR import semmle.code.cpp.valuenumbering.GlobalValueNumbering import semmle.code.cpp.models.interfaces.Allocation import semmle.code.cpp.ir.IRConfiguration -import DataFlow::PathGraph +import ArraySizeFlow::PathGraph1 // temporary - custom allocator for ffmpeg class AvBufferAlloc extends AllocationFunction { @@ -39,14 +39,12 @@ predicate bounded(Instruction i, Bound b, int delta, boolean upper) { semBounded(getSemanticExpr(i), b, delta, upper, _) } -class ArraySizeConfiguration extends ProductFlow::Configuration { - ArraySizeConfiguration() { this = "ArraySizeConfiguration" } - - override predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) { +module ArraySizeConfig implements ProductFlow::ConfigSig { + predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) { source1.asConvertedExpr().(AllocationExpr).getSizeExpr() = source2.asConvertedExpr() } - override predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) { + predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) { exists(PointerAddInstruction pai, int delta | isSinkPair1(sink1, sink2, pai, delta) and ( @@ -63,6 +61,8 @@ class ArraySizeConfiguration extends ProductFlow::Configuration { } } +module ArraySizeFlow = ProductFlow::Make; + pragma[nomagic] predicate isSinkPair1( DataFlow::Node sink1, DataFlow::Node sink2, PointerAddInstruction pai, int delta @@ -76,9 +76,9 @@ predicate isSinkPair1( } from - ArraySizeConfiguration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2, - DataFlow::PathNode sink1, DataFlow2::PathNode sink2 -where conf.hasFlowPath(source1, source2, sink1, sink2) -// TODO: pull delta out and display it + ArraySizeFlow::PathNode1 source1, ArraySizeFlow::PathNode2 source2, + ArraySizeFlow::PathNode1 sink1, ArraySizeFlow::PathNode2 sink2 +where ArraySizeFlow::hasFlowPath(source1, source2, sink1, sink2) +// TODO: pull delta osut and display it select sink1.getNode(), source1, sink1, "Off-by one error allocated at $@ bounded by $@.", source1, source1.toString(), sink2, sink2.toString() diff --git a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql index 7f5315863f4..1a4291bc105 100644 --- a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql +++ b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql @@ -19,7 +19,7 @@ import semmle.code.cpp.models.interfaces.Allocation import semmle.code.cpp.models.interfaces.ArrayFunction import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific -import DataFlow::PathGraph +import StringSizeFlow::PathGraph1 pragma[nomagic] Instruction getABoundIn(SemBound b, IRFunction func) { @@ -77,12 +77,13 @@ predicate isSinkPairImpl( ) } -class StringSizeConfiguration extends ProductFlow::Configuration { - StringSizeConfiguration() { this = "StringSizeConfiguration" } +module StringSizeConfig implements ProductFlow::StateConfigSig { + class FlowState1 = string; - override predicate isSourcePair( - DataFlow::Node bufSource, DataFlow::FlowState state1, DataFlow::Node sizeSource, - DataFlow::FlowState state2 + class FlowState2 = string; + + predicate isSourcePair( + DataFlow::Node bufSource, FlowState1 state1, DataFlow::Node sizeSource, FlowState2 state2 ) { // In the case of an allocation like // ```cpp @@ -94,9 +95,8 @@ class StringSizeConfiguration extends ProductFlow::Configuration { hasSize(bufSource.asConvertedExpr(), sizeSource, state2) } - override predicate isSinkPair( - DataFlow::Node bufSink, DataFlow::FlowState state1, DataFlow::Node sizeSink, - DataFlow::FlowState state2 + predicate isSinkPair( + DataFlow::Node bufSink, FlowState1 state1, DataFlow::Node sizeSink, FlowState2 state2 ) { state1 instanceof DataFlow::FlowStateEmpty and state2 = [-32 .. 32].toString() and // An arbitrary bound because we need to bound `state2` @@ -106,9 +106,18 @@ class StringSizeConfiguration extends ProductFlow::Configuration { ) } - override predicate isAdditionalFlowStep2( - DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2, - DataFlow::FlowState state2 + predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() } + + predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() } + + predicate isAdditionalFlowStep1( + DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState2 state2 + ) { + none() + } + + predicate isAdditionalFlowStep2( + DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState2 state2 ) { exists(AddInstruction add, Operand op, int delta, int s1, int s2 | s1 = [-32 .. 32] and // An arbitrary bound because we need to bound `state` @@ -122,12 +131,14 @@ class StringSizeConfiguration extends ProductFlow::Configuration { } } +module StringSizeFlow = ProductFlow::MakeWithState; + from - StringSizeConfiguration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2, - DataFlow::PathNode sink1, DataFlow2::PathNode sink2, int overflow, int sinkState, + StringSizeFlow::PathNode1 source1, StringSizeFlow::PathNode2 source2, + StringSizeFlow::PathNode1 sink1, StringSizeFlow::PathNode2 sink2, int overflow, int sinkState, CallInstruction c, DataFlow::Node sourceNode, Expr buffer, string element where - conf.hasFlowPath(source1, source2, sink1, sink2) and + StringSizeFlow::hasFlowPath(source1, source2, sink1, sink2) and sinkState = sink2.getState().toInt() and isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and overflow > 0 and diff --git a/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql b/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql index 7ac8f05d2b0..3c2806d9bc4 100644 --- a/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql +++ b/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql @@ -107,11 +107,13 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, string state) * Finally, the range-analysis library will find a load from (or store to) an address that * is non-strictly upper-bounded by `end` (which in this case is `*p`). */ -class AllocToInvalidPointerConf extends ProductFlow::Configuration { - AllocToInvalidPointerConf() { this = "AllocToInvalidPointerConf" } +module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig { + class FlowState1 = string; - override predicate isSourcePair( - DataFlow::Node source1, string state1, DataFlow::Node source2, string state2 + class FlowState2 = string; + + predicate isSourcePair( + DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2 ) { // In the case of an allocation like // ```cpp @@ -123,9 +125,8 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration { hasSize(source1.asConvertedExpr(), source2, state2) } - override predicate isSinkPair( - DataFlow::Node sink1, DataFlow::FlowState state1, DataFlow::Node sink2, - DataFlow::FlowState state2 + predicate isSinkPair( + DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2 ) { state1 = "" and // We check that the delta computed by the range analysis matches the @@ -136,13 +137,31 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration { ) } - override predicate isBarrierOut2(DataFlow::Node node) { + predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() } + + predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() } + + predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) } + + predicate isBarrierOut2(DataFlow::Node node) { node = any(DataFlow::SsaPhiNode phi).getAnInput(true) } - override predicate isBarrierIn1(DataFlow::Node node) { this.isSourcePair(node, _, _, _) } + predicate isAdditionalFlowStep1( + DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2 + ) { + none() + } + + predicate isAdditionalFlowStep2( + DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2 + ) { + none() + } } +module AllocToInvalidPointerFlow = ProductFlow::MakeWithState; + /** * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the * left operand of the pointer-arithmetic operation. @@ -224,9 +243,9 @@ module InvalidPointerToDerefFlow = DataFlow::Global predicate invalidPointerToDerefSource( PointerArithmeticInstruction pai, DataFlow::Node source, int delta ) { - exists(ProductFlow::Configuration conf, DataFlow::PathNode p, DataFlow::Node sink1 | + exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 | pragma[only_bind_out](p.getNode()) = sink1 and - conf.hasFlowPath(_, _, pragma[only_bind_into](p), _) and + AllocToInvalidPointerFlow::hasFlowPath(_, _, pragma[only_bind_into](p), _) and isSinkImpl(pai, sink1, _, _) and bounded2(source.asInstruction(), pai, delta) and delta >= 0 @@ -235,7 +254,7 @@ predicate invalidPointerToDerefSource( newtype TMergedPathNode = // The path nodes computed by the first projection of `AllocToInvalidPointerConf` - TPathNode1(DataFlow::PathNode p) or + TPathNode1(AllocToInvalidPointerFlow::PathNode1 p) or // The path nodes computed by `InvalidPointerToDerefConf` TPathNode3(InvalidPointerToDerefFlow::PathNode p) or // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConf`. @@ -251,7 +270,7 @@ newtype TMergedPathNode = class MergedPathNode extends TMergedPathNode { string toString() { none() } - final DataFlow::PathNode asPathNode1() { this = TPathNode1(result) } + final AllocToInvalidPointerFlow::PathNode1 asPathNode1() { this = TPathNode1(result) } final InvalidPointerToDerefFlow::PathNode asPathNode3() { this = TPathNode3(result) } @@ -266,7 +285,7 @@ class MergedPathNode extends TMergedPathNode { class PathNode1 extends MergedPathNode, TPathNode1 { override string toString() { - exists(DataFlow::PathNode p | + exists(AllocToInvalidPointerFlow::PathNode1 p | this = TPathNode1(p) and result = p.toString() ) @@ -326,7 +345,8 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) { * of `InvalidPointerToDerefConf`, and they are connected through `pai`. */ predicate joinOn1( - PointerArithmeticInstruction pai, DataFlow::PathNode p1, InvalidPointerToDerefFlow::PathNode p2 + PointerArithmeticInstruction pai, AllocToInvalidPointerFlow::PathNode1 p1, + InvalidPointerToDerefFlow::PathNode p2 ) { isSinkImpl(pai, p1.getNode(), _, _) and invalidPointerToDerefSource(pai, p2.getNode(), _) @@ -346,11 +366,8 @@ predicate hasFlowPath( MergedPathNode source1, MergedPathNode sink, InvalidPointerToDerefFlow::PathNode source3, PointerArithmeticInstruction pai, string operation ) { - exists( - AllocToInvalidPointerConf conf1, InvalidPointerToDerefFlow::PathNode sink3, - DataFlow::PathNode sink1 - | - conf1.hasFlowPath(source1.asPathNode1(), _, sink1, _) and + exists(InvalidPointerToDerefFlow::PathNode sink3, AllocToInvalidPointerFlow::PathNode1 sink1 | + AllocToInvalidPointerFlow::hasFlowPath(source1.asPathNode1(), _, sink1, _) and joinOn1(pai, sink1, source3) and InvalidPointerToDerefFlow::flowPath(source3, sink3) and joinOn2(sink3, sink.asSinkNode(), operation)