randomvisitor

7 ms·

1. 1.▲
   by randomvisitor 13y ago

   In fact you can perform a birthday attack, which costs on the order of 2^16 calls with n=32. I'm surprised the researchers don't mention this: they're handwaving counter-attacks away because of the "very good digital pos
2. 2.▲
   by randomvisitor 13y ago

   > they are using unsigned 64-bit values (which conveniently have defined overflow semantics) for the lengths of the input buffer. Yes, if you examine the code you can manually prove that it's safe: but that's not proven by thei
3. 3.▲
   by randomvisitor 13y ago

   > No variation of the gravitational constant is discernible, (dG/dt) / G = (0.0±1.1)x10–12 /yr If we're obsessing over details, I'm wondering if 0.0 is indeed the center of the confidence interval, or if this is
4. 4.▲
   by randomvisitor 13y ago

   It's a flaw in the specification of the theorem, not in the verification. The way it works is that they choose fixed sizes INLEN and OUTLEN, and prove that when data points to a buffer of INLEN bytes, they can allocate a result buffer
5. 5.▲
   by randomvisitor 13y ago

   It's pretty impressive that this can be done completely automatically (model checking), although the price to pay is that he can only prove the implementation for a fixed input size. I'm very curious about what would happen if he