From c00bc1a8a00d0afbd9d5082960184e200b6baec7 Mon Sep 17 00:00:00 2001 From: Nikita Kraiouchkine Date: Fri, 12 May 2023 14:06:07 +0200 Subject: [PATCH] Add stateful data-flow (flow state) content --- .gitignore | 3 +- README.md | 93 ++++++++++------ exercises/Exercise13.ql | 186 ++++++++++++++++++++++++++++++++ exercises/Exercise14.ql | 117 +++++++++++++++++++++ exercises/Exercise15.ql | 200 +++++++++++++++++++++++++++++++++++ exercises/Exercise16.ql | 227 ++++++++++++++++++++++++++++++++++++++++ exercises/Exercise5.ql | 4 +- solutions/Exercise13.ql | 186 ++++++++++++++++++++++++++++++++ solutions/Exercise14.ql | 125 ++++++++++++++++++++++ solutions/Exercise15.ql | 216 ++++++++++++++++++++++++++++++++++++++ solutions/Exercise16.ql | 227 ++++++++++++++++++++++++++++++++++++++++ solutions/Exercise5.ql | 4 +- 12 files changed, 1552 insertions(+), 36 deletions(-) create mode 100644 exercises/Exercise13.ql create mode 100644 exercises/Exercise14.ql create mode 100644 exercises/Exercise15.ql create mode 100644 exercises/Exercise16.ql create mode 100644 solutions/Exercise13.ql create mode 100644 solutions/Exercise14.ql create mode 100644 solutions/Exercise15.ql create mode 100644 solutions/Exercise16.ql diff --git a/.gitignore b/.gitignore index d13d707..bfbdd6b 100644 --- a/.gitignore +++ b/.gitignore @@ -9,4 +9,5 @@ cpp-dataflow-part1-database cpp-dataflow-part2-database cpp-dataflow-part3-database settings.json -.DS_Store \ No newline at end of file +.DS_Store +*.code-workspace diff --git a/README.md b/README.md index cbcb4cf..abd6501 100644 --- a/README.md +++ b/README.md @@ -79,7 +79,7 @@ Before use, `input_types` must be validated against an expected value. If no suc ## Part 1: Introduction to Data-Flow Analysis by Modeling Missing Type Validation ### Exercise 1 -Output all expressions that access a `dynamic_input_t` array. Accessing dynamic inputs involves an `ArrayExpr` where the base type of the array type accessed is `dynamic_input_t`. These expressions can be thought of as "sinks" for the purpose of data-flow analysis. +Output all expressions that access a `dyn_input_t` array. Accessing dynamic inputs involves an `ArrayExpr` where the base type of the array type accessed is `dyn_input_t`. These expressions can be thought of as "sinks" for the purpose of data-flow analysis.
Hint @@ -105,7 +105,7 @@ if(expected_types != input_types) { // access ``` -Validation involves a comparison of the `input_types` parameter with a value returned from `DYN_INPUT_TYPE`, where the arguments to that call dictate the expected types of the `dynamic_input_t` array. +Validation involves a comparison of the `input_types` parameter with a value returned from `DYN_INPUT_TYPE`, where the arguments to that call dictate the expected types of the `dyn_input_t` array. There are three steps to this exercise: 1. Find all calls to `DYN_INPUT_TYPE`. @@ -140,7 +140,7 @@ void func(dyn_input_t *input, unsigned int input_types, int irrelevant_param) { } ``` -The solution is global data-flow analysis. Start by modeling the source, i.e. the entrypoints and their parameters. Entrypoints are functions that are not called from anywhere else in the program and match the signature `int(dynamic_input_t*, unsigned int)`. +The solution is global data-flow analysis. Start by modeling the source, i.e. the entrypoints and their parameters. Entrypoints are functions that are not called from anywhere else in the program and match the signature `int(dyn_input_t*, unsigned int)`. Specifically, these functions are: - `EP_copy_mem` @@ -309,12 +309,11 @@ What is the missing edge?
## Exercise 12 -In this final exercise for Part 2, in the global data-flow configuration, add an additional flow step between the `input` parameter and the `output` parameter of calls to `lock_input` to add the missing edges. +In this final exercise for Part 2, in the global data-flow configuration, add an additional flow step between the `input` parameter and the result of calls to `lock_input` (represented as the `FunctionCall` itself) to add the missing edges.
Hint -* Use `Node::asDefiningArgument` to model the `output` parameter. * Use `Node::asExpr` to model the `input` parameter.
@@ -323,47 +322,75 @@ You should now see additional results through flow paths that include `lock_inpu Optional: Re-add the barrier checks from `Exercise10` to see their impact on a larger set of results. -# End of workshop - -This workshop is currently in ongoing development. Planned topics include: -- Outputting flow state context for each result (currently, state is only bound inside the data-flow configuration). -- Using runtime value analysis to identify type checks with patterns differing from `DYN_INPUT_TYPE`. - ## Part 3: Flow-State The second part of this workshop built upon the data-flow and control-flow analysis from the first part to further identify cases where type validation exists but does not match the subsequent access type. However, that rudimentary recursive control-flow analysis might not work in all cases, as it does not preserve flow path state in the case of multiple function calls with varying validation states. To preserve the state of type validation checks across each data-flow path, we can use flow-state. ### Exercise 13 -Flow states are defined by a class extending `DataFlow::FlowState`. Within a data-flow configuration, an initial flow state is specified in the `isSource` predicate and can be subsequently updated in the `isAdditionalFlowStep` and `isBarrier` predicates. The `isSink` predicate can then check the (path-sensitive) flow-state and conditionally restrict sinks based on the state on the path to the sink. +Definitions modelling the two possible states of type validation for a flow path to a `DynamicInputAccess`, validated and unvalidated, have been provided for you in this exercise. These states have been defined using `newtype` in order to create the [algebraic datatype](https://codeql.github.com/docs/ql-language-reference/types/#algebraic-datatypes) `TTypeValidationState`, which represents the possible states of type validation for a flow path to a `DynamicInputAccess`. Three classes have also been defined to extend from it using this [standard pattern](https://codeql.github.com/docs/ql-language-reference/types/#standard-pattern-for-using-algebraic-datatypes). Try to understand the syntax and the way these types have been structured before proceeding. -First define the necessary flow-state classes: -1. Define the flow state `InputTypesNotValidated` (hint: just use FlowStateString::FlowStateEmpty). -2. Define the flow state `InputTypesValidated` with a [field declaration](https://codeql.github.com/docs/ql-language-reference/types/#fields) specifying the type validation call. Implement a `getValidatedType()` predicate to return the field. +Secondly, the `InputToAccessConfig` data-flow configuration has been modified from the previous exercise to be stateful. Note the following four changes: +1. `InputToAccessConfig` now implements `DataFlow::StateConfigSig` rather than `DataFlow::ConfigSig`. +1. `InputToAccessConfig` now requires some changes to its predicate signatures to include state parameters. +1. `InputToAccessConfig` requires a declaration of a `FlowState` type, which in this example, is an alias to `TTypeValidationState`. +1. `InputToAccess` now constructs a data-flow computation using `DataFlow::MakeWithState` rather than `DataFlow::Make`. -Note the changes in the data-flow configuration in Exercise13.ql: some predicates now have one or more `state` parameters. Complete the predicates to implement the flow-state logic. +It helps to approach implementing each predicate with an understanding of its purpose in stateful data-flow: +| Predicate | Standard use-pattern | +|--------------------------|----------------------------------------------------------| +| `isSource` | Bind `state` to an initial state | +| `isSink` | Restrict sinks to those on paths with a specific `state` | +| `isAdditionalFlowStep/4` | Define state changes from `node1` to `node2` | +| `isAdditionalFlowStep/2` | As before, define flow steps without a state change | +| `isBarrier` | Block flow through `node` with a specific `state` | -For now, in `isSink`, only check if the state is `InputTypesNotValidated`. +Reimplement the new `isSource` and `isSink` predicates to bind state to `TypeUnvalidatedState`. Ignore the `isAdditionalFlowStep/4` and `isBarrier/2` predicates for now; they will be used in a later exercise. -
-Hint - -* `isSource` should check if state is an `instanceof` `InputTypesNotValidated`. -* In `isAdditionalFlowStep`, we don't actually want to add another additional flow step. However, we should restrict the new state to be an `instanceof InputTypesValidated`, where `InputTypesValidated::getValidatedType()` is derived from -the call column of `typeValidationGuard`. - -
- -Output all flow paths. You should see all results that do not have type validation. +You should see the same results as in Exercise 12. ### Exercise 14 -In this final exercise, complete the `isSink` predicate to include cases where the state is `InputTypesValidated` and the expected type *does not* match the access type. +There are two primary ways to define state along a path: +1. Bind an initial state based on the source. +1. Change a state along a path based on a step between two nodes. -You should now see path-sensitive results with no false-negatives or false-positives. +Those two approaches can also be used together. -
-Hint +In this workshop, we will use the second approach: changing state along a path. Start by defining those state-changing steps as part of the `TypeValidatedState` class. Modeling and exposing the state changing step as part of the flow state class is a common pattern used frequently in the CodeQL standard library. -* Use `typeValidationCallMatchesUse` in `isSink`. +Complete the characteristic predicate of `TypeValidatedState` to bind all of its field declarations, where: +* `node1` flows to `node2` in one step +* `node1` is not guarded by a validation check that `node2` is guarded by +* `call` is the call in the validation check `node2` is guarded by -
+Use `DataFlow::localFlowStep` to model the local flow step. + +You should see 69 results. + +### Exercise 15 +Next, combine the class written in Exercise 14 with the stateful data-flow introduced in Exercise 13. Rather than recursively checking if a sink/access is type-validated, introduce that check along the flow path with `isAdditionalFlowStep/4`. + +Reimplement the `isSink`, `isAdditionalFlowStep/4`, and `isBarrier` predicates. + +**Important**: +A peculiarity of flow-state is that modelling a state change in `isAdditionalFlowStep` for an edge that exists independently of this additional flow step created results in a duplicate subsequent flow path for *both* states. Therefore, `isBarrier` must be used to block that duplicate subsequent flow for the unwanted old state. Take the following example as a demonstration of this behavior. Assume that two states exist: `InitialState` and `ChangedState`. If `state_change(node)` is referenced in `isAdditionalFlowStep` but a matching reference in `isBarrier` for the `state_change` with `state instanceof InitialState` is missing, the flow state will be as follows: +```cpp +void flow_state_example(char* node) { + *node; // state instanceof InitialState + state_change(node); // arg_state instanceof InitialState, + // return_state instanceof [InitialState, ChangedState] + *node; // state instanceof [InitialState, ChangedState] +} +``` + +**Hint:** +Make sure to add a barrier to nodes on paths with a validated state but that are guarded by a type check with a type validation call not matching the call of the state (`state.(TypeValidatedState).getCall() != call_guarding_node`). + +You should now see 22 results. + +### Exercise 16 +Lastly, refine the output message of your query by accessing the state of the sink node. Use an `if/then/else` statement in the `where` clause of the query to check if the sink is validated or unvalidated and output a descriptive message for each case accordingly. + +You can retrieve the state of a path node with `DataFlow::PathNode::getState()`. You can cast that state to the appropriate derived type if necessary. + +You should see the same 22 results but with more descriptive messages. \ No newline at end of file diff --git a/exercises/Exercise13.ql b/exercises/Exercise13.ql new file mode 100644 index 0000000..d43f801 --- /dev/null +++ b/exercises/Exercise13.ql @@ -0,0 +1,186 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + * @kind path-problem + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +int dyn_input_type_mem() { result = 1 } + +int dyn_input_type_val() { result = 2 } + +predicate typeValidationCallMatchesUse(TypeValidationCall call, DynamicInputAccess use) { + exists(FieldAccess f, int expected | + expected = call.getExpectedInputType(use.getArrayOffset().getValue().toInt()) and + f.getQualifier() = use and + ( + expected = dyn_input_type_mem() and f.getTarget().getName() = "ptr" + or + expected = dyn_input_type_val() and f.getTarget().getName() = "val" + ) + ) +} + +/** + * An access of a dynamic input array (of type `dyn_input_t`) + */ +class DynamicInputAccess extends ArrayExpr { + DynamicInputAccess() { + this.getArrayBase().getType().(DerivedType).getBaseType().getName() = "dyn_input_t" + } + + predicate isTypeNotValidated() { + not typeValidationGuardOrIndirect(_, _, _, this.getBasicBlock()) + or + exists(TypeValidationCall call | + typeValidationGuardOrIndirect(_, call, _, this.getBasicBlock()) and + not typeValidationCallMatchesUse(call, this) + ) + } +} + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } + + /** + * Returns the integer value of the expected type specified for the element at `input_index` + */ + int getExpectedInputType(int input_index) { + result = this.getArgument(input_index).getValue().toInt() + } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputParameter() { result = this.getParameter(0) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { } + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input` parameter to a subsequent `ArrayExpr` access. + */ +module InputToAccessConfig implements DataFlow::StateConfigSig { + class FlowState = TTypeValidationState; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(EntrypointFunction ep | ep.getInputParameter() = source.asParameter()) and + none() + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(DynamicInputAccess access | + sink.asExpr() = access.getArrayBase() and + access.isTypeNotValidated() and + none() + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(FunctionCall fc | + fc.getTarget().hasName("lock_input") and + fc.getArgument(0) = node1.asExpr() and + fc = node2.asExpr() + ) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + // leave this predicate as-is for this workshop step + none() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { + // leave this predicate as-is for this workshop step + none() + } +} + +module InputToAccess = DataFlow::MakeWithState; + +import InputToAccess::PathGraph + +from InputToAccess::PathNode source, InputToAccess::PathNode sink +where InputToAccess::hasFlowPath(source, sink) +select sink, source, sink, + "Access to dynamic input array with missing or mismatched type validation." diff --git a/exercises/Exercise14.ql b/exercises/Exercise14.ql new file mode 100644 index 0000000..27f4052 --- /dev/null +++ b/exercises/Exercise14.ql @@ -0,0 +1,117 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { + TypeValidationCall call; + DataFlow::Node node1; + DataFlow::Node node2; + + TypeValidatedState() { none() } + + /** + * Returns the call to `DYN_INPUT_TYPE` that validated the type of the dynamic input array. + */ + TypeValidationCall getCall() { result = call } + + /** + * Returns the node *from* which the state-changing step occurs + */ + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } +} + +from TypeValidatedState state, DataFlow::Node preceding +where DataFlow::localFlowStep(preceding, state.getFstNode()) +select state.getFstNode(), state.getSndNode(), state.getCall() diff --git a/exercises/Exercise15.ql b/exercises/Exercise15.ql new file mode 100644 index 0000000..5a0acf7 --- /dev/null +++ b/exercises/Exercise15.ql @@ -0,0 +1,200 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + * @kind path-problem + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +int dyn_input_type_mem() { result = 1 } + +int dyn_input_type_val() { result = 2 } + +predicate typeValidationCallMatchesUse(TypeValidationCall call, DynamicInputAccess use) { + exists(FieldAccess f, int expected | + expected = call.getExpectedInputType(use.getArrayOffset().getValue().toInt()) and + f.getQualifier() = use and + ( + expected = dyn_input_type_mem() and f.getTarget().getName() = "ptr" + or + expected = dyn_input_type_val() and f.getTarget().getName() = "val" + ) + ) +} + +/** + * An access of a dynamic input array (of type `dyn_input_t`) + */ +class DynamicInputAccess extends ArrayExpr { + DynamicInputAccess() { + this.getArrayBase().getType().(DerivedType).getBaseType().getName() = "dyn_input_t" + } +} + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } + + /** + * Returns the integer value of the expected type specified for the element at `input_index` + */ + int getExpectedInputType(int input_index) { + result = this.getArgument(input_index).getValue().toInt() + } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputParameter() { result = this.getParameter(0) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { + TypeValidationCall call; + DataFlow::Node node1; + DataFlow::Node node2; + + TypeValidatedState() { + this = TTypeValidatedState(call) and + exists(GuardCondition gc | + DataFlow::localFlowStep(node1, node2) and + typeValidationGuard(gc, call, _, node2.asExpr().getBasicBlock()) and + not typeValidationGuard(gc, call, _, node1.asExpr().getBasicBlock()) + ) + } + + /** + * Returns the call to `DYN_INPUT_TYPE` that validated the type of the dynamic input array. + */ + TypeValidationCall getCall() { result = call } + + /** + * Returns the node *from* which the state-changing step occurs + */ + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input` parameter to a subsequent `ArrayExpr` access. + */ +module InputToAccessConfig { + class FlowState = TTypeValidationState; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(EntrypointFunction ep | ep.getInputParameter() = source.asParameter()) and + state instanceof TypeUnvalidatedState + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(DynamicInputAccess access | + sink.asExpr() = access.getArrayBase() and + none() + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(FunctionCall fc | + fc.getTarget().hasName("lock_input") and + fc.getArgument(0) = node1.asExpr() and + fc = node2.asExpr() + ) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + none() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { none() } +} + +module InputToAccess = DataFlow::MakeWithState; + +import InputToAccess::PathGraph + +from InputToAccess::PathNode source, InputToAccess::PathNode sink +where InputToAccess::hasFlowPath(source, sink) +select sink, source, sink, + "Access to dynamic input array with missing or mismatched type validation." diff --git a/exercises/Exercise16.ql b/exercises/Exercise16.ql new file mode 100644 index 0000000..c0b84f8 --- /dev/null +++ b/exercises/Exercise16.ql @@ -0,0 +1,227 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + * @kind path-problem + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +int dyn_input_type_mem() { result = 1 } + +int dyn_input_type_val() { result = 2 } + +predicate typeValidationCallMatchesUse(TypeValidationCall call, DynamicInputAccess use) { + exists(FieldAccess f, int expected | + expected = call.getExpectedInputType(use.getArrayOffset().getValue().toInt()) and + f.getQualifier() = use and + ( + expected = dyn_input_type_mem() and f.getTarget().getName() = "ptr" + or + expected = dyn_input_type_val() and f.getTarget().getName() = "val" + ) + ) +} + +/** + * An access of a dynamic input array (of type `dyn_input_t`) + */ +class DynamicInputAccess extends ArrayExpr { + DynamicInputAccess() { + this.getArrayBase().getType().(DerivedType).getBaseType().getName() = "dyn_input_t" + } +} + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } + + /** + * Returns the integer value of the expected type specified for the element at `input_index` + */ + int getExpectedInputType(int input_index) { + result = this.getArgument(input_index).getValue().toInt() + } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputParameter() { result = this.getParameter(0) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { + TypeValidationCall call; + DataFlow::Node node1; + DataFlow::Node node2; + + TypeValidatedState() { + this = TTypeValidatedState(call) and + exists(GuardCondition gc | + DataFlow::localFlowStep(node1, node2) and + typeValidationGuard(gc, call, _, node2.asExpr().getBasicBlock()) and + not typeValidationGuard(gc, call, _, node1.asExpr().getBasicBlock()) + ) + } + + /** + * Returns the call to `DYN_INPUT_TYPE` that validated the type of the dynamic input array. + */ + TypeValidationCall getCall() { result = call } + + /** + * Returns the node *from* which the state-changing step occurs + */ + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input` parameter to a subsequent `ArrayExpr` access. + */ +module InputToAccessConfig implements DataFlow::StateConfigSig { + class FlowState = TTypeValidationState; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(EntrypointFunction ep | ep.getInputParameter() = source.asParameter()) and + state instanceof TypeUnvalidatedState + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(DynamicInputAccess access | + sink.asExpr() = access.getArrayBase() and + ( + state instanceof TypeUnvalidatedState + or + state instanceof TypeValidatedState and + not typeValidationCallMatchesUse(state.(TypeValidatedState).getCall(), access) + ) + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(FunctionCall fc | + fc.getTarget().hasName("lock_input") and + fc.getArgument(0) = node1.asExpr() and + fc = node2.asExpr() + ) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + state1 instanceof TypeUnvalidatedState and + node1 = state2.(TypeValidatedState).getFstNode() and + node2 = state2.(TypeValidatedState).getSndNode() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { + exists(TypeValidationCall call | + typeValidationGuard(_, call, _, node.asExpr().getBasicBlock()) and + ( + state instanceof TypeUnvalidatedState + or + state.(TypeValidatedState).getCall() != call + ) + ) + } +} + +module InputToAccess = DataFlow::MakeWithState; + +import InputToAccess::PathGraph + +from + InputToAccess::PathNode source, InputToAccess::PathNode sink, string message, Expr additionalExpr +where + InputToAccess::hasFlowPath(source, sink) and + ( + if none() + then ( + message = "No type validation performed before dynamic input access." and + none() + ) else ( + message = "Dynamic input access does not match prior type-validation $@." and + none() + ) + ) +select sink, source, sink, message, additionalExpr, "here" diff --git a/exercises/Exercise5.ql b/exercises/Exercise5.ql index 0413563..f6605fd 100644 --- a/exercises/Exercise5.ql +++ b/exercises/Exercise5.ql @@ -81,7 +81,9 @@ module InputToAccessConfig implements DataFlow::ConfigSig { } predicate isSink(DataFlow::Node sink) { - exists(DynamicInputAccess access | sink.asExpr() = access.getArrayBase()) + exists(DynamicInputAccess access | sink.asExpr() = access.getArrayBase() and + not typeValidationGuard(_, _, _, access.getBasicBlock()) + ) } predicate isBarrier(DataFlow::Node node) { diff --git a/solutions/Exercise13.ql b/solutions/Exercise13.ql new file mode 100644 index 0000000..766a6c8 --- /dev/null +++ b/solutions/Exercise13.ql @@ -0,0 +1,186 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + * @kind path-problem + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +int dyn_input_type_mem() { result = 1 } + +int dyn_input_type_val() { result = 2 } + +predicate typeValidationCallMatchesUse(TypeValidationCall call, DynamicInputAccess use) { + exists(FieldAccess f, int expected | + expected = call.getExpectedInputType(use.getArrayOffset().getValue().toInt()) and + f.getQualifier() = use and + ( + expected = dyn_input_type_mem() and f.getTarget().getName() = "ptr" + or + expected = dyn_input_type_val() and f.getTarget().getName() = "val" + ) + ) +} + +/** + * An access of a dynamic input array (of type `dyn_input_t`) + */ +class DynamicInputAccess extends ArrayExpr { + DynamicInputAccess() { + this.getArrayBase().getType().(DerivedType).getBaseType().getName() = "dyn_input_t" + } + + predicate isTypeNotValidated() { + not typeValidationGuardOrIndirect(_, _, _, this.getBasicBlock()) + or + exists(TypeValidationCall call | + typeValidationGuardOrIndirect(_, call, _, this.getBasicBlock()) and + not typeValidationCallMatchesUse(call, this) + ) + } +} + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } + + /** + * Returns the integer value of the expected type specified for the element at `input_index` + */ + int getExpectedInputType(int input_index) { + result = this.getArgument(input_index).getValue().toInt() + } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputParameter() { result = this.getParameter(0) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { } + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input` parameter to a subsequent `ArrayExpr` access. + */ +module InputToAccessConfig implements DataFlow::StateConfigSig { + class FlowState = TTypeValidationState; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(EntrypointFunction ep | ep.getInputParameter() = source.asParameter()) and + state instanceof TypeUnvalidatedState + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(DynamicInputAccess access | + sink.asExpr() = access.getArrayBase() and + access.isTypeNotValidated() and + state instanceof TypeUnvalidatedState + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(FunctionCall fc | + fc.getTarget().hasName("lock_input") and + fc.getArgument(0) = node1.asExpr() and + fc = node2.asExpr() + ) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + // leave this predicate as-is for this workshop step + none() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { + // leave this predicate as-is for this workshop step + none() + } +} + +module InputToAccess = DataFlow::MakeWithState; + +import InputToAccess::PathGraph + +from InputToAccess::PathNode source, InputToAccess::PathNode sink +where InputToAccess::hasFlowPath(source, sink) +select sink, source, sink, + "Access to dynamic input array with missing or mismatched type validation." diff --git a/solutions/Exercise14.ql b/solutions/Exercise14.ql new file mode 100644 index 0000000..6a0d41b --- /dev/null +++ b/solutions/Exercise14.ql @@ -0,0 +1,125 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { + TypeValidationCall call; + DataFlow::Node node1; + DataFlow::Node node2; + BasicBlock bb2; + + TypeValidatedState() { + this = TTypeValidatedState(call) and + exists(GuardCondition gc | + DataFlow::localFlowStep(node1, node2) and + typeValidationGuard(gc, call, _, node2.asExpr().getBasicBlock()) and + not typeValidationGuard(gc, call, _, node1.asExpr().getBasicBlock()) + ) + } + + /** + * Returns the call to `DYN_INPUT_TYPE` that validated the type of the dynamic input array. + */ + TypeValidationCall getCall() { result = call } + + /** + * Returns the node *from* which the state-changing step occurs + */ + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } +} + +from TypeValidatedState state, DataFlow::Node preceding +where DataFlow::localFlowStep(preceding, state.getFstNode()) +select state.getFstNode(), state.getSndNode(), state.getCall() diff --git a/solutions/Exercise15.ql b/solutions/Exercise15.ql new file mode 100644 index 0000000..4ea0411 --- /dev/null +++ b/solutions/Exercise15.ql @@ -0,0 +1,216 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + * @kind path-problem + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +int dyn_input_type_mem() { result = 1 } + +int dyn_input_type_val() { result = 2 } + +predicate typeValidationCallMatchesUse(TypeValidationCall call, DynamicInputAccess use) { + exists(FieldAccess f, int expected | + expected = call.getExpectedInputType(use.getArrayOffset().getValue().toInt()) and + f.getQualifier() = use and + ( + expected = dyn_input_type_mem() and f.getTarget().getName() = "ptr" + or + expected = dyn_input_type_val() and f.getTarget().getName() = "val" + ) + ) +} + +/** + * An access of a dynamic input array (of type `dyn_input_t`) + */ +class DynamicInputAccess extends ArrayExpr { + DynamicInputAccess() { + this.getArrayBase().getType().(DerivedType).getBaseType().getName() = "dyn_input_t" + } +} + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } + + /** + * Returns the integer value of the expected type specified for the element at `input_index` + */ + int getExpectedInputType(int input_index) { + result = this.getArgument(input_index).getValue().toInt() + } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputParameter() { result = this.getParameter(0) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { + TypeValidationCall call; + DataFlow::Node node1; + DataFlow::Node node2; + + TypeValidatedState() { + this = TTypeValidatedState(call) and + exists(GuardCondition gc | + DataFlow::localFlowStep(node1, node2) and + typeValidationGuard(gc, call, _, node2.asExpr().getBasicBlock()) and + not typeValidationGuard(gc, call, _, node1.asExpr().getBasicBlock()) + ) + } + + /** + * Returns the call to `DYN_INPUT_TYPE` that validated the type of the dynamic input array. + */ + TypeValidationCall getCall() { result = call } + + /** + * Returns the node *from* which the state-changing step occurs + */ + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input` parameter to a subsequent `ArrayExpr` access. + */ +module InputToAccessConfig implements DataFlow::StateConfigSig { + class FlowState = TTypeValidationState; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(EntrypointFunction ep | ep.getInputParameter() = source.asParameter()) and + state instanceof TypeUnvalidatedState + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(DynamicInputAccess access | + sink.asExpr() = access.getArrayBase() and + ( + state instanceof TypeUnvalidatedState + or + state instanceof TypeValidatedState and + not typeValidationCallMatchesUse(state.(TypeValidatedState).getCall(), access) + ) + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(FunctionCall fc | + fc.getTarget().hasName("lock_input") and + fc.getArgument(0) = node1.asExpr() and + fc = node2.asExpr() + ) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + state1 instanceof TypeUnvalidatedState and + node1 = state2.(TypeValidatedState).getFstNode() and + node2 = state2.(TypeValidatedState).getSndNode() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { + exists(TypeValidationCall call | + typeValidationGuard(_, call, _, node.asExpr().getBasicBlock()) and + ( + state instanceof TypeUnvalidatedState + or + state.(TypeValidatedState).getCall() != call + ) + ) + } +} + +module InputToAccess = DataFlow::MakeWithState; + +import InputToAccess::PathGraph + +from InputToAccess::PathNode source, InputToAccess::PathNode sink +where InputToAccess::hasFlowPath(source, sink) +select sink, source, sink, + "Access to dynamic input array with missing or mismatched type validation." diff --git a/solutions/Exercise16.ql b/solutions/Exercise16.ql new file mode 100644 index 0000000..27aca2b --- /dev/null +++ b/solutions/Exercise16.ql @@ -0,0 +1,227 @@ +/** + * @id cpp/check-type-before-use + * @name Check type before use + * @kind path-problem + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.controlflow.Guards + +int dyn_input_type_mem() { result = 1 } + +int dyn_input_type_val() { result = 2 } + +predicate typeValidationCallMatchesUse(TypeValidationCall call, DynamicInputAccess use) { + exists(FieldAccess f, int expected | + expected = call.getExpectedInputType(use.getArrayOffset().getValue().toInt()) and + f.getQualifier() = use and + ( + expected = dyn_input_type_mem() and f.getTarget().getName() = "ptr" + or + expected = dyn_input_type_val() and f.getTarget().getName() = "val" + ) + ) +} + +/** + * An access of a dynamic input array (of type `dyn_input_t`) + */ +class DynamicInputAccess extends ArrayExpr { + DynamicInputAccess() { + this.getArrayBase().getType().(DerivedType).getBaseType().getName() = "dyn_input_t" + } +} + +/** + * A call to `DYN_INPUT_TYPE` + */ +class TypeValidationCall extends FunctionCall { + TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") } + + /** + * Returns the integer value of the expected type specified for the element at `input_index` + */ + int getExpectedInputType(int input_index) { + result = this.getArgument(input_index).getValue().toInt() + } +} + +/** + * Relates a `call` to a `guard`, which uses the result of the call to validate + * equality of the result of `call` against `other` to guard `block`. + */ +predicate typeValidationGuard( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + exists(Expr dest | + DataFlow::localExprFlow(call, dest) and + guard.ensuresEq(dest, other, 0, block, true) and + InputTypesToTypeValidation::hasFlowToExpr(other) + ) +} + +predicate typeValidationGuardOrIndirect( + GuardCondition guard, TypeValidationCall call, Expr other, BasicBlock block +) { + typeValidationGuard(guard, call, other, block) or + typeValidationGuardOrIndirect(guard, call, other, + block.getEnclosingFunction().getACallToThisFunction().getBasicBlock()) +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input_types` parameter to a subsequent use in a GuardCondition. + */ +module InputTypesToTypeValidation = DataFlow::Make; + +module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + exists(EntrypointFunction f | f.getInputTypesParameter() = source.asParameter()) + } + + predicate isSink(DataFlow::Node sink) { + // avoid non-monotonic recursion, as `typeValidationGuard` depends on this config + sink.asExpr() instanceof VariableAccess + } +} + +/** + * An entrypoint that has a `dyn_array_t[2]` `input` parameter and + * `input_types` parameter. + */ +class EntrypointFunction extends Function { + EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) } + + Parameter getInputParameter() { result = this.getParameter(0) } + + Parameter getInputTypesParameter() { result = this.getParameter(1) } +} + +/** + * A flow-state representing the state of dynamic input type validation. + */ +newtype TTypeValidationState = + TTypeUnvalidatedState() or + TTypeValidatedState(TypeValidationCall call) + +/** + * A class describing the type validation state + */ +class TypeValidationState extends TTypeValidationState { + string toString() { + this = TTypeUnvalidatedState() and result = "unvalidated" + or + this = TTypeValidatedState(_) and result = "validated" + } +} + +/** + * A flow-state in which the type of a dynamic input array has *not* been validated. + */ +class TypeUnvalidatedState extends TypeValidationState, TTypeUnvalidatedState { } + +/** + * A flow-state in which the type of a dynamic input array has been validated. + */ +class TypeValidatedState extends TypeValidationState, TTypeValidatedState { + TypeValidationCall call; + DataFlow::Node node1; + DataFlow::Node node2; + + TypeValidatedState() { + this = TTypeValidatedState(call) and + exists(GuardCondition gc | + DataFlow::localFlowStep(node1, node2) and + typeValidationGuard(gc, call, _, node2.asExpr().getBasicBlock()) and + not typeValidationGuard(gc, call, _, node1.asExpr().getBasicBlock()) + ) + } + + /** + * Returns the call to `DYN_INPUT_TYPE` that validated the type of the dynamic input array. + */ + TypeValidationCall getCall() { result = call } + + /** + * Returns the node *from* which the state-changing step occurs + */ + DataFlow::Node getFstNode() { result = node1 } + + /** + * Returns the node *to* which the state-changing step occurs + */ + DataFlow::Node getSndNode() { result = node2 } +} + +/** + * A global data-flow configuration tracking flow from an entrypoint's + * `input` parameter to a subsequent `ArrayExpr` access. + */ +module InputToAccessConfig implements DataFlow::StateConfigSig { + class FlowState = TTypeValidationState; + + predicate isSource(DataFlow::Node source, FlowState state) { + exists(EntrypointFunction ep | ep.getInputParameter() = source.asParameter()) and + state instanceof TypeUnvalidatedState + } + + predicate isSink(DataFlow::Node sink, FlowState state) { + exists(DynamicInputAccess access | + sink.asExpr() = access.getArrayBase() and + ( + state instanceof TypeUnvalidatedState + or + state instanceof TypeValidatedState and + not typeValidationCallMatchesUse(state.(TypeValidatedState).getCall(), access) + ) + ) + } + + predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + exists(FunctionCall fc | + fc.getTarget().hasName("lock_input") and + fc.getArgument(0) = node1.asExpr() and + fc = node2.asExpr() + ) + } + + predicate isAdditionalFlowStep( + DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2 + ) { + state1 instanceof TypeUnvalidatedState and + node1 = state2.(TypeValidatedState).getFstNode() and + node2 = state2.(TypeValidatedState).getSndNode() + } + + predicate isBarrier(DataFlow::Node node, FlowState state) { + exists(TypeValidationCall call | + typeValidationGuard(_, call, _, node.asExpr().getBasicBlock()) and + ( + state instanceof TypeUnvalidatedState + or + state.(TypeValidatedState).getCall() != call + ) + ) + } +} + +module InputToAccess = DataFlow::MakeWithState; + +import InputToAccess::PathGraph + +from + InputToAccess::PathNode source, InputToAccess::PathNode sink, string message, Expr additionalExpr +where + InputToAccess::hasFlowPath(source, sink) and + ( + if sink.getState() instanceof TypeUnvalidatedState + then ( + message = "No type validation performed before dynamic input access." and + additionalExpr = sink.getNode().asExpr() + ) else ( + message = "Dynamic input access does not match prior type-validation $@." and + additionalExpr = sink.getState().(TypeValidatedState).getCall() + ) + ) +select sink, source, sink, message, additionalExpr, "here" diff --git a/solutions/Exercise5.ql b/solutions/Exercise5.ql index daa59b9..e78db6a 100644 --- a/solutions/Exercise5.ql +++ b/solutions/Exercise5.ql @@ -81,7 +81,9 @@ module InputToAccessConfig implements DataFlow::ConfigSig { } predicate isSink(DataFlow::Node sink) { - exists(DynamicInputAccess access | sink.asExpr() = access.getArrayBase()) + exists(DynamicInputAccess access | sink.asExpr() = access.getArrayBase() and + not typeValidationGuard(_, _, _, access.getBasicBlock()) + ) } predicate isBarrier(DataFlow::Node node) {