On writing a dedicated model-checker for the RERS competition

In recent posts I have shown that Frama-C's value analysis could answer many reachability questions and some questions that weren't originally phrased as reachability questions about the programs in the RERS competition.

If you are vaguely familiar with the internals of Frama-C's value analysis and if you tried analyzing some of the competition programs yourself you may have noticed that these analyses use only a small fraction of the plug-in's capabilities. The analyzer is only ever propagating abstract states that correspond to singletons. It does juggle with many program states but the programs here have small states that are encoded in just a few variables (the analyzer would have been able to manipulate the states encoded on a much larger number of variables and would efficiently share in memory the values common to several of the explored states). There are no bit-fields no structs with padding (both of which might make identical states look different if carelessly handled). The programs obviously do not execute any undefined behavior for lack of any operation that might introduce them. There is a single outermost loop. There is no arithmetic at all.

In favor of the general verifier

A specialized verifier that was designed for just these programs would have a huge opportunity to do a better job on them. On the other hand the advantage of working on a more general verifier is that it is useful for more tasks. This enables to spend more time improving it. Some of the improvements enhance the analysis of many programs including the specific programs built only from assignments equality tests and conditionals considered in the competition. Some of these improvements are too sophisticated to justify implementing in a verifier that only handles programs with assignments equality tests and conditionals because such a verifier will never be usable to find that the SHA-3 candidate Skein's reference implementation does not exhibit undefined behavior that AES may be susceptible to timing attacks (but Skein isn't) where a couple of bugs are in an old undocumented piece of control software that there is a subtle memory overflow in compression library QuickLZ or that units of code have the data and control flows mandated by specification.

What a dedicated verifier might look like

In the particular case of these programs the same propagation done by the value analysis could be done in C by a program that would incorporate the transition function directly and execute it as compiled code. This would be much more efficient than what the value analysis does and in this particular case it would give the same results. From experiments interpreting Csmith programs the value analysis slowdown with respect to compiled code can be expected to be of the order of 10000.

Accumulating reachable states

In order to reproduce what Frama-C's value analysis does a dedicated verifier would need to store states that have already been visited and to be able to recognize after applying the transition function once more whether the obtained state was one that was already visited.

In this particular case this could be done in constant time with a hashset. Note however that it is only possible to compute a hash in this specialized case because all states are “singleton” states. If some states represented several values at once e.g. a1 ∈ {1; 2} a2 ∈ {0; 1} the good criterion would then be whether the newly computed state is included in one of the previously propagated states. Testing inclusion in one of the previous states cannot be done in constant time with a hashset (hashsets only allow you to test whether the new state is equal to an existing state and you need to be careful to use compatible equality and hash functions).

Frama-C's value analysis uses a data structure that is generally as efficient as hashsets when the manipulated states are singletons and that often remains efficient when testing inclusion in one another of states that are not singletons.

Storing states that remain to be propagated

A small thing: the propagation algorithm also requires a workqueue. Any propagation order will do (Frama-C's value analysis propagation order is not specified either) but since C comes with so few data structures I just thought I would mention it. For a dedicated verifier in C one would need to find some linked list implementation or write eir own. Frama-C's value analysis may interpret C slower than the code can be executed once compiled but it comes with ready to use data structures for the reached set and for the workqueue. One needs not even know they are there to use the analyzer.

Specific drawbacks

Obviously this ad-hoc verifier could be expected to be must faster than the value analysis. This makes the experiment tempting. What prevents me from starting work on it is the lack of generality of the resulting tool. Some examples follow.

Undefined behavior

Suppose that you had implemented such a specialized verifier for the competition's program and that you were looking for more transition functions written in C that the same verifier could apply to. You would certainly find some but would you in general be certain that the transition function never exhibits undefined behavior (not for the first transition and not for the transition from any reachable state to a successor)? If one isn't certain that the transition function does not cause undefined behavior from a formal verification point of view the tool is worthless. An undefined behavior can cause anything to happen. In particular an out-of-bounds memory access in the transition function can mess up the verifier's reached set or workqueue and compromise the results of the verification.

Any automatic verifier is susceptible to the caveat that a bug in the verifier can compromise results. This is different: your implementation could be flawless but it would still be susceptible to a bug in the transition function a bug in the system being verified.

Of course you could as a preliminary step in your verification check that the transition function does not have any undefined behavior for any input state. If you find that there are a lot of different undefined behaviors in C and that it's a bother to detect them all we have a tool that we have been working on. It also answers reachability questions.

General interference between unrelated traces

Even if you have only “frank” run-time errors to fear—undefined behavior that compilers kindly translate to run-time errors at least when optimizations are disabled— a run-time error in one transition will still interrupt the entire dedicated analyzer. You will notice when this happens and you can add a guard to the particular division by zero or NULL dereference but this iterative process may end up taking as long as the value analysis for the same result. The value analysis when encountering division by zero or NULL dereference makes a note of it considers the trace as terminated and goes on to the propagation of the next trace. The end result a list of run-time errors to worry about and a reachable states set is the same but it is obtained in a single pass.

There is also the issue of non-termination of the transition function. The value analysis detects cases of non-termination more or less quickly; again when the infinite loop is detected it simply goes on to the next trace. With an ad-hoc verifier if you expect the verification to take days it may take days before you realize that the verifier is executing an infinite loop in its third considered transition.

Conclusion

In summary considering the general C verification framework we already have it looks like it wouldn't be a good investment of our time to develop a dedicated fast verifier for the competition—although it would provide an insightful datapoint if someone did.

Perhaps participating in the meeting will convince us that Event Condition Action (ECA) systems are more generally useful than our current experience has led us to believe. We could work on a verifier for them if there is a need. There is not much code to reuse from a general-purpose C abstract interpreter. There would be ideas to reuse certainly. I will come to one of them in the next post.