5 ms·
Exhaustive search is untenable for the 64-bit case. Any strategy here? Testing 2^40 bits might be tenable; any way to select which ones would have the best ROI?
by kardos 8y ago
Exhaustive search is untenable for the 64-bit case. Any strategy here? Testing 2^40 bits might be tenable; any way to select which ones would have the best ROI?
- mehrdadn 8y agoIt's hard to give a general strategy without knowing the problem structure, but I guess you could say one general strategy is to exploit the problem structure in a way that lets you test multiple values in one shot.
- namibj 8y agoFeed llvm bytecode through Z3 and hope you didn't implement something with cryptographic behaviour.
- fao_ 8y agoCould you give some advice or pointers on this?
- namibj 8y agoThis should get you going. Come back if you get stuck. https://twitter.com/whitequark/status/915211914443153409 https://twitter.com/whitequark/status/915211914443153409 Edit: sorry, I just don't have the time to get you the details.
- pag 8y agoCheck out DeepState! https://github.com/trailofbits/deepstate https://github.com/trailofbits/deepstate
- reitzensteinm 8y agoI'm not so sure that's true. You can rent a Skylake chip on Google Cloud that'll perform 1.6 trillion 64 bit operations per second for $0.96/hr preemptively. That's enough to run one instruction over a 64 bit address space exhaustively over 120 days, or for ~$2800. Obviously that needs to be multiplied by the number of instructions a test needs to execute (and it has to be well written with AVX 512), but we're not talking nation state levels of resources here for simple cases, and that figure is only going to drop further with time. Not to mention the potential for FPGA or ASIC implementations if the tests are important enough.
- kardos 8y agoHmm that's surprisingly within reach. I bet you could crowd-source that kind of verification with BOINC.