|
From: Lok K. Y. <lo...@sy...> - 2012-08-02 00:58:07
|
Please let me preface my comments with some comments on what we have done: 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. 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? 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. 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. ________________________________________ From: John Reiser [jr...@bi...] Sent: Wednesday, August 01, 2012 6:33 PM To: val...@li... Subject: Re: [Valgrind-developers] V-Bit Verification On 08/01/2012 12:08 PM, Julian Seward wrote: > >> I am interested in the accuracy of the V-Bit calculations > > So am I. I consider that memcheck often generates incorrect V bits. Memcheck does not understand word-wide binary integer inequality. !!((a ^ b) & Va & Vb) ==> (a != b) [inequality at any position that has two Valid bits determines Valid inequality for the whole operation. http://bugs.kde.org/show_bug.cgi?id=117362 Summary: false positive uninit for bitfields or partial word. This bug is nearing 7 years old (filed 2005-11-30) and includes three suggested approaches for a fix.] 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. Memcheck does not understand binary integer addition. If there is a place value [bit number] at which both operands have a Valid zero bit, then a CarryIn which propagates into that bit gets stopped (CarryOut is guaranteed to be zero), but memcheck will propagate an Undef Carry through that bit position anyway. Memcheck propagates Undef "all the way to the left" regardless of CarryStop. ----- #include <stdlib.h> #include <stdio.h> main(int argc, char *argv[]) { int *p = malloc(sizeof(int)); *p &= 0xff; /* top 24 bits of *p are Valid and zero */ int *q = malloc(sizeof(int)); *q &= 0xff; /* top 24 bits of *q are Valid and zero */ /* The top 23 bits of the sum are Valid and zero. */ if ((*p + *q) < 0) { printf("Impossible.\n"); } return 0; } ----- The complaint from memcheck [below] is incorrect. ==15496== Conditional jump or move depends on uninitialised value(s) ==15496== at 0x400585: main (memcheck-add.c:11) 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. Memcheck does not understand unsigned integer remainder by 2**n-1. (((a*256*256*256) + (b*256*256) + (c*256) + d) % 255) == ((a+b+c+d) % 255) >From that it can be seen that Undef "middle" bits in each of a,b,c,d do not affect the V bits for low bits of the remainder, as long as (a+b+c+d) < 255. But memcheck says that any Undef on input gives an Undef remainder. Memcheck gives up if it encounters Undef bits in floating point arithmetic. If either operand has any Undef bits, then all bits of all results are Undef. In practice for floating point compare, often this is the worst thing to do. It is very likely that the floating condition codes do not depend on a few Undef bits in either input. [Numerical analysis wouldn't exist if it did.] Almost the same can be said for floating point addition, subtraction, and multiplication: the sign, exponent and more-significant fraction bits of many particular results often do not depend on a few less-significant fraction bits. LOK: *** Floating point is hard Beyond individual operations, memcheck is blind with respect to "re-convergent fan-out". If there is any common history between the two operands, then memcheck does not care, even though the result may. (a ^ a) ==> 0 regardless of Undef in 'a'; but memcheck ignores this (x & ~x) ==> 0 regardless of Undef in 'x'; but memcheck ignores this Generally, memcheck often ignores any contribution that the actual values of Valid operand bits might make to the Valid bits of the result. That is, memcheck often believes that the V bits of the result depend only on the opcode and the V bits of the inputs, and not on the inputs themselves (in particular, the actual values of input bits that are Valid.) [If the actual shift count is all-Valid, then "shift by variable number of bits" is an exception. But if the shift count itself has any Undef bits, then memcheck says "all result bits are Undef" even though a detailed analysis might not give such a pessimistic result. 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. -- ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ Valgrind-developers mailing list Val...@li... https://lists.sourceforge.net/lists/listinfo/valgrind-developers |