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 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
-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:
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:
Nonterm restores some of the information lost due to callstack consolidation. The highlighted warning in particular gives us the following information:
h5 -= c5 << 25does not 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.
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.
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
-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
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
u64 instead of
i64. Then, re-parse the sources, re-run the analysis, and keep iterating.
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.
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.André Maroneze