Fix unsafe bounds check in ssl_load_session()

[hanno-becker]

Summary: This fixes #659. See there for more information, as well as the commit message of aa7503d.

Internal Reference: IOTSSL-1046.

[mpg]

I'm sorry, I don't think I like the casting to an int.

While I agree it's correct in this case, we need to rely on external knowledge (that the value is unsigned 24-bit and the so far undocumented assumption that int is at least 25-bit) to make sure it's correct. I think it's a problem for two reasons:

• code correctness should be as local as possible, ie rely as few as possible on knowledge of eg the possible range of values previously assigned to a variable. It's important both for humans and for static analyzers (the fewer false positives due to undocumented assumptions about int size, the better).
• basic coding idioms should be as uniform as possible: if we end up using the int cast most of the time, and another idiom when it's possible than len > INT_MAX, the result is confusing to readers and harder to maintain.

For these reasons, I think I prefer Guido's proposal. It turns out it's also currently the most used in the library (grep 'end < p' library/*.c finds 17 occurrences vs 1 for grep '(int).*end' library/*.c).

[mpg]

I think "unsafe bounds check" is alarming enough that people might question why it's in the Bugfix section, not Security. We might want to make it clear that this is not exploitable without breaking the authentication of the session ticket.

[hanno-becker]

Fixed.

[gilles-peskine-arm]

I'm ok with the wording now, but I'd also be ok with classifying this under “Changes” with wording like “Improve robustness”, since it's fixing a second line of defense.

[hanno-becker]

@mpg Thanks for your comments, I changed the PR.

@mpg @AndrzejKurek Please re-review.

[mpg]

@hanno-arm Thanks for making the changes. However I'm not entirely happy yet, as correctness is still not as local as it could be (we need to remember that end < p was checked and the beginning, and then know exactly how p was updated up to the present check), and as a result the idiom is not as uniform as it could be.

I'd like us to use the following idiom everywhere:

if( end < p || len > (size_t)( end - p ) )

This idioms works a 100% of the time with 0 previous knowledge assumed.

If, inside a particular function, the compiler can prove that end < p is always true, then it will remove that check. However I don't think that's the kind of optimisation we should worry about ourselves, as it's a very small one which is trumped by obvious code correctness.

(I think micro optimisation trumps readability only in the core loop of computation-heavy crypto primitives. Parsing code is quite the opposite: it's not nearly as CPU intensive, while being extremely sensitive to bounds issues. Please note that I'm only talking about micro optimisations here, obviously if we have a choice between a quadratic and a linear algorithm, or a memory usage of N vs 2N, that kind of optimisation is worth considering.)

[hanno-becker]

@mpg Thanks for your detailed comments! You persuaded me that in principle your proposal, matching Guido's, is the safest to use.

I am not concerned about performance, but rather about code size - we have a large number of bounds checks in the library, and if we add end < p in many places where they are not needed because we maintain the precondition p <= end (or potentially checking for it once in the beginning of the function), this might result in a non-negligible increase of code-size.
In general, we must allow ourselves some extend of informal reasoning as a justification for the omission of checks. For example, internal functions don't always check that pointers are not NULL, because we rely on callers to not calling them with invalid parameters. Similarly, I think it should be acceptable to assume (or once check it, if it's not a precondition) that end >= p and to reason that it need not be checked in subsequent bounds checks in the same function.

[mpg]

@hanno-arm I see your point. Code size is indeed a more serious issue than performance, and worth considering. I must say I'm not sure what I think any more in that particular case. On one hand, you're making good points. On the other hand, I investigated a bit and found the code size impact for checking for end < p before we do end - p every single time would be about 300 bytes (or less depending on compiler value tracking), which seems a relatively low price to pay for some increased safety / readability / ease of maintenance.

Here's how I got this number, so you can criticize if you think I'm mistaken: egrep '\<end\>.*-.*\<p\>' library/*.c | wc -l prints 76. Then I used the following file:

#include <stdlib.h>

int hanno( size_t len, const unsigned char *p, const unsigned char *end ) {
    return( (int) len > end - p );
}

int guido( size_t len, const unsigned char *p, const unsigned char *end ) {
    return( p > end || len > (size_t)( end - p ) );
}

and observed the size of the functions with: arm-none-eabi-gcc -Wall -Wextra -Os -c -march=armv6-m -mthumb foo.c and arm-none-eabi-objdump -d foo.o which shows a 4 bytes difference.

I would be interested in doing more tests to see if the compiler can optimize away some of the superfluous end < p tests in larger functions, but I'm running out of time for today.

Of course in an ideal world we would have formal verification of bounds for all our parsing functions, so we could confidently remove any redundant check and be sure that we still have enough check, and that it will remain that way when adding code in the middle of the function later, but we don't live in that world yet.

[hanno-becker]

@mpg Thank you for doing that analysis and for explaining how you got the numbers!

I think the fact that this simple example would allow us to save 300 Bytes of code indicates that we should take the underlying question seriously: Which implicit invariants are simple enough to reason about that we don't need to assert them, and which are complex enough that we do want to include an assertion? While I think we must be careful not to allow too complex informal reasoning in the former approach, I also think we shouldn't too easily fall back to the former. In this particular case, for example, I think it is justifiable to omit the p <= end check, because p is solely under the control of the function body - for functions using various ASN.1 parsing or writing functions, it's already more delicate, because those modify the pointers they are given.

Also, a check like if( end < p || len > (size_t)( end - p ) ) mixes an assertion that should never fail unless we made a mistake with a genuine check that we must expect to fail if len is uncontrolled (***) - however, that separation is not immediate by looking at the code. If we want to assert p <= end, say, I think it would be more appropriate to add it as a separate check, and return an analogue of INTERNAL_ERROR on failure, to allow us to distinguish it from a bounds violation due to invalid arguments.

(***) In this case, one might even be tempted to argue that len > (size_t)( end - p ) never fails because otherwise the ticket was invalid, which should never happen - but this certainly is an example of a too complex reasoning with too many assumptions.

[gilles-peskine-arm]

I find this check really strange. What is the semantics of the arguments buf and len? They designate a buffer, so buf must be the start of a buffer of len bytes. end has to be >= buf.

And below, end - p is len. The one check at this point should be sizeof( mbedtls_ssl_session ) <= len.

[hanno-becker]

@gilles-peskine-arm This again is a question of what we take as guaranteed and what not. If we assume that the caller uses sane arguments, then yes, we can omit the check. If not, we have to include it to guard a wraparound. OTOH, even if buf + len doesn't overflow, we cannot check that buf, ..., buf + len - 1 is actually valid memory, we have to assume it. So I'd agree that it's cleaner to remove the check end < p here.

[hanno-becker]

And below, end - p is len. The one check at this point should be sizeof( mbedtls_ssl_session ) <= len.

I prefer to leave that to the compiler and aim at using a single idiom for bounds checking.

[gilles-peskine-arm]

The remaining length in the buffer is len - sizeof( mbedtls_ssl_session ). The current code is ok, but I'd find this bit more readable if it used len -= sizeof( mbedtls_ssl_session ) at the same time as incrementing p, and then checked len >= 3. However I'm ok with keeping the current structure because it's more uniform with other parsing code in the library.

[hanno-becker]

These are two different idioms to use for bounds checks: Either incrementing p, keeping end, and somehow inferring the remaining size from p and end, or incrementing p while decrementing a length parameter like len. I think the former is more commonly used, so I'd prefer to stick to it here.

[gilles-peskine-arm]

On the topic of p <= end, I am strongly in favor of maintaining this invariant everywhere. A check for p <= end should be rare because this should be checked before incrementing p.

[hanno-becker]

@mpg @gilles-peskine-arm @AndrzejKurek Please re-review.

[gilles-peskine-arm]

Style: we normally put a space between (type) and ( value ).

[mpg]

I don't think that's the case: egrep '(int|char|size_t)\)\(' library/*.c | wc -l prints 307 while egrep '(int|char|size_t)\) \(' library/*.c | wc -l only prints 93. Admittedly, one of them should print 0 if we were fully consistent, but most of the time we're not putting a space here.

[gilles-peskine-arm]

Oh. So it's (foo_t) single_word with a space (~90% prevalence) but (foo_t)( more complex expression ) (~80% prevalence). Can we switch to a standard whitespace style in 3.0?

[mpg]

On the topic of checking for p > end, I accept @hanno-arm's and @gilles-peskine-arm's views.