Solution: Exercise 04

The following is the solution for Exercise 04.

For this exercise, make sure you run all commands from the directory:

  /path/to/cbat_tools/docs/exercises/04

Task 1

Use wp to check the function calls in the SSLVerifySignedServerKeyExchange function. Be sure to include --show=refuted-goals when you run wp. How do the two programs differ, with respect to the function calls they can make?

Run wp on the SSLVerifySignedServerKeyExchange function in the two binaries, and compare the function calls (and include --show=refuted-goals):

    $ bap wp \
          --func=SSLVerifySignedServerKeyExchange \
          --compare-func-calls \
          --show=refuted-goals \
          binary/main_1 \
          binary/main_2

When you run this, you will see that wp responds with SAT, meaning that it did indeed find a way to make the second version of the SSLVerifySignedServerKeyExchange function call different functions than the first version.

The output of wp reveals the difference in function calls. Note the refuted goals near the bottom of the output:

SAT!

Model:
  ZF  |->  0x0
  SF  |->  0x0
  RSP |->  0x000000003f800082
  RSI |->  0x0000000000000000
  RDX |->  0x0000000000000000
  RDI |->  0x0000000000000000
  RCX |->  0x0000000000000000
  RBP |->  0x0000000000000000
  RAX |->  0x0000000000000000
  R9  |->  0x0000000000000000
  R8  |->  0x0000000000000000
  PF  |->  0x0
  OF  |->  0x0
  CF  |->  0x0
  AF  |->  0x0
  mem_orig |-> [
    else |-> 0x00]
  mem_mod = mem_orig

Refuted goals:
SSLHashSHA1_final not called in modified: <-- An extra function call
  Z3 Expression: false

This tells us that in the modified version of the program (in binary/main_2), wp found a way to make the second version call SSLHashSHA1_final, when the first version does not.

Task 2

Study the output of wp, and then study the source code of the two programs, to identify where the bug lies in the source code.

The output of wp tells us that SSLHashSHA1_final is called in the second version of the program, but not in the first version of the program. Look at the source code to see how this can happen.

In the first version of the program, in (binary/main_1.c)[./binary/main_1.c]), there is an important line:

/* Check that the key exchange is signed correctly. */
status SSLVerifySignedServerKeyExchange(hash *data, hash *signature) {

    status code;

    if ((code = ReadyHash(data)) != 0)
        return cleanUp(data, code);
    if ((code = SSLHashSHA1_update(data)) != 0)
        return cleanUp(data, code);
        return cleanUp(data, code);            <-- Why is this here?
    if ((code = SSLHashSHA1_final(data)) != 0)
        return cleanUp(data, code);

    code = sslRawVerify(data, signature);

    return cleanUp(data, code);

}

There is an extra return cleanUp(data, code) that occurs in this function. This looks very much like a simple typo/mistake. The extra return cleanUp(data, code) is indented, so it is easy to think that it is a part of the body of the if statement that appears just two lines above it. However, there are no curly braces here, so that extra return cleanUp(data, code) is actually not a part of that if statement. It is really this:

/* Check that the key exchange is signed correctly. */
status SSLVerifySignedServerKeyExchange(hash *data, hash *signature) {

    status code;

    if ((code = ReadyHash(data)) != 0)
        return cleanUp(data, code);
    if ((code = SSLHashSHA1_update(data)) != 0)
        return cleanUp(data, code);
    return cleanUp(data, code);            <-- Correct indentation
    if ((code = SSLHashSHA1_final(data)) != 0)
        return cleanUp(data, code);

    code = sslRawVerify(data, signature);

    return cleanUp(data, code);

}

With the indentation fixed like this, now it is clear that the last if statement will never be executed, because this function will always return before it gets to it. Even worse, that very crucial sslRawVerify function that occurs at the end of the function will never be called either! Here we have the bug. This function returns before it ever verifies the SSL key exchange.

But notice that this is very easy to miss because of the incorrect indentation, and the missing curly braces.

In the second version of the program, in (binary/main_2.c)[./binary_main_2.c], the extra return cleanUp(data, code) has been removed:

/* Check that the key exchange is signed correctly. */
status SSLVerifySignedServerKeyExchange(hash *data, hash *signature) {

    status code;

    if ((code = ReadyHash(data)) != 0)
        return cleanUp(data, code);
    if ((code = SSLHashSHA1_update(data)) != 0)
        return cleanUp(data, code);
    if ((code = SSLHashSHA1_final(data)) != 0)
        return cleanUp(data, code);

    code = sslRawVerify(data, signature);

    return cleanUp(data, code);

}

In this second (fixed) version of the function, execution can continue through the entirety of the function, and crucially, that means sslRawVerify will be called when it is supposed to be called.

Go back to the list of exercises.