Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Tag - derived analysis

Entries feed - Comments feed

Tuesday, November 23 2010

Value analysis tutorial, part 5: jumping to conclusions

This post is in two parts, both of them independently good fits for the title, and still not completely without relation to each other, but that's probably a coincidence.

Methodology

In this thread, we aim at the verification of low-level properties for the functions in Skein. In the last post, I closed one line of reasoning as if the objective had been reached. But someone might object. "How do you know you can trust the verifier?", ey might say. "What have you really proved?". And, "are you asking me to believe that all cases are covered with separate analyses for 0, 1, even numbers greater than 2, and odd numbers greater than 3?".

Answers, in reverse order:

  1. yes. In C, you cannot call a function a negative number of times, so I am asking you to believe that this partition covers the "calling Update(...,80) an arbitrary number of times" part of the informal specification we settled on from the beginning.
  2. The middle question refers to the fact that there is a translation of sorts from the informal requirement or specification to the formal one. This is not unlike the translation in traditional verification from the informal requirement to executable test (or code review) plans. Yes, there are dangers here, but the dangers are not new. Both with testing or with more formal verification as we have been outlining, you can make unjustified assumptions, or forget a critical case. That weakness does not prevent replacing some tests and code reviews with formal methods, since all these techniques have the weakness. If anything, formal specifications that are slightly more expressive than individual test cases or review objectives are slightly closer to informal speech, and could be argued to have a slightly lower, and therefore slightly less risky, translation step.
  3. The first question is even less original than the middle one. We gain confidence in the verifier with tests and code reviews. They didn't suddenly stop working, you know.

Jumping ahead to the conclusion of the Skein-256 verification

All the techniques to deploy have not been exposed yet in this blog, but now that the thread gives a good idea of how absence of run-time errors can be verified in very general circumstances using the value analysis, I thought I would hint at the final results. One of the techniques to deploy is (as of November 2010) the next Frama-C release, which contains many optimizations and performance improvements, so there is no hurry for me to go into the details (yet).

Following roughly the same method, we have verified in-house that there wasn't any alarm when calling Skein_256_Update an arbitrary number of times between Skein_256_Init and Skein_256_Final, using for each call to Skein_256_Update a value n for the length, and an input buffer of length exactly n, with for each call an arbitrary, independent n between 1 and 128.

The question of what has been proved is even more acute than previously. The above informal specification could have several interpretations. Let us just say that one part of the main function used for the verification looks like this:

