Re: [Valgrind-developers] V-Bit Verification

[John R. <jr...@bi...>]

On 08/01/2012 05:42 PM, Lok Kwong Yan wrote:
> Please let me preface my comments with some comments on what we have done:

OK, but I have posted short test cases for which memcheck generates
false positive complaints of usage of uninit bits.  So far, analysis
and explanation have not fixed memcheck.

> 
> 1. Our formal model is for tainting, which is (should) be equivalent to "undefinedness" in memcheck.
> 2. Verification is also conducted for tainting. (Once again this should be equivalent to "undefinedness"). In particular, we have been successful in verifying or show that a bit that is marked as not-tainted is indeed not-tainted. We have not been successful (theorem prover times out) in verifying that something that is tainted CAN NOT be not-tainted - in all cases (e.g. this works for rotate left but not add). This means if a bit is marked as defined - then it is definitedly defined, whereas a bit that is marked as undefined can possible be defined. 

> 3. It is important to keep in mind that there are limitations to tracking definedness
> (or tainting) through instructions. For example, the simple combo of a = a & ~a
> is very hard to capture if we are looking at undefindness per instruction.
> Basically the problem is that we don't know what the overall operation
> is until we have processed over multiple instructions.

There are only two operations [instructions] involved in "(a & ~a)".
Why are two instructions so much more difficult than one?
If the representation of the output properties for an instruction
is in the same general form as the representation of the input properties,
then an ordinary theorem prover should be able to cascade the two operations,
and infer the conclusion quickly.

> 4. We have NOT conducted any analysis on floating point units - the fundamental problem
> for us is we haven't found an IEEE 754 model yet. Maybe we can write our own definitions?

There was a formal model of [some parts of?] IEEE 754 written in the "Z" verification
language (theorem prover language?), and some subset of the Transputer floating-point
subsystem was verified successfully against this model.  The work received
a commendation from the British Crown.  The Transputer was a chip of the
late 1980s by STMicroelectronics, SGS-THOMSON Microelectronics, etc.


> 5. Because the V-Bit rules are generic - they might lead to false positives for some special cases.
> I think a good comparison is LEAKPOINT, http://www.eecis.udel.edu/~clause/research/papers/clause-orso-icse10.pdf.

Thank you for the reference!

> It is very interesting to me that their taint propagation rules (or definedness rules) are much simpler
> than the V-Bit rules, but for their tests they achieved the same detection rate. I am not saying
> that it will always remain true, but it is enlightening how simple rules can cover so many test cases.

"detection rate" should be perfect: no false positives, no false negatives.
This is _hardware_: so simple that even silicon can do it correctly
[and profitably for the chip maker, even after all that research and
development, chip fabrication, marketing, ...]


[[Notice the different style of quoting below this point.]]

> Memcheck does not understand word-wide binary integer inequality.
> [snip]

> LOK: *** From what I can see in the memcheck source code (mc_translate.c)
> it seems like there is already support for accurately calculating the CmpEQ and CmpNE.
> These rules seems correct - at least from my understanding of it, but I just
> need to verify that they are correct.

Whatever the support for accurately calculating CmpNE, nevertheless
memcheck generates a false positive complaint.  The test case in
Bug 117362 still fails for me under memcheck 3.7.0 [the current release],
almost SEVEN YEARS after first filing.

> 
> Memcheck does not understand binary integer addition.
> [snip]

> LOK: *** I am also a little bit confused about the carry problem since there
> expensiveAddSub (in mc_translate.c) seems to address the problem outlined above.
> the default LEFT operation does not though.

Did you try the test case?  memcheck 3.7.0 gives me a false positive complaint.

> Memcheck gives up if it encounters Undef bits in floating point arithmetic.
> [snip]

> LOK: *** Floating point is hard

Floating point may be long (de-compose into several pieces of integers, operate,
re-compose into floating point), but it is not difficult.

> [snip]    Shifting by
> "either 2 or 3" (because of an Undef low bit in the count) need not
> totally destroy the output, although in this case memcheck says "every bit
> of the result is Undef, regardless of the actual bits and actual V bits
> of the other operand."
> 
> LOK: *** I agree that the pessimistic nature of the shift count being undefined
> means the whole result is undefined could cause problems. At the same time,
> it makes a lot of sense to make that tradeoff if performance is an issue.
> We might be able to come up with improved rules (like the ones that were defined
> for AND/OR/CMP/ADD/SUB) and if our model and methods turn out to be correct,
> then verification of these new rules is possible.

It seems to me that the performance issue can be handled by case analysis.
The inline code emulates the operation as if all inputs are Valid ("untainted"),
and in parallel performs such a check.  If there are any Uninit bits ("tainted")
then call an out-of-line helper, possibly semi-interpreted [perhaps even
re-parsing the actual client target instruction] and possibly with a special
calling sequence, not necessarily the normal ABI calling convention.

--