|
From: Lok K. Y. <lo...@sy...> - 2012-07-27 16:17:47
|
All, I am interested in the accuracy of the V-Bit calculations and would like to know: 1. Is there anyone who is working on Memcheck V-Bit Verification? 2. Is there a more updated list of operations in addition to the ones described in the original USENIX ATC paper in 2005? Thank you for your help. Enjoy, Lok |
|
From: Julian S. <js...@ac...> - 2012-08-01 19:16:34
|
> I am interested in the accuracy of the V-Bit calculations So am I. > 1. Is there anyone who is working on Memcheck V-Bit Verification? It has been looked at informally from time to time, but there has never been a formal study of it, as far as I know. It would be really great to have more analysis of it. Even better would be to have a test suite, since a formal proof is a one-time thing that becomes invalid as soon as the Memcheck code changes. Florian Krohm worked on tester which is at https://bugs.kde.org/show_bug.cgi?id=300102 Not sure of its current status though. > 2. Is there a more updated list of operations in addition to the > ones described in the original USENIX ATC paper in 2005? That paper is quite out of date on the details, although the basic ideas are still valid. To see the set of primitive operations which give 95% of the complexity in Memcheck instrumentation, have a look in VEX/pub/libvex_ir.h, at the type IROp. ----- Can you say a bit more about what your goals are? ----- It would be nice to have a way to test Memcheck's V-bit propagation through each IROp individually -- that would provide a way to do the abovementioned regression test. This requires 2 parts: first, a way to set and get V bits on arbitrary pieces of memory. That is easy -- the VALGRIND_GET_VBITS and VALGRIND_SET_VBITS client requests. The second thing that is required is a way to write an instruction that passes its operands though an IROp that is specified in a test program, and no others -- so they can be tested individually. One way we could achieve this is to extend the "Special" instruction mechanism (eg, see guest_amd64_toIR.c and search for "Special") so that it will accept a pseudo-instruction with a specified IR op in the middle of it. J |
|
From: John R. <jr...@bi...> - 2012-08-01 22:32:42
|
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.]
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)
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.
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."]
--
|
|
From: Julian S. <js...@ac...> - 2012-08-02 08:31:05
|
On Thursday, August 02, 2012, John Reiser wrote: > I consider that memcheck often generates incorrect V bits. Yes. This is by design. There's a tradeoff between accuracy of V bit tracking and performance. Memcheck is designed to be accurate enough to give a low false positive rate in real use scenarios whilst not being excessively slow. It is also designed to err on the side of false positives rather than false negatives. If there's one single thing that Loyan's crew could usefully do, it is to show that if a bit is marked as defined then it really is defined -- that is, demonstrate that there are no false negatives. False positives are inconvenient and we try to minimise them, but fundamentally are not a hindrance to using Memcheck to making software more reliable, since they can be worked around by over-initialising data. False negatives are dangerous -- they cause program flaws to be missed and there is no way to recover from that. > Memcheck does not understand word-wide binary integer inequality. > !!((a ^ b) & Va & Vb) ==> (a != b) True. Is this a problem in practice? I don't remember many bug reports about this. > Memcheck does not understand binary integer addition. [...] Yeah. We know. It leads to bug 242137. There is a mode in which addition is done exactly. The problem is it is slow and is not necessary 99.9% of the time. It would be nice to have an intermediate-cost version which is accurate enough to correctly handle the underlying LLVM optimisation whilst not being as expensive as the full version, but I'm not sure this is possible. > Memcheck gives up if it encounters Undef bits in floating point arithmetic. Yes. Show me the bug reports where this causes users problems in practice. > (a ^ a) ==> 0 regardless of Undef in 'a'; but memcheck ignores this xor-with-self cases are transformed out by iropt upstream of instrumentation, which gets rid of all such cases resulting from xoring a register with itself. > (x & ~x) ==> 0 regardless of Undef in 'x'; but memcheck ignores this Mmhmh, is this really a problem in practice? J |
|
From: Florian K. <br...@ac...> - 2012-08-02 00:26:33
|
On 08/01/2012 03:08 PM, Julian Seward wrote: > Even better would be > to have a test suite, since a formal proof is a one-time thing > that becomes invalid as soon as the Memcheck code changes. > > Florian Krohm worked on tester which is at > https://bugs.kde.org/show_bug.cgi?id=300102 > Not sure of its current status though. > Dormant but not forgotten. > It would be nice to have a way to test Memcheck's V-bit > propagation through each IROp individually -- that would provide > a way to do the abovementioned regression test. This is what I do, essentially. The tester generates an asm program that tests propagation of undefinedness through a specific IROp. So you need an asm insn that maps to the IROp you want to test. If you don't have that you cannot test it. That's a limitation. It tests for each input bit of the IROp in isolation that its undefinedness propagates properly to the output bits. > This requires 2 > parts: first, a way to set and get V bits on arbitrary pieces of > memory. That is easy -- the VALGRIND_GET_VBITS and > VALGRIND_SET_VBITS client requests. > > The second thing that is required is a way to write an > instruction that passes its operands though an IROp that is > specified in a test program, and no others -- so they can be > tested individually. One way we could achieve this i to extend > the "Special" instruction mechanism (eg, see guest_amd64_toIR.c > and search for "Special") so that it will accept a > pseudo-instruction with a specified IR op in the middle of it. Interesting idea with the advantage that you don't have to retarget it. I'll keep it in mind. Florian |
|
From: Lok K. Y. <lo...@sy...> - 2012-08-02 01:07:14
|
In our case, we use SMT2 and bitvectors to model the v-bit calculation behavior and then verify the model. Since the bitvector operations are very similar to VEX IR operations, it should not take long to convert the IR implementation into SMT2 or similar. ________________________________________ From: Florian Krohm [br...@ac...] Sent: Wednesday, August 01, 2012 8:26 PM To: Julian Seward Cc: val...@li... Subject: Re: [Valgrind-developers] V-Bit Verification On 08/01/2012 03:08 PM, Julian Seward wrote: > Even better would be > to have a test suite, since a formal proof is a one-time thing > that becomes invalid as soon as the Memcheck code changes. > > Florian Krohm worked on tester which is at > https://bugs.kde.org/show_bug.cgi?id=300102 > Not sure of its current status though. > Dormant but not forgotten. > It would be nice to have a way to test Memcheck's V-bit > propagation through each IROp individually -- that would provide > a way to do the abovementioned regression test. This is what I do, essentially. The tester generates an asm program that tests propagation of undefinedness through a specific IROp. So you need an asm insn that maps to the IROp you want to test. If you don't have that you cannot test it. That's a limitation. It tests for each input bit of the IROp in isolation that its undefinedness propagates properly to the output bits. > This requires 2 > parts: first, a way to set and get V bits on arbitrary pieces of > memory. That is easy -- the VALGRIND_GET_VBITS and > VALGRIND_SET_VBITS client requests. > > The second thing that is required is a way to write an > instruction that passes its operands though an IROp that is > specified in a test program, and no others -- so they can be > tested individually. One way we could achieve this i to extend > the "Special" instruction mechanism (eg, see guest_amd64_toIR.c > and search for "Special") so that it will accept a > pseudo-instruction with a specified IR op in the middle of it. Interesting idea with the advantage that you don't have to retarget it. I'll keep it in mind. Florian ------------------------------------------------------------------------------ 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 |
|
From: Julian S. <js...@ac...> - 2012-08-02 08:51:38
|
> > The second thing that is required is a way to write an > > instruction that passes its operands though an IROp that is > > specified in a test program, and no others -- so they can be > > tested individually. One way we could achieve this i to extend > > the "Special" instruction mechanism (eg, see guest_amd64_toIR.c > > and search for "Special") so that it will accept a > > pseudo-instruction with a specified IR op in the middle of it. > > Interesting idea with the advantage that you don't have to retarget it. The _toIR.c's for the architectures that we'd want to test on would require some minor modification. Also, we would have to specify these pseudo instructions to take operands from memory and write results back to memory, since without that we'd have to write target-specific assembly to get the operands to/from specific registers. So, yes, could be retargetable with a little care. J |
|
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 |
|
From: John R. <jr...@bi...> - 2012-08-02 03:33:57
|
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. -- |
|
From: Lok K. Y. <lo...@sy...> - 2012-08-03 20:34:14
|
I am not overly familiar with Valgrind/Memcheck's configuration options and don't know what "bogusLiterals" are, but I did go into mc_translate.c and forced the usage of the expensiveCmpEQorNE and the false positive in bug 117362 is gone.
Perhaps someone more familiar with Valgrind can tell us how to enable the slow-but more accurate version of Memcheck without my hack. They might also be able to shed more light on the other bugs outlined below.
*** Output from Valgrind ***
==22113== Memcheck, a memory error detector
==22113== Copyright (C) 2002-2011, and GNU GPL'd, by Julian Seward et al.
==22113== Using Valgrind-3.7.0 and LibVEX; rerun with -h for copyright info
==22113== Command: ./a.out
==22113==
==22113==
==22113== HEAP SUMMARY:
==22113== in use at exit: 4 bytes in 1 blocks
==22113== total heap usage: 1 allocs, 0 frees, 4 bytes allocated
==22113==
==22113== LEAK SUMMARY:
==22113== definitely lost: 4 bytes in 1 blocks
==22113== indirectly lost: 0 bytes in 0 blocks
==22113== possibly lost: 0 bytes in 0 blocks
==22113== still reachable: 0 bytes in 0 blocks
==22113== suppressed: 0 bytes in 0 blocks
==22113== Rerun with --leak-check=full to see details of leaked memory
==22113==
==22113== For counts of detected and suppressed errors, rerun with: -v
==22113== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 16 from 11)
*** Changes in the code ***
Lines 3181-3200 in mc_translate.c
case Iop_CmpEQ64:
case Iop_CmpNE64:
if (1 || mce->bogusLiterals) //short circuited this test
return expensiveCmpEQorNE(mce,Ity_I64, vatom1,vatom2, atom1,atom2 );
else
goto cheap_cmp64;
cheap_cmp64:
case Iop_CmpLE64S: case Iop_CmpLE64U:
case Iop_CmpLT64U: case Iop_CmpLT64S:
return mkPCastTo(mce, Ity_I1, mkUifU64(mce, vatom1,vatom2));
case Iop_CmpEQ32:
case Iop_CmpNE32:
if (1 || mce->bogusLiterals) //short circuited this test
return expensiveCmpEQorNE(mce,Ity_I32, vatom1,vatom2, atom1,atom2 );
else
goto cheap_cmp32;
cheap_cmp32:
case Iop_CmpLE32S: case Iop_CmpLE32U:
case Iop_CmpLT32U: case Iop_CmpLT32S:
return mkPCastTo(mce, Ity_I1, mkUifU32(mce, vatom1,vatom2));
Also, I will look into the Z model for floating point. Thank you for the pointer.
Enjoy,
Lok
________________________________________
From: John Reiser [jr...@bi...]
Sent: Wednesday, August 01, 2012 11:34 PM
To: val...@li...
Subject: Re: [Valgrind-developers] V-Bit Verification
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.
--
------------------------------------------------------------------------------
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
|