From 543121cd9f5f943f6df043a0d79ceb7c6554e1ac Mon Sep 17 00:00:00 2001 From: Kevin Backhouse Date: Mon, 18 Nov 2019 15:56:37 +0000 Subject: [PATCH] Demo of MIN_INT negate query. --- CodeQL_Queries/cpp/MinIntNegate/.gitignore | 2 + .../cpp/MinIntNegate/00_MinIntNegate.ql | 29 +++++ .../cpp/MinIntNegate/01_MinIntNegate.ql | 29 +++++ .../cpp/MinIntNegate/02_MinIntNegate.ql | 34 ++++++ .../cpp/MinIntNegate/03_MinIntNegate.ql | 36 +++++++ .../cpp/MinIntNegate/04_MinIntNegate.ql | 47 ++++++++ .../cpp/MinIntNegate/05_MinIntNegate.ql | 63 +++++++++++ .../cpp/MinIntNegate/06_MinIntNegate.ql | 75 +++++++++++++ .../cpp/MinIntNegate/07_MinIntNegate.ql | 90 ++++++++++++++++ CodeQL_Queries/cpp/MinIntNegate/README.md | 33 ++++++ CodeQL_Queries/cpp/MinIntNegate/test.cpp | 102 ++++++++++++++++++ 11 files changed, 540 insertions(+) create mode 100644 CodeQL_Queries/cpp/MinIntNegate/.gitignore create mode 100644 CodeQL_Queries/cpp/MinIntNegate/00_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/01_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/02_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/03_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/04_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/05_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/06_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/07_MinIntNegate.ql create mode 100644 CodeQL_Queries/cpp/MinIntNegate/README.md create mode 100644 CodeQL_Queries/cpp/MinIntNegate/test.cpp diff --git a/CodeQL_Queries/cpp/MinIntNegate/.gitignore b/CodeQL_Queries/cpp/MinIntNegate/.gitignore new file mode 100644 index 0000000..49c2921 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/.gitignore @@ -0,0 +1,2 @@ +MinIntNegateDB +test.o diff --git a/CodeQL_Queries/cpp/MinIntNegate/00_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/00_MinIntNegate.ql new file mode 100644 index 0000000..2847886 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/00_MinIntNegate.ql @@ -0,0 +1,29 @@ +/** + * @name 00_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards + +// Find this pattern: +// +// ``` +// if (x < 0) { +// x = -x; +// } +// ``` +// +// If the value of `x` is `0x80000000` then this will not make the value of `x` positive. +from GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Variable v, Expr use +where + guard.(LTExpr).getLeftOperand() = v.getAnAccess() and + guard.(LTExpr).getRightOperand().getValue().toInt() = 0 and + guard.controls(block, true) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = v.getAnAccess() +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", v, + v.getName() diff --git a/CodeQL_Queries/cpp/MinIntNegate/01_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/01_MinIntNegate.ql new file mode 100644 index 0000000..c4798ab --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/01_MinIntNegate.ql @@ -0,0 +1,29 @@ +/** + * @name 01_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards + +// The previous query had an incorrect result at test.cpp, line 20: +// +// if (s->myfield < 0) { +// s->myfield = -t->myfield; +// } +// +// The problem is that the query used `Variable`, which includes fields. +// So here we restrict the query to use `LocalScopeVariable` instead. +from + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, LocalScopeVariable v, Expr use +where + guard.(LTExpr).getLeftOperand() = v.getAnAccess() and + guard.(LTExpr).getRightOperand().getValue().toInt() = 0 and + guard.controls(block, true) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = v.getAnAccess() +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", v, + v.getName() diff --git a/CodeQL_Queries/cpp/MinIntNegate/02_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/02_MinIntNegate.ql new file mode 100644 index 0000000..c1865e6 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/02_MinIntNegate.ql @@ -0,0 +1,34 @@ +/** + * @name 02_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.GlobalValueNumbering + +// The previous query, 01_MinIntNegate, eliminated a bad result +// from 00_MinIntNegate, but it also lost a good result. +// The missing result is test.cpp, line 14: +// +// if (s->myfield < 0) { +// s->myfield = -s->myfield; +// } +// +// The problem is that `s->myfield` is not a `LocalScopeVariable`. +// The solution is to use the GlobalValueNumbering library, which +// is a more general way to find expressions that compute the same +// value. +from GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2 +where + guard.(LTExpr).getLeftOperand() = use1 and + guard.(LTExpr).getRightOperand().getValue().toInt() = 0 and + guard.controls(block, true) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = use2 and + globalValueNumber(use1) = globalValueNumber(use2) +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", + use2, use2.toString() diff --git a/CodeQL_Queries/cpp/MinIntNegate/03_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/03_MinIntNegate.ql new file mode 100644 index 0000000..3b7fb1f --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/03_MinIntNegate.ql @@ -0,0 +1,36 @@ +/** + * @name 03_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.GlobalValueNumbering + +// The previous query only worked for `x < 0` and not for the +// equivalent `0 > x`. It's easier to handle both if we refactor +// the logic into a separate predicate. + +/** Holds if `cond` is a comparison of the form `lhs < rhs`. */ +predicate lessThan(Expr cond, Expr lhs, Expr rhs) { + cond.(LTExpr).getLeftOperand() = lhs and + cond.(LTExpr).getRightOperand() = rhs + or + cond.(GTExpr).getLeftOperand() = rhs and + cond.(GTExpr).getRightOperand() = lhs +} + +from + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, Expr zero +where + lessThan(guard, use1, zero) and + zero.getValue().toInt() = 0 and + guard.controls(block, true) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = use2 and + globalValueNumber(use1) = globalValueNumber(use2) +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", + use2, use2.toString() diff --git a/CodeQL_Queries/cpp/MinIntNegate/04_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/04_MinIntNegate.ql new file mode 100644 index 0000000..43ff26a --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/04_MinIntNegate.ql @@ -0,0 +1,47 @@ +/** + * @name 04_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.GlobalValueNumbering + +// Let's also add support for <= and >=. + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + */ +predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) { + cond.(LTExpr).getLeftOperand() = lhs and + cond.(LTExpr).getRightOperand() = rhs and + isStrict = true + or + cond.(GTExpr).getLeftOperand() = rhs and + cond.(GTExpr).getRightOperand() = lhs and + isStrict = true + or + cond.(LEExpr).getLeftOperand() = lhs and + cond.(LEExpr).getRightOperand() = rhs and + isStrict = false + or + cond.(GEExpr).getLeftOperand() = rhs and + cond.(GEExpr).getRightOperand() = lhs and + isStrict = false +} + +from + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, Expr zero +where + lessThan(guard, use1, zero, _) and + zero.getValue().toInt() = 0 and + guard.controls(block, true) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = use2 and + globalValueNumber(use1) = globalValueNumber(use2) +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", + use2, use2.toString() diff --git a/CodeQL_Queries/cpp/MinIntNegate/05_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/05_MinIntNegate.ql new file mode 100644 index 0000000..c4f3174 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/05_MinIntNegate.ql @@ -0,0 +1,63 @@ +/** + * @name 05_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.GlobalValueNumbering + +// The previous query added support for <= and >=, but failed to +// find any new results. That's because the comparison is 0 <= x, +// so the operands are the wrong way around. We can solve this by +// adding a recursive predicate which swaps them. + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + */ +predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) { + cond.(LTExpr).getLeftOperand() = lhs and + cond.(LTExpr).getRightOperand() = rhs and + isStrict = true + or + cond.(GTExpr).getLeftOperand() = rhs and + cond.(GTExpr).getRightOperand() = lhs and + isStrict = true + or + cond.(LEExpr).getLeftOperand() = lhs and + cond.(LEExpr).getRightOperand() = rhs and + isStrict = false + or + cond.(GEExpr).getLeftOperand() = rhs and + cond.(GEExpr).getRightOperand() = lhs and + isStrict = false +} + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + * `branch` is true if the comparison is true and false if it is not. + */ +predicate lessThanWithNegate(Expr cond, Expr lhs, Expr rhs, boolean isStrict, boolean branch) { + branch = true and lessThan(cond, lhs, rhs, isStrict) + or + // (x < y) == !(y <= x) + lessThanWithNegate(cond, rhs, lhs, isStrict.booleanNot(), branch.booleanNot()) +} + +from + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, + Expr zero, boolean branch +where + lessThanWithNegate(guard, use1, zero, _, branch) and + zero.getValue().toInt() = 0 and + guard.controls(block, branch) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = use2 and + globalValueNumber(use1) = globalValueNumber(use2) +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", + use2, use2.toString() diff --git a/CodeQL_Queries/cpp/MinIntNegate/06_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/06_MinIntNegate.ql new file mode 100644 index 0000000..3b59139 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/06_MinIntNegate.ql @@ -0,0 +1,75 @@ +/** + * @name 06_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.GlobalValueNumbering +import semmle.code.cpp.dataflow.DataFlow + +// Let's add local dataflow, so that we can also handle cases like this: +// +// ``` +// bool b = x < 0; +// if (b) { +// x = -x; +// } +// ``` + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + */ +predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) { + cond.(LTExpr).getLeftOperand() = lhs and + cond.(LTExpr).getRightOperand() = rhs and + isStrict = true + or + cond.(GTExpr).getLeftOperand() = rhs and + cond.(GTExpr).getRightOperand() = lhs and + isStrict = true + or + cond.(LEExpr).getLeftOperand() = lhs and + cond.(LEExpr).getRightOperand() = rhs and + isStrict = false + or + cond.(GEExpr).getLeftOperand() = rhs and + cond.(GEExpr).getRightOperand() = lhs and + isStrict = false +} + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + * `branch` is true if the comparison is true and false if it is not. + */ +predicate lessThanWithNegate(Expr cond, Expr lhs, Expr rhs, boolean isStrict, boolean branch) { + branch = true and lessThan(cond, lhs, rhs, isStrict) + or + // (x < y) == !(y <= x) + lessThanWithNegate(cond, rhs, lhs, isStrict.booleanNot(), branch.booleanNot()) + or + // bool b = x < 0; + // if (b) { ... } + exists(Expr prev | + DataFlow::localExprFlow(prev, cond) and + lessThanWithNegate(prev, lhs, rhs, branch, isStrict) + ) +} + +from + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, + Expr zero, boolean branch +where + lessThanWithNegate(guard, use1, zero, _, branch) and + zero.getValue().toInt() = 0 and + guard.controls(block, branch) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = use2 and + globalValueNumber(use1) = globalValueNumber(use2) +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", + use2, use2.toString() diff --git a/CodeQL_Queries/cpp/MinIntNegate/07_MinIntNegate.ql b/CodeQL_Queries/cpp/MinIntNegate/07_MinIntNegate.ql new file mode 100644 index 0000000..b9fa0f3 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/07_MinIntNegate.ql @@ -0,0 +1,90 @@ +/** + * @name 07_MinIntNegate + * @description Negating MIN_INT is an integer overflow + * @kind problem + * @id cpp/min-int-negate + * @problem.severity warning + */ + +import cpp +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.GlobalValueNumbering +import semmle.code.cpp.dataflow.DataFlow + +// The guards library automatically handles negations like this for us: +// +// ``` +// if (!(x < 0)) { +// // Do nothing. +// } else { +// x = -x; +// } +// ``` +// +// But it does not handle cases where dataflow is involved. For example: +// +// ``` +// bool b = !(0 <= x); +// if (b) { +// x = -x; +// } +// ``` +// +// It's easy to fix by adding one more recursive clause to `lessThanWithNegate`. + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + */ +predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) { + cond.(LTExpr).getLeftOperand() = lhs and + cond.(LTExpr).getRightOperand() = rhs and + isStrict = true + or + cond.(GTExpr).getLeftOperand() = rhs and + cond.(GTExpr).getRightOperand() = lhs and + isStrict = true + or + cond.(LEExpr).getLeftOperand() = lhs and + cond.(LEExpr).getRightOperand() = rhs and + isStrict = false + or + cond.(GEExpr).getLeftOperand() = rhs and + cond.(GEExpr).getRightOperand() = lhs and + isStrict = false +} + +/** + * Holds if `cond` is a comparison of the form `lhs < rhs`. + * `isStrict` is true for < and >, and false for <= and >=. + * `branch` is true if the comparison is true and false if it is not. + */ +predicate lessThanWithNegate(Expr cond, Expr lhs, Expr rhs, boolean isStrict, boolean branch) { + branch = true and lessThan(cond, lhs, rhs, isStrict) + or + // (x < y) == !(y <= x) + lessThanWithNegate(cond, rhs, lhs, isStrict.booleanNot(), branch.booleanNot()) + or + // (!(x < y) == branch) == ((x < y) == !branch) + lessThanWithNegate(cond.(NotExpr).getOperand(), lhs, rhs, isStrict, branch.booleanNot()) + or + // bool b = x < 0; + // if (b) { ... } + exists(Expr prev | + DataFlow::localExprFlow(prev, cond) and + lessThanWithNegate(prev, lhs, rhs, branch, isStrict) + ) +} + +from + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, + Expr zero, boolean branch +where + lessThanWithNegate(guard, use1, zero, _, branch) and + zero.getValue().toInt() = 0 and + guard.controls(block, branch) and + block.contains(unaryMinus) and + unaryMinus.getOperand() = use2 and + globalValueNumber(use1) = globalValueNumber(use2) +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", + use2, use2.toString() diff --git a/CodeQL_Queries/cpp/MinIntNegate/README.md b/CodeQL_Queries/cpp/MinIntNegate/README.md new file mode 100644 index 0000000..4a37e5d --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/README.md @@ -0,0 +1,33 @@ +# Unary minus integer overflow gotcha + +This demo is about building a query to find the bug from +[this tweet by Nico Waisman](https://twitter.com/nicowaisman/status/1147178477692608512). + +This is the pattern that we're interested in: + +``` +int32_t Size = user_supplied32(); +if(Size < 0) { + Size = -Size; +} +``` + +The developer who wrote this probably thinks that `Size` is now a positive number. +But they have forgotten that `MIN_INT` will trigger an integer overflow and remain +negative. +So if the subsequent code relies on `Size` being positive, then something could +go badly wrong. + +## Generating a snapshot. + +This directory contains a unit test file, [`test.cpp`](test.cpp), +which you can use to create a small database for testing, like this: + +``` +codeql database create MinIntNegateDB --language=cpp --command="g++ -c test.cpp" +``` + +This creates a database in a sub-directory named `MinIntNegateDB`. +You can add this database in the +[CodeQL for VSCode extension](https://github.com/github/vscode-codeql) +by clicking the `+` button. diff --git a/CodeQL_Queries/cpp/MinIntNegate/test.cpp b/CodeQL_Queries/cpp/MinIntNegate/test.cpp new file mode 100644 index 0000000..b8da358 --- /dev/null +++ b/CodeQL_Queries/cpp/MinIntNegate/test.cpp @@ -0,0 +1,102 @@ +unsigned int test000(int x) { + if (x < 0) { + x = -x; + } + return x; +} + +struct MyStruct { + int myfield; +}; + +void test001(MyStruct *s) { + if (s->myfield < 0) { + s->myfield = -s->myfield; + } +} + +void test002(MyStruct *s, MyStruct *t) { + if (s->myfield < 0) { + s->myfield = -t->myfield; + } +} + +unsigned int test003(int x) { + if (0 > x) { + x = -x; + } + return x; +} + +unsigned int test004(int x) { + if (x > 0) { + // Do nothing. + } else { + x = -x; + } + return x; +} + +unsigned int test005(int x) { + if (0 <= x) { + // Do nothing. + } else { + x = -x; + } + return x; +} + +unsigned int test006(int x) { + if (!(0 > x)) { + // Do nothing. + } else { + x = -x; + } + return x; +} + +unsigned int test007(int x) { + if (!(x > 0)) { + x = -x; + } + return x; +} + +unsigned int test008(int x) { + if (!(0 <= x)) { + x = -x; + } + return x; +} + +unsigned int test009(int x) { + if (!!(x < 0)) { + x = -x; + } + return x; +} + +unsigned int test010(int x) { + bool b = x < 0; + if (b) { + x = -x; + } + return x; +} + +unsigned int test011(int x) { + bool b = !(0 <= x); + if (b) { + x = -x; + } + return x; +} + +unsigned int test012(int x) { + bool b = x < 0; + bool c = !b; + if (!c) { + x = -x; + } + return x; +}