This is the submission corresponding to Frama-C's value analysis for SATE V. We wish to participate in the “Ockham Sound Analysis Criteria”.

After defining “finding” as a “definitive report about a site”, the webpage states:

“Sound means every finding is correct.”

Frama-C's value analysis is able to guarantee the absence of some weaknesses. That is, it can guarantee that a “site”, as defined by the webpage, is never reached through a defined execution starting from the program's entry point with values that cause the weakness to occur.

For this reason, in order to accommodate the above definition of “soundness”, the findings of Frama-C's value analysis should be taken as all sites in the C testcases in the listed subdirectories of synthetic/ for which no warning was emitted:

CWE121_Stack_Based_Buffer_Overflow  CWE190_Integer_Overflow
CWE122_Heap_Based_Buffer_Overflow   CWE191_Integer_Underflow
CWE123_Write_What_Where_Condition   CWE369_Divide_by_Zero
CWE124_Buffer_Underwrite            CWE457_Use_of_Uninitialized_Variable
CWE126_Buffer_Overread              CWE476_NULL_Pointer_Dereference
CWE127_Buffer_Underread             CWE562_Return_of_Stack_Variable_Address

Frama-C's value analysis may emit “false alarms”. The presence in the log of a warning for a site does not guarantee that the weakness exists. But if a warning is not emitted, the site is definitely not a weakness (for the analysis parameters used including choice of entry point and of target architecture. The small print is Frama-C's value analysis manual).

As previously discussed, in CWE190_Integer_Overflow and CWE191_Integer_Underflow, only the undefined overflows (signed arithmetic overflows involving types of width at least "int") are identified. A site where a defined or implementation-defined overflow occurs is not listed, but the correct (“wrapped-around”) value is propagated.

As suggested by Aurélien in answer to our question M/, we used two different configurations, one in which allocation functions always succeed and one in which the possibility of malloc() or realloc() returning NULL is modeled. This lead to two different XML reports.

The Juliet testcases use library functions. The meaning of these functions is defined in Frama-C though code and/or specifications. When the weakness occurs in the code of such a library function, I took the liberty of localizing the weakness at the call site inside Juliet. 
For instance, consider the following report:

<weakness id="2958">
<name>invalid memory access</name>
<location path="synthetic/testcases/CWE126_Buffer_Overread/s02/CWE126_Buffer_Overread__malloc_wchar_t_loop_03.c" line="70">
</location>
<grade severity="4"/>
<output><textoutput><![CDATA[../ppc/share/libc/wchar.c:32:[kernel] warning: out 
of bounds write. assert \valid(tmp);
                  stack: wmemset :: testcases/CWE126_Buffer_Overread/s02/CWE126_Buffer_Overread__malloc_wchar_t_loop_03.c:70 <-
                         goodG2B1 :: testcases/CWE126_Buffer_Overread/s02/CWE126_Buffer_Overread__malloc_wchar_t_loop_03.c:123 <-
                         CWE126_Buffer_Overread__malloc_wchar_t_loop_03_good
]]></textoutput></output></weakness>

The actual error is at line 32 of our file wchar.c, that provides an implementation for wmemset(). But for convenience, the location path is set as line 70 of the testcase that causes the illegal memory access.

In any case, each report usually contains a call stack of form:

function1 :: file:line at which function1 is called inside function2 <-
function2 :: file:line at which function2 is called inside function3 <-
...
entry point

These call stacks are only hints for understanding how the weakness can occur. Even if the user confirms a weakness does not to happen for the particular call stack in the log, it does not mean that the analyzer did not identify the same weakness for another call stack. When this happens, the weakness is mentioned only once in the log (which is long enough as it is). The liberty I took with the localization of weaknesses could theoretically be a problem with respect with the “hint” status of call stacks, e.g. if the same weakness inside wmemset() can be activated from several call sites inside the same Juliet testcase. Still, I anticipate that the choice I made will save more time than it wastes.

Each XML report was produced by processing Frama-C log files generated as files X_good and X_bad for each testcase X*.c.
In the original log files, an alarm is identified as either a pre-condition for a library function that could not be established (status unknown or invalid) or invalid arguments to an operator, causing an assertion (the message contains the keyword “assert”). Even for conditions that do not fit well in our specification language, we try to use the word “assert” somewhere in each message that should be taken seriously. For instance, when the arguments of a printf() call are suspicious, the message may be:

assert(match format and arguments)

Most of the times, the contents of an assertion are an actual logical formula describing the condition that should hold for the execution to continue. For instance, when the program divides by variable data and the analyzer cannot rule out the possibility that data contains zero, the assertion is:

assert data ≢ 0;

Some pre-conditions with status “unknown” are voluntarily omitted from by the processing scripts. We think that this does not constitute “filtering” as intended in http://samate.nist.gov/SATE5OckhamCriteria.html :

“No automated filtering specialized to a test case or to SATE is allowed”

The pre-conditions that are filtered are pre-conditions that Frama-C's value analysis can *never* validate because they are currently outside its scope. The annotations are written in a specification language, ACSL, that is intended to be as general as possible. Other Frama-C plug-ins with different abilities use ACSL, thus it does not make sense to limit the language to what the value analysis plug-in supports.

Similarly, it does not make sense either to write only partial specifications for library functions. The specification for function strcpy() in the Frama-C headers is:

/*@ requires valid_string_src: valid_string(src);
  @ requires room_string: \valid(dest+(0..strlen(src)));
  @ assigns dest[0..strlen(src)] \from src[0..strlen(src)];
  @ assigns \result \from dest;
  @ ensures strcmp(dest,src) == 0;
  @ ensures \result == dest;
  @*/
extern char *strcpy(char *restrict dest, const char *restrict src);

This specification uses logical predicates valid_string, strlen and strcmp. These predicates are defined axiomatically, and this is why the value analysis plug-in cannot take advantage of them.

The first pre-condition valid_string(src) expresses the expectation that a terminating zero must be found when reading from src before the memory access becomes invalid. The value analysis is unable to interpret this axiomatic definition, but this does not matter: an invalid memory access before the terminating zero can be detected by interpreting the implementation of strcpy().

The second pre-condition \valid(dest+(0..strlen(src))) expresses that there is room at the destination to copy the entire string. Again, the value analysis cannot take advantage of this axiomatic specification but it can detect an invalid write in the implementation of strcpy().

The presence of these pre-conditions that the value analysis plug-in cannot validate is unfortunate, but there is still hope that the plug-in will one day support the logical predicates these pre-conditions involve. Meanwhile, other Frama-C plug-ins need these specifications for the deductive verification of the target programs. 

The XML reports are attached. They can also be found in CEA's SWAMP virtual machine, in /home/cea . The complete logs are also available there, as logs.*.tar.bz2

MD5 (frama_c_report.allocfail.xml.bz2) = 39b87adceaaa471f4f67d612a7ba6b12
MD5 (frama_c_report.succalloc.xml.bz2) = 85a8811cbdddef7870de5e564ddd0603

I am unsure whether the next step is for me to upload to SWAMP the Frama-C development version with proprietary extensions that was used to participate and the scripts that were used to generate the XML reports. Is this necessary, and is there anything else I need to do?

Best regards,

Pascal
