TIS-interpreter progress report

tis-interpreter is a specialized version of Frama-C for interpreting C programs and finding bugs in them. The development of tis-interpreter started from Frama-C’s Value Analysis plug-in, and discarded the possibility of analyzing the behaviors of the program for all inputs. Instead, tis-interpreter monitors the program’s behavior for one input at a time. In exchange for giving up on generality, tis-interpreter gains on precision: it never emits false positives. tis-interpreter only warns about illegal operations—out of bounds memory accesses, uses of uninitialized memory, …—that actually happen in the target program for at least one input, namely, the input that was provided for execution.

Not having to deal with false positives is life-changing, to a point that the reader may perhaps only fully apprehend if they have previously used Frama-C’s value analysis or a similar system. It is liberating: suddenly, the size of, the difficulties in the target codebase are no longer the user’s problem. One finds oneself wanting to tackle large, real programs. Programs that matter.

Which leads directly into the next limitation: real programs that matter use the standard library to access the environment, the time of day, and the filesystem. TrustInSoft had developed some of the foundations of the execution environment necessary to the analysis of real programs, and the Core Infrastructure Initiative is funding the development of the missing pieces of the puzzle and the release of the whole as Open-Source in 2016.

Until recently, progress was mostly of internal interest only. Now, development has reached a point where we are analyzing open-source library after library, and finding hitherto-unknown bugs in them. For this reason the latest progress report I sent to the CII may interest the reader of this blog, and I am republishing it here, lightly edited.

A- Improving the interpreter

 

Since the last quarter, John Regehr (who is visiting TrustInSoft on sabbatical), the TrustInSoft team and I have been implementing the detection of seemingly minor infringements to the C standard, such as calling a standard library function with an invalid pointer (say, NULL) together with a size of zero, or passing overlapping memory zones as arguments to standard functions that do not expect this. To illustrate the first family of issues, a C programmer might think that passing NULL together with a size of 0 is fine because the size of 0 means that no memory access will take place, but as of version 4.9, GCC started to use an obscure rule in the C standard for optimization purposes, and long story short, the BIND project was bitten when GCC 4.9 came out and BIND now has to be compiled with an explicit commandline option to disable this GCC behavior.

 

In the last quarter, progress on libotr and libgrypt had been stumped by the latter’s use of va_list to implement homegrown variadic functions in C, and I had promised to look at SQLite instead. It turned out that SQLite uses va_list too. As a consequence we got started on support for this construct, and va_list is now well-supported enough that we have reported our first bugs in SQLite, including some bugs in SQLite’s use of va_list (!)

 

Testing the interpreter on the implementation of webp, a modern, very computationally intensive image format, revealed an inefficiency that was creeping up as the interpretation was going on for a long time. This inefficiency is being fixed.

 

Finally, using the interpreter together with a file-based fuzzer such as afl meant that the file-access functions needed to be available in the interpreter too. The library of file-access functions has been systematically completed and tested with a dedicated file-access fuzzer.

 

These functions are written so as first to enable the execution of programs that use files, but not necessarily to detect all errors in the usage of file access functions. The easy-to-spot misuses of file-access functions are detected, and my hope is that, in the future, we will be able to harden the file-access functions to detect all wrong uses of them.

 

B- Applying the interpreter on existing tests

 

We took great advantage of pre-generated test suites that Michal Zalewski made available for download. Although these tests had already been executed either directly or under Valgrind/ASan/UBSan, executing them in tis-interpreter reveals additional subtle bugs that were reached by the test suites but were not recognized as bugs. As an example, we reported an erroneous pointer comparison in Google’s implementation of the webp image format. The pointer comparison usually behaves as intended, and behaved as intended when Michal generated and executed the testcase, but, depending on the memory layout, it can produce the wrong result and lead to an invalid pointer access further in the library.

 

The same pattern was present in other libraries: it turns out to be the foremost typical mistake that can remain in libraries that have already been closely inspected with previously available tools. So I wrote a short essay on this pattern and why it should be avoided.

 

Bugs were also reported against libpng, libjpg, OpenSSL, LibreSSL, libsodium, and SQLite.

 

We have started playing with afl ourselves and looking at ways to make it and tis-interpreter interact more closely.

tis-interpreter is not publicly available yet because we would rather find its more embarrassing bugs ourselves. The bugs can be quite puzzling, and could induce a trusting user to report as a bug in the target code what was a correct idiom and the symptom of a bug in tis-analyzer. No-one involved would gain from this happening.

Sometimes, bugs in tis-interpreter may confuse because of the unusual (for Frama-C) scale of the programs being tackled. Imagine that you were applying last month’s beta version of tis-interpreter to the following program:

#include 

… 11 823 lines of robust function definitions

int main(void) {

  … 5 367 lines of perfectly good code

  strlen(NULL);

  … 7 412 lines of harmless C

}

Last month’s tis-interpreter, because of a bug in the handling of the specific function call strlen(NULL), would only tell you that this program does not terminate, with absolutely no additional information. Previous experience with Frama-C’s Value Analysis might help you infer that it had found that something was wrong along the way and simply forgotten to say what, but even that in itself does not help identify either the strlen(NULL) bug in the target code or the strlen(NULL)-handling bug in tis-interpreter.

Needless to say, I omitted the resolution of this particularly shameful bug in the official progress report I sent the CII. This one can stay between us.