This new series is dedicated to the verification of the C version of Open Source compression library QuickLZ version 1.5.0 using Frama-C's Value Analysis. The source code can be downloaded from the web site.

QuickLZ offers compression and decompression routines using the Lempel-Ziv (LZ) algorithm. Various options are provided at compile-time. One noteworthy setting is the QLZ_MEMORY_SAFE compilation mode; this option guarantees that the decompression routine will terminate safely if fed corrupted data, without illegal memory accesses.

In this post we focus on the analysis of the decompression routines using QLZ_COMPRESSION_LEVEL == 1 with the option QLZ_MEMORY_SAFE enabled.

Analysis Context

The QLZ_MEMORY_SAFE guarantee is interesting to verify formally, and a good fit for the value analysis. Still, with the Skein tutorial under our belt, we do not expect to immediately get this kind of general result. Let us start with the decompression of a 20-char compressed buffer inside a 40-char destination buffer. If we succeed at verifying that, we can come back to these choices and see what is needed to make the verification more general.

We need to define a variable state_decompress, used by the library for temporary storage during decompression:

#include "quicklz.h"

qlz_state_decompress state_decompress;

We define the destination array as a global variable. This means the value analysis assumes it is initialized to zero. If we succeed, we may later improve the verification by using an uninitialized local array for the destination buffer. If we are able to analyze that program without alarms, it will confirm that the decompression routine does not use any contents of the destination buffer it has not already written there, which will be another interesting property. For now, let us concentrate on memory safety:

unsigned char file_data[20];
unsigned char decompressed[40];

The program we write for the purpose of this analysis fills file_data with arbitrary contents by calling an unknown function u(). Then, the decompression function qlz_decompress() reads from file_data, decompresses using state_decompress and writes the decompressed data to array decompressed, returning the decompressed size:

int main(int argc, char* argv[])
{
  size_t d;
  int i;

  for (i=0; i<20; i++)
    file_data[i] = u();

  d = qlz_decompress(file_data, decompressed, &state_decompress);

  return 0;
}

Get the files: decompress.c, quicklz.c, quicklz.h.

The QuickLZ library calls in two places the function memcpy() which is expected to be in a system library. A list of missing functions can be printed with the command:

$ frama-c -metrics quicklz.c
...
Undefined functions (1):
  memcpy  (2 calls); 
...

The value analysis needs source code to work accurately. As explained in the Frama-C Value Analysis manual the best way to handle missing functions like memset() or memcpy() is to provide source code for them. In the same fashion as in the analysis of the Skein library we provide our own implementation of memcpy() and place it in a file libc.c with the other source files.

Step by Step Analysis

We first launch an imprecise analysis:

$ frama-c -val decompress.c quicklz.c libc.c > log

$ grep assert log
quicklz.c:209:[kernel] warning: out of bounds read. assert \valid(src);
quicklz.c:668:[kernel] warning: pointer comparison: assert \pointer_comparable(offset2, (dst-2)-1);
quicklz.c:209:[kernel] warning: out of bounds write. assert \valid(dst);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+3);
quicklz.c:112:[kernel] warning: out of bounds read. assert \valid(p);
quicklz.c:110:[kernel] warning: out of bounds read. assert \valid(p);
quicklz.c:110:[kernel] warning: out of bounds read. assert \valid(p+1);
quicklz.c:108:[kernel] warning: out of bounds read. assert \valid(p);
quicklz.c:108:[kernel] warning: out of bounds read. assert \valid(p+1);
quicklz.c:108:[kernel] warning: out of bounds read. assert \valid(p+2);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+1);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+2);
quicklz.c:607:[kernel] warning: out of bounds read. assert \valid(src+2);
quicklz.c:713:[kernel] warning: out of bounds read. assert \valid(src);
quicklz.c:713:[kernel] warning: out of bounds write. assert \valid(dst);
libc.c:9:[kernel] warning: out of bounds read. assert \valid(tmp_0);
libc.c:9:[kernel] warning: out of bounds write. assert \valid(tmp);

