A simple Eva tutorial, part 3

In the previous post we’ve seen how to run Eva, but at the end we had a NON TERMINATING FUNCTION for a function that is supposed to always terminate, a likely indication that a definitive undefined behavior has been found in the analysis. In this post, we will see how to diagnose such cases, using derived plug-ins and the GUI.

We will reuse the save file produced at the end of the analysis, value2.sav.

When the GUI is not enough

Usually, after running the value analysis in the command-line, we launch the GUI to visualize the results:

frama-c-gui -load value2.sav

In this case, because of the NON TERMINATING FUNCTION message, we know that at some point in the program we will have red statements in the GUI, which indicate unreachable code.

By scrolling down from the main function, we reach the non-terminating statement, which is a call to test_x25519:

Note the red semicolon at the end of the statement, and the fact that the following statements are also red. If we click on the statement, the Information panel says that This call never terminates.

You can right-click on the function and Go to the definition of test_x25519, and you will find the same thing inside, this time a call to crypto_x25519_public_key, and so on, until you reach fe_tobytes, which is slightly different: it contains a for loop (defined via a macro FOR), after which all statements are red, but the loop itself is not an infinite loop: it simply iterates i from 0 to 5. How can this be non-terminating?

The answer, albeit non-intuitive, is simple: there is one statement inside the loop which is non-terminating, but not during the first iteration of the loop. Because the GUI colors are related to the consolidated result of all callstacks (i.e., if there is at least one path which reaches a statement, it is marked as reachable), it cannot show precisely which callstack led to the non-termination. To better understand what happens here, we will use the Nonterm plug-in.

Nonterm to the rescue

Nonterm is a small plug-in that uses the result of the value analysis to display callstack-wise information about non-terminating statements, by emitting warnings when such statements are found. It requires Eva to have been executed previously, but it runs very quickly itself, so you do not need to save its results. Close the GUI and re-run it again, this time with Nonterm:

frama-c-gui -load value2.sav -then -nonterm -nonterm-ignore exit

The -nonterm-ignore exit argument serves to minimize the number of warnings related to calls to the libc exit() function, which is always non-terminating.

The warnings generated by Nonterm are displayed in the Messages panel, after those emitted by Eva.

The warnings display the non-terminating callstacks. The order of the warnings themselves is not relevant. However, some kinds of warnings are more useful than others. Here is a rough indication of their relevance, from most to least precise:

1. Non-terminating statements;
2. Non-terminating loops;
3. Non-terminating function calls;
4. Unreachable returns.

In our analysis, the first (and only) warning about a non-terminating statement is the following:

Note a few important details about the Frama-C GUI:

• When you click on the warning in the Messages panel, the GUI focuses on the related statement.
• When a statement has associated annotations (here, two warnings), the focus is placed on the first annotation, instead of the statement itself. This does not imply that the annotation itself is related to this specific warning.
• The property status indicators (colored circles, or bullets on the left of each property) display the consolidated status of all callstacks; in particular, if the property is definitively valid in one callstack, but possibly/definitively invalid in another, the GUI displays a yellow bullet.

Nonterm restores some of the information lost due to callstack consolidation. The highlighted warning in particular gives us the following information:

1. There exists a stack trace in which statement h5 -= c5 << 25 does not terminate;
2. There is exactly one stack trace in which the statement never terminates; all other stack traces (which are not shown in the warning) terminate.

Currently, it is not possible to select a stack trace from the Messages panel, but we can do so using the Values panel. If we switch to it (keeping the statement highlighted in the source code), we can see that there are 40 different stack traces reaching this point.

Values Panel

The Values panel is arguably the most powerful inspection tool for the Eva plug-in in the Frama-C GUI. Some of its features were presented in earlier posts, but for the sake of completeness, here are some commented screenshots:

The values displayed in this panel are related to the green highlighted zone in the Cil source.

The Ctrl+E shortcut is equivalent to highlighting a statement, then right-clicking Evaluate ACSL term. The Ctrl+Shift+E shortcut is slightly more powerful: it also evaluates terms, such as \valid(p). This command is not available from any menus.

The Multiple selections checkbox allows adding several expressions to be compared side-by-side. When checked, highlighting an expression in the same statement adds a column with its value. Note that highlighting a different statement results in resetting all columns.

The three checkboxes to the right are seldom used: Expand rows simply expands all callstacks (but generates visual clutter); Consolidated value displays the row all (union of all callstacks); and Per callstack displays a row for each separate callstack.

The callstacks display has several contextual menus that can be accessed via right-clicks.

Let us start from the bottom: right-clicking on a callstack shows a popup menu that allows you to focus on a given callstack. This focus modifies the display in the Cil code viewer: reachability will only be displayed for the focused callstack(s). We will come back to that later.

Right-clicking on a cell containing a value allows filtering on all callstacks for which the expression has the same value. This is often used, for instance, to focus on all callstacks in which a predicate evaluates to invalid or unknown.

Finally, clicking on the column headers allows filtering columns.

Note that the Callstacks column header displays a pipette icon when a filter is being applied, to remind you that other callstacks exist.

Filtering non-terminating callstacks

In our code, despite the existence of 40 callstacks, only one of them is non-terminating. If you highlight the 0 ≤ c5 expression before statement h5 -= c5 << 25, you will see that only a single callstack displays invalid in the column 0 ≤ c5. Focus on this callstack using the popup menu, then highlight expression c5 in the Cil code. You will obtain the following:

As you can see, the GUI now displays the statements following h5 -= c5 << 25 in red, indicating thay they are unreachable in the currently focused callstacks. The exact value that caused this is shown in column c5: -1. The C standard considers the left-shift of a negative number as undefined behavior. Because -1 is the only possible value in this callstack, the reduction caused by the alarm leads to a post-state that is <BOTTOM>.

Proceeding with the analysis

To allow Eva to continue the analysis of the code, we need to modify it in some way. Since we are not experts in cryptography, we are unable to provide a definitive explanation why the code was written this way. In any case, it is not specific to Monocypher, but also present in TweetNaCl and ref10, two cryptographic libraries.

It is likely that replacing the signed carry variables in function fe_mul with unsigned ones would get rid of the undefined behavior, without changing the expected behavior of the code. However, without a more formal analysis performed by a cryptographer, this is just guesswork. Still, we need to do something to be able to continue the analysis (and possibly spot more undefined behaviors), such as changing the declarations of variables c0 to c9 to u64 instead of i64. Then, re-parse the sources, re-run the analysis, and keep iterating.

Ideas for complex situations

In the beta version of this post, we were using version 0.1 of Monocypher, which had a different version of functions related to fe_mul. In particular, some of the functions were taken from TweetNaCl, and the code was not unrolled the same way as in Monocypher 0.3. One of the consequences was that Nonterm was unable to show as clear a picture as in this case; it was necessary to perform syntactic loop unrolling (e.g., using loop pragma UNROLL) just to be able to clearly see in the GUI which statement was non-terminating.

Future developments in Frama-C and in the Eva plug-in will help identifying and visualizing such situations more easily.

Acknowledgments

We would like to thank loup-vaillant (Monocypher’s author) for the discussions concerning Monocypher and Eva’s analysis. New versions of Monocypher have been released since the analysis performed for this series of posts, which do not present the undefined behavior described in this post.