|
| 1 | +Example: Bad overflow guard |
| 2 | +=========================== |
| 3 | + |
| 4 | +.. container:: semmle-logo |
| 5 | + |
| 6 | + Semmle :sup:`TM` |
| 7 | + |
| 8 | + |
| 9 | +Getting started and setting up |
| 10 | +============================== |
| 11 | + |
| 12 | +To try the examples in this presentation you should download: |
| 13 | + |
| 14 | +- `QL for Eclipse <https://help.semmle.com/ql-for-eclipse/Content/WebHelp/install-plugin-free.html>`__ |
| 15 | +- Snapshot: `ChakraCore <https://downloads.lgtm.com/snapshots/cpp/microsoft/chakracore/ChakraCore-revision-2017-April-12--18-13-26.zip>`__ |
| 16 | + |
| 17 | +More resources: |
| 18 | + |
| 19 | +- To learn more about the main features of QL, try looking at the `QL language handbook <https://help.semmle.com/QL/ql-handbook/>`__. |
| 20 | +- For further information about writing queries in QL, see `Writing QL queries <https://help.semmle.com/QL/learn-ql/ql/writing-queries/writing-queries.html>`__. |
| 21 | + |
| 22 | +.. note:: |
| 23 | + |
| 24 | + To run the queries featured in this training presentation, we recommend you download the free-to-use `QL for Eclipse plugin <https://help.semmle.com/ql-for-eclipse/Content/WebHelp/getting-started.html>`__. |
| 25 | + |
| 26 | + This plugin allows you to locally access the latest features of QL, including the standard QL libraries and queries. It also provides standard IDE features such as syntax highlighting, jump-to-definition, and tab completion. |
| 27 | + |
| 28 | + A good project to start analyzing is `ChakraCore <https://github.com/microsoft/ChakraCore>`__–a suitable snapshot to query is available by visiting the link on the slide. |
| 29 | + |
| 30 | + Alternatively, you can query any project (including ChakraCore) in the `query console on LGTM.com <https://lgtm.com/query/project:2034240708/lang:cpp/>`__. |
| 31 | + |
| 32 | + Note that results generated in the query console are likely to differ to those generated in the QL plugin as LGTM.com analyzes the most recent revisions of each project that has been added–the snapshot available to download above is based on an historical version of the code base. |
| 33 | + |
| 34 | + |
| 35 | +Checking for overflow in C |
| 36 | +========================== |
| 37 | + |
| 38 | +- Arithmetic operations overflow if the result is too large for their type. |
| 39 | +- Developers sometimes exploit this to write overflow checks: |
| 40 | + |
| 41 | +.. code-block:: cpp |
| 42 | +
|
| 43 | + if (v + b < v) { |
| 44 | + handle_error("overflow"); |
| 45 | + } else { |
| 46 | + result = v + b; |
| 47 | + } |
| 48 | +
|
| 49 | +Where might this go wrong? |
| 50 | + |
| 51 | +.. note:: |
| 52 | + |
| 53 | + - In C/C++ we often need to check for whether an operation `overflows <https://en.wikipedia.org/wiki/Integer_overflow>`__. |
| 54 | + - An overflow is when an arithmetic operation, such as an addition, results in a number which is too large to be stored in the type. |
| 55 | + - When an operation overflows, the value “wraps” around. |
| 56 | + - A typical way to check for overflow of an addition, therefore, is whether the result is less than one of the arguments - i.e. the result has “wrapped”. |
| 57 | + |
| 58 | +Integer promotion |
| 59 | +================= |
| 60 | + |
| 61 | +From `https://en.cppreference.com/w/c/language/conversion <https://en.cppreference.com/w/c/language/conversion>`__: |
| 62 | + |
| 63 | +*Integer promotion is the implicit conversion of a value of any integer type with rank less or equal to rank of* ``int`` *... to the value of type* ``int`` *or* ``unsigned int``. |
| 64 | + |
| 65 | +The arguments of the following arithmetic operators undergo implicit conversions: |
| 66 | + |
| 67 | +- binary arithmetic (* / % + - ) |
| 68 | +- relational operators (< > <= >= == !=) |
| 69 | +- binary bitwise operators (& ^ \|) |
| 70 | +- the conditional operator (?:) |
| 71 | + |
| 72 | +.. note:: |
| 73 | + |
| 74 | + - Most of the time integer conversion works fine. However, the rules governing addition in C/C++ are complex, and it easy to get bitten. |
| 75 | + - CPUs generally prefer to perform arithmetic operations on 32 bit or larger integers, as the architectures are optimised to perform those efficiently. |
| 76 | + - The compiler therefore performs “integer promotion” for arguments to arithmetic operations that are smaller than 32 bit. |
| 77 | + |
| 78 | +Checking for overflow in C revisited |
| 79 | +==================================== |
| 80 | + |
| 81 | +Which branch gets executed in this example? What is the value of ``result``? |
| 82 | + |
| 83 | +.. code-block:: cpp |
| 84 | +
|
| 85 | + uint16_t v = 65535; |
| 86 | + uint16_t b = 1; |
| 87 | + uint16_t result; |
| 88 | + if (v + b < v) { |
| 89 | + handle_error("overflow"); |
| 90 | + } else { |
| 91 | + result = v + b; |
| 92 | + } |
| 93 | +
|
| 94 | +.. note:: |
| 95 | + |
| 96 | + In this example the second branch is executed, even though there is a 16-bit overflow, and ``result`` is set to zero. |
| 97 | + |
| 98 | +Checking for overflow in C revisited |
| 99 | +==================================== |
| 100 | + |
| 101 | +Here is the example again, with the conversions made explicit: |
| 102 | + |
| 103 | +.. code-block:: cpp |
| 104 | +
|
| 105 | + uint16_t v = 65535; |
| 106 | + uint16_t b = 1; |
| 107 | + uint16_t result; |
| 108 | + if ((int)v + (int)b < (int)v) { |
| 109 | + handle_error("overflow"); |
| 110 | + } else { |
| 111 | + result = (uint16_t)((int)v + (int)b); |
| 112 | + } |
| 113 | +
|
| 114 | +.. note:: |
| 115 | + |
| 116 | + In this example the second branch is executed, even though there is a 16-bit overflow, and result is set to zero. |
| 117 | + |
| 118 | + Explanation: |
| 119 | + - The two integer arguments to the addition, v and b, are promoted to 32 bit integers. |
| 120 | + - The comparison (<) is also an arithmetic operation, therefore it will also be completed on 32 bit integers. |
| 121 | + - This means that v + b < v will never be true, because v and b can hold at most 216. |
| 122 | + - Therefore, the second branch is executed, but the result of the addition is stored into the result variable. Overflow will still occur as result is a 16 bit integer. |
| 123 | + |
| 124 | +This happens even though the overflow check passed! |
| 125 | + |
| 126 | +.. rst-class:: background2 |
| 127 | + |
| 128 | +Developing a QL query |
| 129 | +===================== |
| 130 | + |
| 131 | +Finding bad overflow guards |
| 132 | + |
| 133 | +QL query: bad overflow guards |
| 134 | +============================= |
| 135 | + |
| 136 | +Let’s look for overflow guards of the form ``v + b < v``, using the classes |
| 137 | +``AddExpr``, ``Variable`` and ``RelationalOperation`` from the ``cpp`` library. |
| 138 | + |
| 139 | +.. rst-class:: build |
| 140 | + |
| 141 | +.. literalinclude:: ../query-examples/cpp/bad-overflow-guard-1.ql |
| 142 | + :language: ql |
| 143 | + |
| 144 | +.. note:: |
| 145 | + |
| 146 | + - When performing `variant analysis <https://semmle.com/variant-analysis>`__, it is usually helpful to write a simple query that finds the simple syntactic pattern, before trying to go on to describe the cases where it goes wrong. |
| 147 | + - In this case, we start by looking for all the *overflow* checks, before trying to refine the query to find all *bad overflow* checks. |
| 148 | + - The select clause defines what this query is looking for: |
| 149 | + - an ``AddExpr``: the expression that is being checked for overflow. |
| 150 | + - a ``RelationalOperation``: the overflow comparison check. |
| 151 | + - a ``Variable``: used as an argument to both the addition and comparison. |
| 152 | + - The where part of the query ties these three QL variables together using `predicates <https://help.semmle.com/QL/ql-handbook/predicates.html>`__ defined in the `standard QL for C/C++ library <https://help.semmle.com/qldoc/cpp/>`__. |
| 153 | + |
| 154 | +QL query: bad overflow guards |
| 155 | +============================= |
| 156 | + |
| 157 | +We want to ensure the operands being added have size less than 4 bytes. |
| 158 | + |
| 159 | +We may want to reuse this logic, so let us create a separate predicate. |
| 160 | + |
| 161 | +Looking at autocomplete suggestions, we see that we can get the type of an expression using the ``getType()`` method. |
| 162 | + |
| 163 | +We can get the size (in bytes) of a type using the ``getSize()`` method. |
| 164 | + |
| 165 | +.. rst-class:: build |
| 166 | + |
| 167 | +.. code-block:: ql |
| 168 | +
|
| 169 | + predicate isSmall(Expr e) { |
| 170 | + e.getType().getSize() < 4 |
| 171 | + } |
| 172 | +
|
| 173 | +.. note:: |
| 174 | + |
| 175 | + - An important part of the query is to determine whether a given expression has a “small” type that is going to trigger integer promotion. |
| 176 | + - We therefore write a helper predicate for small expressions. |
| 177 | + - This predicate effectively represents the set of all expressions in the database where the size of the type of the expression is less than 4 bytes, i.e. less than 32 bits. |
| 178 | + |
| 179 | +QL query: bad overflow guards |
| 180 | +============================= |
| 181 | + |
| 182 | +We can ensure the operands being added have size less than 4 bytes, using our new predicate. |
| 183 | +QL has logical quantifiers like ``exists`` and ``forall``, allowing us to declare variables and enforce a certain condition on them. |
| 184 | +Now our query becomes: |
| 185 | + |
| 186 | +.. rst-class:: build |
| 187 | + |
| 188 | +.. literalinclude:: ../query-examples/cpp/bad-overflow-guard-2.ql |
| 189 | + :language: ql |
| 190 | + |
| 191 | +.. note:: |
| 192 | + |
| 193 | + - Recall from earlier that what makes an overflow check a “bad” check is that all the arguments to the addition are integers smaller than 32 bits. |
| 194 | + - We could write this by using our helper predicate ``isSmall`` to specify that each individual operand to the addition ``isSmall`` (i.e. under 32 bits): |
| 195 | + |
| 196 | + .. code-block:: ql |
| 197 | +
|
| 198 | + isSmall(a.getLeftOperand()) and |
| 199 | + isSmall(a.getRightOperand()) |
| 200 | +
|
| 201 | + - However, this is a little bit repetitive. What we really want to say is that: all the operands of the addition are small. Fortunately, QL provides a ``forall`` formula that we can use in these circumstances. |
| 202 | + - A ``forall`` has three parts: |
| 203 | + - A declaration part, where we can introduce variables. |
| 204 | + - A “range” part, which allows us to restrict those variables. |
| 205 | + - A “condition” part. The ``foral`` as a whole holds if the condition holds for each of the values in the range. |
| 206 | + - In our case: |
| 207 | + - The declaration introduces a variable for Expressions, called ``op``. At this stage, this variable represents all the expressions in the program. |
| 208 | + - The “range” part, ``op = a.getAnOperand()``, restricts ``op`` to being one of the two operands to the addition. |
| 209 | + - The “condition” part, ``isSmall(op)``, says that the ``forall`` holds only if the condition - that the ``op`` is small - holds for everything in the range - i.e. both the arguments to the addition |
| 210 | + |
| 211 | +QL query: bad overflow guards |
| 212 | +============================= |
| 213 | + |
| 214 | +In some cases the result of the addition is cast to a small type of size less than 4 bytes, preventing automatic widening. We don’t want our query to flag these instances. |
| 215 | + |
| 216 | +We can use predicate ``Expr.getExplicitlyConverted()`` to reason about casts that are applied to an expression, adding this restriction to our query: |
| 217 | + |
| 218 | +.. code-block:: ql |
| 219 | +
|
| 220 | + not isSmall(a.getExplicitlyConverted()) |
| 221 | +
|
| 222 | +The final query |
| 223 | +=============== |
| 224 | + |
| 225 | +.. literalinclude:: ../query-examples/cpp/bad-overflow-guard-3.ql |
| 226 | + :language: ql |
| 227 | + |
| 228 | +This query finds a single result, which is `a genuine bug in ChakraCore <https://github.com/Microsoft/ChakraCore/commit/2500e1cdc12cb35af73d5c8c9b85656aba6bab4d>`__. |
0 commit comments