18 alarms are emitted. As there are large arrays used in the source code, we try to improve this result by passing a very large argument to the -slevel option.

$ frama-c -val decompress.c quicklz.c libc.c -slevel 6000 > log

$ grep assert log
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+3);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+1);
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+2);
quicklz.c:209:[kernel] warning: out of bounds read. assert \valid(src);
quicklz.c:607:[kernel] warning: out of bounds read. assert \valid(src+2);
quicklz.c:209:[kernel] warning: out of bounds write. assert \valid(dst);
quicklz.c:108:[kernel] warning: out of bounds read. assert \valid(p+2);
quicklz.c:108:[kernel] warning: out of bounds read. assert \valid(p+1);
quicklz.c:108:[kernel] warning: out of bounds read. assert \valid(p);
quicklz.c:713:[kernel] warning: out of bounds read. assert \valid(src);
quicklz.c:713:[kernel] warning: out of bounds write. assert \valid(dst);
libc.c:9:[kernel] warning: out of bounds read. assert \valid(tmp_0);
libc.c:9:[kernel] warning: out of bounds write. assert \valid(tmp);

The analyzer still emits 14 alarms. We now try to eliminate these. The process is a routine of picking an alarm, investigating where it comes from, displaying values of variables to comprehend the situation, in order to eventually resolve it by helping the analyzer.

Let us have a look at the first alarm:

[value] computing for function fast_read <-qlz_decompress_core <-qlz_decompress <-main.
        Called from quicklz.c:578.
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+3);

We have a look at line 106 in the source code. It refers to the access to p+3 in case 4 of the switch construct in the function fast_read().

static __inline ui32 fast_read(void const *src, ui32 bytes)
{
...
  unsigned char *p = (unsigned char*)src;
  switch (bytes)
  {
    case 4:
      return(*p | *(p + 1) << 8 | *(p + 2) << 16 | *(p + 3) << 24);
    case 3: 
      return(*p | *(p + 1) << 8 | *(p + 2) << 16);
    case 2:
      return(*p | *(p + 1) << 8);
    case 1: 
      return(*p);
  }
...
}

fast_read() is unlikely to be at fault here. Instead, if there is a bug, it is likely to be in fast_read()'s caller, and if this is a false alarm, the imprecision again is to be found in the analysis of fast_read()'s caller.

The log indicates that fast_read() was called from line 578 when the alarm appeared. Going to line 578, we indeed find the function call:

  cword_val = fast_read(src, CWORD_LEN);

CWORD_LEN is defined to be 4 at the top of the quicklz.c file. Here we want to inspect the values of variable src. Therefore, we insert a call to a Frama_C_show_each...() function immediately before the call to fast_read():

  Frama_C_show_each_src_at_beginning(src);
  cword_val = fast_read(src, CWORD_LEN);

Regarding the time taken by the analysis: the analyzer may need some time to finish the analysis, especially when unrolling with very large arguments or when the analyzer is made to inspect a large number of cases separately. You do not have to wait for the end of the analysis to look at the log file. We decided to start with the first alarms. Inserting assertions or logging functions Frama_C_show_each...() to get more information, we expect the corresponding output to appear early in the log, even while the analysis is still running.

Although only logging some values with a Frama_C_show_each...() function does not change what the program does, it may change a bit the order in which values are propagated, so we get a different first alarm this time. The new first alarm is still very close to the previous one, and obviously related: it takes place in the same function, at the same line, but for the next call to this function in the caller, a few lines below. Let us study this new alarm as if it was the one we were after from the beginning. The log says:

[value] Called Frama_C_show_each_src_at_beginning({{ &file_data + [7..17] ;}})
[value] computing for function fast_read <-qlz_decompress_core <-qlz_decompress <-main.
        Called from quicklz.c:588.
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+3);

This time, the alarm refers to a call to fast_read() a few lines below, at 588:

  fetch = fast_read(src, 4);