...
while(Frama_C_interval(0,1))
  {
    {
      int c = Frama_C_interval(0,1);
      if (c)
        {
          u08b_t msg[1];
          arbitrarize_msg(msg, 1);
          Skein_256_Update( &skein_context, msg, 1);
          continue;
        }
    }
    {
      int c = Frama_C_interval(0,1);
      if (c)
        {
          u08b_t msg[2];
          arbitrarize_msg(msg, 2);
          Skein_256_Update( &skein_context, msg, 2);
          continue;
        }
    }
    ...

In the verification described in detail until now, we re-use the same buffer for each call to Skein_256_Update. This is a small weakness in the verification plan: there could be a bug that happens only with two calls with two different buffers. For instance, Skein_256_Update could memorize the address of the buffer passed the first time, and access it on the second call, when the buffer may no longer exist. It goes to show that there is some validity to the question "what have you really proved?", but in this example, as often, the problem is with the ambiguous, informal specification and not with the formal method itself.

Using local variables as in the above C code snippet, the possibility of such a breach can be eliminated: we cannot prevent function Update to keep trace of a previous input buffer in its state, but if it then accessed it, or even just compared it to another address, this would be detected as an operation on a dangling pointer and an alarm would be emitted.

Digression: actually, we can also prevent function Update to keep trace of a previous input buffer, thanks to secondary analyses derived from the value analysis. One of them computes the set of locations written to by a C function. With this analysis, we can list the entire set of memory locations that Update uses as state, and check that only information that should be kept is. Here is a future blog post on this topic.

With the future Frama-C release, the verification takes about 5h and 150MiB of memory on a computer that was near top-of-the-line in 2006 (Intel Xeon 5150). Since we are speaking of performance, this analysis is single-threaded. With the memory footprint that it now has, there is hope that it will get a bit faster in time as a larger and larger proportion of the working set fits in lower and lower levels of memory cache. A parallel value analysis applicable to some verification plans (but untried for this one) is also at the proof-of-concept stage. Where applicable, this parallel analysis will allow to take advantage of multicore processors and computation farms.

Sunday, November 7 2010

Unspecified behaviors and derived analyses

Prologue

The C standard(s) specifies a minimum of things that all C compilers must agree on. For the sake of efficiency, many syntactically correct constructs are left without an unambiguous meaning.

The worst way for a construct not to have an unambiguous meaning is to be undefined behavior. An example of undefined behavior is invalid pointer access. Not all platforms have the required MMU, and even when they do, the MMU does not catch all invalid memory uses. Accessing an invalid pointer is not guaranteed to crash the program cleanly. A program that does so may "crash cleanly", or continue executing in an inconsistent state. The program may crash a little bit later because of the inconsistency, or it may appear to work fine and return a wrong result, or it may reformat your harddrive. All these behaviors and others are encompassed by "undefined behavior".

Compilers and compilation-platform-specific static analysis

Recently, C compilers have started to take advantage of undefinedness in the C99 standard for the sake of aggressive optimization. They apply program transformations that are only valid in the case of defined behaviors, and leave the program doing strange, unpredictable things in other cases. John Regehr has a very good explanation of C's undefined behaviors that spans three blog posts.

There are other, more benign ways for a construct not to have an unambiguous meaning, though. Implementation-defined behaviors must be documented and consistent for a given compiler. In the case of unspecified behaviors, one of several plausible alternatives must happen. In Frama-C, we have reclassified some unspecified, and even some undefined, behaviors as implementation-defined. For instance, the value analysis assumes by default that signed arithmetic overflows have been put there on purpose by the programmer and that he intended 2's complement modulo results. In this default configuration, the value analysis does not warn about these overflows and propagate 2's complement modulo results. John Regehr convinced us, however, that this was not satisfactory, so there is now an option -val-signed-overflow-alarms for when the programmer is not supposed to rely on this behavior (signed arithmetic overflows are technically undefined behavior). The Jessie plug-in allows roughly the same distinction, with the defaults reversed (by default, you get alarms for integer overflows). In short, a Frama-C analysis session is parameterized by a description of the compilation platform that includes genuine or reclassified implementation-defined choices.

That still leaves, of course, some unspecified and undefined behaviors that the value analysis or Jessie plug-ins do indeed warn about, and prove the absence of when they do not warn about them. Each construct that may cause some kind of unspecifiedness or undefinedness is the object of a warning containing the word assert in the value analysis log. Terms and conditions apply.

This post is about the one use case where the user does not have to worry about the alarms, So if you were tired of the ongoing thread about the verification of Skein-256, good news! This is something else.

Derived analyses

Well, I say "one" use case, but it's really a family of use cases. I am talking about all the analyses that are helping the user to comprehend the code, and that can therefore not mandate that all the alarms have been eliminated through the kind of laborious inspection and refinement illustrated in the Skein verification thread. Instead, the values, and therefore the results of the analysis that relies on them, are guaranteed to apply to well-defined executions only (executions that do not falsify any of the assertions that have been emitted). As long as this is kept in mind, it may even not be necessary to look at these alarms. In fact, it is standard for high-level analyzers of C programs to assume the absence of undefined behaviors or apply only to executions without undefined behaviors. Fast alias analyses intended to scale to millions of lines of C, for instance, assume that you do not transmit an address to pointer p by writing it in *(&q+1) where q is the address below p in memory. These analyses, and any other analyses that rely on the first ones, do not tell you whether you should have reasons to worry about this happening. If you should worry, they do not give you a list of dangerous constructs in the target program. The value analysis provides such a list of alarms, but you can ignore it if you wish, and then you get results with similar caveats.

Well, almost. We are finally arriving to the core of the problem.

What is a well-defined execution?

The value analysis is more precise and more aggressive than the typical large-scale alias analysis in its handling of what look like possible quirks in the analyzed program. The reason the -val-signed-overflow-alarms option mentioned above is not enabled by default is that several test programs became meaningless. The analysis was in effect saying "look, this program is sure to produce an overflow here at the third line, there is no point in going further until this has been resolved", and refused to analyze the rest of the program. The typical large-scale context-insensitive path-insensitive alias analysis does not have this problem, but that's only because it is too imprecise to have it. It is still making assumptions, such that you do not access p when you read or write from *(&q+1).

So does this mean that all high-level analyses of C programs are meaningless, unless the absence of undefined behaviors in target program is also verified(1)? In the style of Dan Simmons' Hyperion cycle, we are going to leave this crucial question for another volume, that is, a future blog post.

(1) which it rarely is in practice. As pointed out earlier, most of them do not even tell you whether you should worry and what to worry about.

page 2 of 2 -