FunctionModels

The FunctionModels plugin can be used to reduce path explosion. It works by replacing typical libc functions with a symbolic expression that represents that function’s return value. The FunctionModels plugin currently supports the following libc functions:

  • strcpy

  • strncpy

  • strcat

  • strncat

  • strcmp

  • strstrncmp

  • memcpy

  • memcmp

  • printf

  • fprintf

For example, strlen is typically implemented as follows:

// Adapted from  µlibc
size_t strlen(const char *s) {
    for (const char *p = s; *p; p++) ;

    return p - s;
}

If the input string s is symbolic, each iteration of the for loop will result in a state fork. This will quickly grow intractible as the length of the input string grows. Instead of symbolically executing this function and forking states, the FunctionModels plugin will return a symbolic expression that essentially “merges” these states and return a symbolic expression that describes the string length (see the strlenHelper function here to see how this is done).

The astute reader will note that while this will reduce the number of forked states that S2E must explore, it will do so by increasing the complexity of the path constraints. This may put pressure on the constraint solver and cause it to take more time to solve path constraints. It is up to the user to decide if this is an acceptable trade-off.

The FunctionModels plugin uses s2e.so to replace the function calls (e.g. strlen, memcpy, etc.) with calls to the functions in guest/linux/function_models/models.c. The functions in models.c determine whether any of the function arguments are symbolic, and if so invoke the FunctionModels plugin to generate the appropriate symbolic expression. Function call replacement relies on the target program being dynamically linked, so you cannot use function models on statically-linked binaries.

To use function models, enable the FunctionModels plugin in your S2E configuration file and use LD_PRELOAD to load s2e.so in your bootstrap.sh script. If you are using s2e-env you will be informed at project creation time whether you can use the FunctionModels plugin. Note however that by default s2e-env will not automatically enable the FunctionModels plugin.

Testing

There is a test suite suite available in guest/linux/function_models/models_test.c. This test suite is compiled along with the guest tools and placed in $S2EDIR/build-s2e/guest-tools{32,64}/linux/function_models. It can be used with the s2e-env new_project command to run in a guest virtual machine. You should see the “Good Model” message in S2E’s debug output.

Options

This plugin does not have any options.