Verifying the Compression Library QuickLZ
Pascal Cuoq - 5th Apr 2011This 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.