Inspecting the output, we can see that src may be in the range {{&file_data + [7..17];}}. As file_data is an array of size 20, it is indeed illegal to read 4 bytes starting from {{&file_data + 17}}. When compiling with the QLZ_MEMORY_SAFE option, we expect this to be prevented by the safety test above. Again, we display the values of src and last_source_byte in the beginning of the QLZ_MEMORY_SAFE block to obtain more information.

#ifdef QLZ_MEMORY_SAFE
  Frama_C_show_each_src_last(src, last_source_byte);
  if(src + CWORD_LEN - 1 > last_source_byte)
    return 0;
#endif

The corresponding output looks like this:

[value] Called Frama_C_show_each_src_last({{ &file_data + [7..17] ;}},
                                          {{ &file_data + [10..4294967294] ;}}))

The pointer last_source_byte seems to possibly contain very large offsets of file_data. We inspect the source to determine where these come from. The last assignment to this pointer can be found within this function a few lines above.

last_source_byte = source + qlz_size_compressed((const char *)source) - 1;

It is the address of the last element in the compressed array. The auxiliary function qlz_size_compressed() is called to determine the size of the compressed array. Studying function qlz_size_compressed(), we find that the information is read from the header of the compressed array. Specifically, the compressed size is read from either 1 or 4 bytes, starting at the second byte in the source array. This explains why the last_source_byte values are so imprecise. As the source array is filled with arbitrary values, the header is filled arbitrarily as well. But in the analysis context, we set the size for our compressed array to be 20. To be consistent, let us make sure the analysis uses the same size by placing an assertion within function qlz_size_compressed().

size_t qlz_size_compressed(const char *source)
{
  ui32 n, r;
  n = (((*source) & 2) == 2) ? 4 : 1;
  r = fast_read(source + 1, n);
  r = r & (0xffffffff >> ((4 - n)*8));
  //@ assert r == 20;
  return r;
}

Once the analysis is launched again, the log near the first alarm looks like:

[value] Called Frama_C_show_each_src_last({{ &file_data + [7..17] ;}},
                                          {{ &file_data + {19; } ;}})
[value] computing for function fast_read <-qlz_decompress_core <-qlz_decompress <-main. 
        Called from quicklz.c:590.
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+3);
[value] Called Frama_C_show_each_src_at_beginning({{ &file_data + [7..17] ;}})

Thinking about it for ourselves, the condition src + 4 - 1 > last_source_byte is true if src is {{&file_data + 17}} and it is false when src is in {{&file_data + [7..16]}}. Still, the output of Frama_C_show_each_src_at_beginning() claims that src might be {{&file_data + [7..17]}}.

Obviously, the analyzer is not taking full advantage of the available information, although in this case the reduced value for src would be representable. This is because computing the values that make the condition false amounts to solving an equation. The analyzer cannot expect to solve all possible equations (The C language allows to write some fiendishly difficult quadratic ones). It could be expected to solve this one, but obviously, it doesn't. We could report this issue as a feature wish, but no one ever listens.

Determining which subsets of values for src make the condition true or false is a difficult problem, but finding out that the condition is true or false for user-provided subsets is easier. Let's help the analyzer by adding an assertion that divides src's values into those that respectively lead to a true condition and to a false one, that is, {{&file_data + 17}} and {{&file_data + [7..16]}}. Note that simple interval arithmetics allow to see that in the first case, src + 4 - 1 > last_source_byte is true, and that in the second case, it is false for all values of src. The analyzer, once told to separate these subsets of value, naturally propagates only the latter after the if.


Note that we place our annotations before the problematic call to fast_read() and that we do not try to make assumptions within function fast_read() itself in line 106 where the alarm occurs. Intuitively, this is a way of saying that the problem (or imprecision) is not with fast_read but with its caller. It is a matter of placing the annotation in just the right place, as in this previous example.

Or, looking at this situation from another angle, the function fast_read() is called nine times in the library. Placing an assertion inside the function means the assertion applies for every function call. If placed before the function call it only applies to this specific call. An assertion to help the analyzer which might be valid for one call may be false for another call to the same function.


#ifdef QLZ_MEMORY_SAFE
  //@ assert src <= source + 16 || src > source + 16;
  if(src + 4 - 1 > last_source_byte)
    return 0;
