Frama C EVA undefined behavior

Question

I tried to analyse a code that I found on the JULIET test directory, from the sate6 reproduction, dealing with the CWE758. For many of them, the tool does not detect the error. The results are unsound, but in the results summary of the Sate, it is marked as "ok" because it detects an alarm but not the one it should. You can try with the code at this address : https://samate.nist.gov/SARD/test-cases/241267/versions/2.0.0 The parameters are the one fixed during the sate :

FCFLAGS="-no-autoload-plugins -load-module from,inout,report,eva,variadic -kernel-warn-key parser:decimal-float=inactive -kernel-warn-key typing:no-proto=inactive -kernel-warn-key typing:implicit-conv-void-ptr=inactive -eva-warn-key locals-escaping=inactive -add-symbolic-path $TESTCASESUPPORT_DIR:TESTCASESUPPORT_DIR

EVAFLAGS="\
  -eva-msg-key=-initial-state,-final-states \
  -eva-no-show-progress \
  -eva-print-callstacks \
  -eva-slevel 300 \
  -warn-special-float none \
  -warn-signed-downcast \
  -warn-unsigned-overflow \
  -eva-warn-copy-indeterminate=-@all \
  -eva-no-remove-redundant-alarms \
  -eva-domains equality,sign \
"

Could you provide me the settings that help detecting the error ? Or is the tool not able to detect it ?

user_1173674 · Answer

Before answering, a quick note: the Github link you included points to an archived version of the Juliet 1.3 test cases; a more up-to-date version is available in Frama-C's Gitlab repository. For the test case you mention, however, there is no difference.

In the README.md file (present in both repositories), there are some details concerning soundness claims:

Note that, except for a few syntactic CWEs, the origin of the CWE may not be located at the point in which the program behavior becomes undefined. Thus Frama-C/Eva cannot automatically locate the origin of the issue, just its "symptoms". The precise identification of the location requires some inspection work (using the Frama-C GUI) to navigate to the program point ultimately responsible for the weakness.

So, your claim that "it detects an alarm but not the one it should" can be interpreted in different ways, for instance:

Frama-C/Eva emits an alarm that is completely unrelated to the bug in the code;
Frama-C/Eva emits an alarm that is a consequence of the bug in the code.

I'd argue that Frama-C/Eva is in the latter case: although the reported alarms do not match the line of code where SARD considers the error to be present, the alarm reported by Eva is still related to that line, and a direct consequence of it (a simple way to test is to remove the statement and see if Eva still reports something; if it does not, then the alarm was a consequence of the removed statement). Here's what the graphical interface shows when running that example:

The assignment data = *pointer does not lead to an alarm for Frama-C/Eva for technical reasons, in the case of structs. One of the reasons is the possible presence of padding bits: when a struct is copied, padding bits (which always contain indeterminate values) are also copied; if an alarm were emitted due to those bits, then struct copies would lead to alarms even in legitimate cases.

However, in practice, such copied values are bound to be read by someone later (as is the case in Juliet's tests), and at that moment, Frama-C/Eva will emit an alarm. Here's the relevant excerpt from the Eva user manual:

[In section Uninitialized variables and dangling pointers to local variables]:

However, it may be normal for some fields in a struct or union to contain such dangerous contents in some cases. Thus, Eva never emits an alarm for a copy from memory to memory of a struct or an union containing dangling addresses or uninitialized contents. This behavior is safe because Eva warns later, as soon as an unsafe value is used in a computation - either directly or after having been copied from another location.

Overall, it would be better for users if the detection happened earlier, and it will possibly be the case someday, but for now, the caveat related to correctness claims is necessary to take into account such cases.

Therefore, to conclude:

Frama-C/Eva does not (at least currently) report the "struct copy with indeterminate values" as an alarm, and there are no settings to change it (a related option is -eva-warn-copy-indeterminate, which is set by default; it allows disabling such alarms in other situations);
The definition of "an alarm but not the one it should" is not straightforward, since the reported alarm is still a direct consequence of the bug introduced in the test case. It is true that the line location is not the same, but this is also the case for other kinds of bugs, when their cause and perceived effects are separated. To remediate it, Frama-C offers many result inspection features (mainly via the GUI) to allow users to profoundly understand what happens and whether the issue is important to them or not.
CWE-758 is too broad to be considered completely handled by any tool.

As a final remark, I copy here the caveat present in the README.md file of the Frama-C SATE 6 repository, especially in relation to CWE-758:

CWE758 - Undefined Behavior is extremely vague and could, in theory, include examples which lead to any of the ~200 undefined behaviors listed in Annex J.2 of the ISO/IEC 9899:1999 standard. It is therefore impossible to guarantee that every program which contains a CWE758-type vulnerability will be reported by Eva. Currently, however, we can state that, for all test cases in the Juliet 1.3 C/C++ set, for the CWEs mentioned as handled by Frama-C/Eva, the analysis reports one or several issues for each test case marked as bad.

Unfortunately the reported issue is not always exactly the one indicated in SARD, but to our knowledge, they are at least related (i.e., no spurious alarm emitted due to an unrelated pattern in the code) to the flaws indicated in SARD. Hopefully more precise claims will be doable in the future, to improve user experience and analysis precision.

Frama C EVA undefined behavior

1 Answers