For this exercise, make sure you run all commands from the directory:
/path/to/cbat_tools/docs/exercises/04
In the binary folder, there are two programs: binary/main_1 and binary/main_2. Their source code resides at binary/main_1.c and binary/main_2.c.
These two programs are simplified versions of some code from Apple's SSL library, and they mimic a real bug that was discovered in Apple's SSL library a few years back (it was called the "goto fail" exploit).
The important function is called SSLVerifySignedServerKeyExchange. The first version of this function (in binary/main_1) has a bug. In the second version (in binary/main_2), the bug is fixed.
This particular bug is revealed by analyzing the function calls that can occur inside SSLVerifySignedServerKeyExchange. It turns out that the bug makes it so that different function calls can occur in the buggy and fixed versions.
Your task is to use wp to find the bug. To do that, complete the following tasks:
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?wp, and then study the source code of the two programs, to identify where the bug lies in the source code.To see the solution, click here.