#endif

After adding this assertion and analyzing again, the output is slightly different.

        Called from quicklz.c:581.
quicklz.c:106:[kernel] warning: out of bounds read. assert \valid(p+3);

The same problem re-appears in line 581 which contains the first call to fast_read. It is normal to see this alarm come back to first position now that we have eliminated its close competitor. In the safety test above line 581, we find the same precision issue we just handled. We again divide the state into values that make the condition true and values that make it false, in order to circumvent the analyzer's limitations.

#ifdef QLZ_MEMORY_SAFE
  Frama_C_show_each_src_last(src, last_source_byte);
  //@ assert src <= source + 16 || src > source + 16;
  if(src + CWORD_LEN - 1 > last_source_byte)
    return 0;
#endif

Launching Frama-C again, we discover that the alarm has disappeared thanks to the hint we provided. Some alarms remain. Let us have a look at the next one.

[value] computing for function memcpy_up <-qlz_decompress_core <-qlz_decompress <-main.
        Called from quicklz.c:680.
quicklz.c:210:[kernel] warning: out of bounds write. assert \valid(dst);

We inspect line 210 in the function memcpy_up().

static __inline void memcpy_up(unsigned char *dst, const unsigned char *src, ui32 n)
{
...
  unsigned char *end = dst + n;
  while(dst < end)
  {
    *dst = *src;
    dst++;
    src++;
  }
...
}

The analyzer warns us of a possible out of bounds write in *dst = *src;. The pointer dst is passed to the function as an argument. Guided by the log, we find the function call at line 680. Again, we start by displaying the values before the function call to understand where the problem comes from.

  Frama_C_show_each_memcpy(dst, offset2, matchlen);
  memcpy_up(dst, offset2, matchlen);

The result is:

[value] Called Frama_C_show_each_memcpy({{ &decompressed + {3; 4; } ;}},
                                        {{ &decompressed + {0; 1; } ;}},[0..255])
[value] Called Frama_C_show_each_src_last({{ &file_data + [7..20] ;}},
                                          {{ &file_data + {19; } ;}})
[value] computing for function memcpy_up <-qlz_decompress_core <-qlz_decompress <-main.
        Called from quicklz.c:680.
quicklz.c:210:[kernel] warning: out of bounds write. assert \valid(dst);

Seeing the #ifdef QLZ_MEMORY_SAFE guard above the call, and inserting some more Frama_C_show_each...() calls, we find that the first issue is that last_destination_byte is imprecise. It seems the problem is that the input buffer having been filled arbitrarily, a nondeterministic value is read from the header to use as the decompressed size. In our analysis context, we set the size of the decompressed array to 40. Remember that earlier, we have assumed that the compressed size indicated by the header was 20. We should write another assertion that similarly sets the decompressed size to be the same as in the analysis context.

size_t qlz_size_decompressed(const char *source)
{
	ui32 n, r;
	n = (((*source) & 2) == 2) ? 4 : 1;
	r = fast_read(source + 1 + n, n);
	r = r & (0xffffffff >> ((4 - n)*8));
    //@ assert r == 40;
	return r;
}

Next:

[value] Called Frama_C_show_each_memcpy({{ &decompressed + [0..8] ;}},
                                        {{ &decompressed + {0; 1; 2; 3; 4; 5; } ;}},
                                        [0..36])
[value] Called Frama_C_show_each_src_last({{ &file_data + [7..20] ;}},
                                          {{ &file_data + {19; } ;}})
[value] computing for function memcpy_up <-qlz_decompress_core <-qlz_decompress <-main.
        Called from quicklz.c:681.
quicklz.c:211:[kernel] warning: out of bounds write. assert \valid(dst);
quicklz.c:211:[kernel] warning: out of bounds read. assert \valid(src);

The output has changed slightly, but the value analysis is still emitting alarms. Assuming the decompressed array is of size 40, we can safely write or read &decompressed + 39. The result of Frama_C_show_each_memcpy() states that at the point we are considering, up to 36 bytes might be read from &decompressed + 5 and might be written to &decompressed + 8 to just mention one example. This would be indeed out of bounds.

