Value-analysis assisted verification of output variables and information flow

A previous post in the value analysis thread in this blog contained this 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. Perhaps there will be a blog post on this topic.

Before the Carbon release, I wasn't in a hurry to talk about this. The value-analysis assisted computations of output variables and information flow are part of the many improvements in Carbon. In the Boron release and before, when applied on the Skein codebase, they gave results that were too approximated to be useful.

Now, they just work.

One example use of these computations is provided as part of the tutorial in the Carbon version of the value analysis manual (it's section 2.5.2 there).

Rather than repeating here this addition to the tutorial I want to reiterate on the notion of derived analysis. Although the outputs and dependencies computations rely on the results of the value analysis they do not require you to check each of the alarms generated by the value analysis.

When a sequence of function calls has dependencies (as computed by option -deps) of hash[0..7] FROM msg[0..79]; ONE[bits 0 to 7] (and SELF) it means that if all goes well array hash after the calls has been computed from array msg and variable ONE. Computing and taking advantage of this information is orthogonal to the verification that all always goes well during the execution of these function calls (which is done by making sure that the value analysis emits no alarm or by checking the emitted alarms with alternative techniques).

In more difficult cases the latter may require a combination of human reflexion and of hours of computer time. But functional dependencies can be useful even when based on the results of a simpler faster value analysis.