Debugging Frama-C analyses: better privacy with C-Reduce

Frama-C has a somewhat obscure plug-in called Obfuscator, whose original purpose was to help industrial users give the Frama-C developers enough information about confidential use cases, for debugging and optimizations. However, sharing proprietary code is never easy: is the obfuscation good enough? Are there legal issues involved? Is it worth the effort, or should I just try to find the problem myself? A better approach consists in not sending any information at all: just minimize the code using C-Reduce, while keeping the undesired behavior intact, so that the Frama-C team can reproduce and explain it. In this post, we briefly describe a new script to help our industrial partners achieve this with minimal effort.

C-Reduce: the most useful code slicer since the invention of sliced bread

C-Reduce is a powerful open-source tool developed by Prof. John Regehr which allows automatic reduction of C source code while following a criterion. A sort of sophisticated, non-semantics-preserving code slicer. The only “semantics” that is preserved by C-Reduce is that of a shell script, given by the user, which says, for a given (reduced) source program, whether it is good or bad.

C-Reduce applies a series of well-crafted passes to transform the program, each time applying the shell script to check if the resulting program is still valid, backtracking otherwise.

In practice, it means that, once a good criterion has been found (e.g., “this source program, given this set of command line options, makes Frama-C crash”), C-Reduce will run the script thousands of times, slicing away code until it reaches a minimal file that exhibits the problem. This is often a shameful, but nevertheless desired, moment.

Minimizing the setup cost

Once you get used to C-Reduce, you often wonder: why didn’t I try it before? The main reason more people still do not use it is the (perceived) setup cost: the impression that “oh, but if I just try a little bit more, I’ll find the bug faster than setting up a script to run C-Reduce”. Therefore, we decided to add a script to Frama-C that will make that cost even lower: for “fatal” crashes – those that produce long stack traces with a “Please report” message at the end – running C-Reduce should be as simple as (1) having it installed, and (2) running:

${FRAMAC_SHARE}/analysis-scripts/creduce.sh <file.c> <command line options>

This will create a creducing directory inside the present working directory, copy <file.c> inside it, and start applying C-Reduce. During its execution, C-Reduce will display which steps it is trying and how much it has reduced the file (in number of bytes). You can always press Ctrl+C if you want, and take a look at the resulting creducing/<file.c>.

No need to obfuscate what is not sent

C-Reduce automatically “obfuscates” the source, since its many transformations include renaming variables and labels, removing declarations and statements, and overall radically transforming the program. As a bonus, the resuting file is often simple enough that the problem becomes evident for the Frama-C team, speeding up its resolution.

Extending the script to other cases

The main difficulty when setting up C-Reduce is to avoid “trivial” reductions: it has a tendency to work very literally, in a way that people are not used to. “But it reduced my program to an invalid statement!”, “Well, you never said your program had to be valid C, did you?”.

Currently, the script distributed with Frama-C only works for fatal crashes, which are easy to identify. For more subtle cases (e.g. a plug-in resulting in an error, but without crashing), it is often necessary to add conditions such as | grep "<expected expression>", or “Frama-C parsing of the source must succeed”, to ensure the reduced program still maintains essential information. In future versions of the script, we expect to give users more options to deal with such cases, to improve the usability of the script.

A few bonuses: hints when using C-Reduce

Besides setting up the initial script for the user, and performing some sanity checks, our creduce.sh script also tries to provide useful hints; for instance, since C-Reduce often runs thousands of instances of Frama-C, minimizing startup time is essential to improve the speed of the script. Therefore, we recommend to the user (when this is not the case) that option -no-autoload-plugins, followed by -load-module <plugins required for the bug>, be included in the command line. We also recommend using preprocessed (.i) files when possible, both to accelerate Frama-C and to avoid that #include directives prevent the script from being reduced. The user can of course keep them if desired.

Conclusion

We expect industrial users to be able to speed their reporting by using C-Reduce with as little effort as possible. C-Reduce is already used by the Frama-C team and saved us a considerable amount of time. We thank John Regehr and his team for the work on it, and we expect Frama-C users will benefit from it as well.