We assume this to be a false alarm, because there should not be any illegal memory access in the QLZ_MEMORY_SAFE mode. Let us have a look at the QLZ_MEMORY_SAFE block just above the problematic call to memcpy_up and obtain more information about the values. MINOFFSET is defined to be 2 and UNCOMPRESSED is defined to be 4 in quicklz.c.

#ifdef QLZ_MEMORY_SAFE
  Frama_C_show_each_all(offset2, history, dst, matchlen);
  if(offset2 < history || offset2 > dst - MINOFFSET - 1)
    return 0;
  Frama_C_show_each_bound(matchlen, last_destination_byte, dst, (last_destination_byte - dst - 4 + 1));
  if(matchlen > (ui32)(last_destination_byte - dst - UNCOMPRESSED_END + 1))
    return 0;
#endif

We search the log for the last calls to Frama_C_show_each_all() and Frama_C_show_each_bound() before the alarm occurs and get this result:

[value] Called Frama_C_show_each_all({{ &NULL ; &decompressed + {0; 1; 2; 3; 4; 5; } ;}},
                                     {{ &decompressed ;}},
                                     {{ &decompressed + [0..8] ;}},[0..255])
[value] Called Frama_C_show_each_bound([0..255],{{ &decompressed + {39; } ;}},
                                       {{ &decompressed + [0..8] ;}},[28..36])

For the sake of memory safety, the QLZ_MEMORY_SAFE block has to make sure nothing bad happens. The suspicion here is that by abstract interpretation the possible values of dst, offset2 and matchlen are summarized in such a way that at the call to memcpy_up, combinations of values are considered to be possible that actually are not. We help the analyzer by providing the hint that each value of dst should be considered separately. For each single value of dst, the analysis can then compute the precise values of offset2 (and matchlen) that are eliminated by the safety test if(offset2 < history || offset2 > dst - MINOFFSET - 1) return 0; (and the other test).

#ifdef QLZ_MEMORY_SAFE
  Frama_C_show_each_all(offset2, history, dst, matchlen);
  /*@ assert 
    dst == decompressed      || dst == decompressed + 1  ||
	dst == decompressed + 2  || dst == decompressed + 3  ||
	dst == decompressed + 4  || dst == decompressed + 5  ||
	dst == decompressed + 6  || dst == decompressed + 7  ||
	dst == decompressed + 8  || dst == decompressed + 9  ||
	dst == decompressed + 10 || dst == decompressed + 11 ||
	dst == decompressed + 12 || dst == decompressed + 13 ||
	dst == decompressed + 14 || dst == decompressed + 15 ||
	dst == decompressed + 16 || dst == decompressed + 17 ||
	dst == decompressed + 18 || dst == decompressed + 19 ||
	dst == decompressed + 20 || dst == decompressed + 21 ||
	dst == decompressed + 22 || dst == decompressed + 23 ||
	dst == decompressed + 24 || dst == decompressed + 25 ||
	dst == decompressed + 26 || dst == decompressed + 27 ||
	dst == decompressed + 28 || dst == decompressed + 29 ||
	dst == decompressed + 30 || dst == decompressed + 31 ||
	dst == decompressed + 32 || dst == decompressed + 33 ||
	dst == decompressed + 34 || dst == decompressed + 35 ||
	dst == decompressed + 36 || dst == decompressed + 37 ||
	dst == decompressed + 38 || dst == decompressed + 39;  */ 
  if(offset2 < history || offset2 > dst - MINOFFSET - 1)
    return 0;
  Frama_C_show_each_bound(matchlen, last_destination_byte, dst, (last_destination_byte - dst - 4 + 1));		
  if(matchlen > (ui32)(last_destination_byte - dst - UNCOMPRESSED_END + 1))
    return 0;
#endif

Running the analysis again, only the following two alarms remain:

[value] computing for function memcpy <-qlz_decompress <-main.
        Called from quicklz.c:854.
libc.c:9:[kernel] warning: using size of 'void'
libc.c:9:[kernel] warning: out of bounds read. assert \valid(tmp_0);
libc.c:9:[kernel] warning: out of bounds write. assert \valid(tmp);

Tackling the last alarms

In line 854 the function memcpy() is called from inside function qlz_decompress().

size_t dsiz = qlz_size_decompressed(source);
...
  if((*source & 1) == 1)
    {
      reset_table_decompress(state);
      dsiz = qlz_decompress_core((const unsigned char *)source, (unsigned char *)destination, dsiz, state, (const unsigned char *)destination);
    }
    else
    {
      Frama_C_show_each_dsiz(destination, source, qlz_size_header(source), dsiz);
      memcpy(destination, source + qlz_size_header(source), dsiz);
    }

The condition if((*source & 1) == 1) checks if the last bit of the first header byte of the compressed data equals 1. By doing some research in the source code we find this bit indicates whether the data was compressible or if it was copied verbatim. If compression was used, the bit contains the value 1. If not, the bit's value is 0. In the then-branch (when the data is indeed compressed by the algorithm), the reverse decompression algorithm is applied. In the else-branch, knowing that the incompressible data was copied verbatim at compress-time, the data from the source buffer is copied to the decompressed array, omitting the header. In this case, the compressed array is supposed to be exactly of the size of the decompressed header plus the size of the header. Let us display the possible values at this point.

[value] Called Frama_C_show_each_dsiz({{ &decompressed ;}},{{ &file_data ;}},
                                      {3; 9; },{40; })

The decompressed size dsiz is read from the header by the function qlz_size_decompressed() and then passed to memcpy(). We forced this size to be 40, so this is what the analyzer prints for dsiz. In this call to memcpy(), 40 bytes will be read starting from either &file_data + 3 or &file_data + 9. But as we fixed the compressed size to 20 there definitely will be an illegal access.

The problem is that this program point can be reached with a corrupted header. Since the source and destination buffers can be assumed to have been allocated with sizes read from the header, when copying the entire contents from one to the other, there should be a guard that checks the compressed size to be equal to the decompressed size plus the size of the header

This bug was reported and is fixed in version 1.5.1 beta of QuickLZ. The fix consists in adding the guard below before the call to memcpy().

if(qlz_size_compressed(source) != qlz_size_decompressed(source) + qlz_size_header(source))
   return 0;

Verification is not finished.

There were several assumptions made during verification: we were checking only QLZ_COMPRESSION_LEVEL 1 and assumed that the compressed and decompressed sizes were fixed in order to help the analyzer. Additionally, the decompressed array is defined globally and therefore initialized before the first use, which represents a weaker property than using an uninitialized local declaration for the analysis.

The manually added assertions are shown to be valid by the analyzer, except for the two assertions that define the compressed and decompressed sizes.

quicklz.c:185:[value] Assertion got status unknown.
quicklz.c:195:[value] Assertion got status unknown.
quicklz.c:580:[value] Assertion got status valid.
quicklz.c:590:[value] Assertion got status valid.
quicklz.c:677:[value] Assertion got status valid.

After investigating the decompression routines, this call to memcpy() contained the last remaining alarms. This means that under the assumptions we made so far, the decompression routines are safe from any other undefined behavior. The next step, now that we have established a base camp, is to remove as many assumptions are possible to get the most general verification result.

Incidentally, once the fix is applied, no alarms at all are emitted, because with our assumptions, the safety test causes the library to return before the memcpy(). This shows the necessity, at the very least, to verify the library using other values for compressed and decompressed sizes.

This post is co-authored by Kerstin Hartig and benefited of suggestions from Lasse Reinhold. Apologies to any reader confused by Douglas Adams references.

Note: this work was done with the development version of the value analysis at the time. Recent released versions of Frama-C detect another, innocuous issue where an uninitialized variable is used in order to silence compiler warnings: { int i; i;…. In order to replay the analysis with such a recent version, the uninitialized access to i should be removed.