3 ms·
But when it's trivial to try QUADRILLION fuzzing operations (sixteen four gigahertz cores do this many operations every 4.1 hours) do you really need formal cor
by logicallee 10y ago
But when it's trivial to try QUADRILLION fuzzing operations (sixteen four gigahertz cores do this many operations every 4.1 hours) do you really need formal correctness? Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state?
We have so much power it's obscene. We're producing SHA-1 collisions without damaging or analyzing the algorithm, just using brute force. Why not take that approach to kernel security?
I'd sooner trust code whose quintillion input and output states have been exhaustively brute-forced over a few months (so that literally every possible path and value that code can take has ACTUALLY been run), than code which has been formally proven to be correct but without having been subject to such a test.
- caf 10y agoCan't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state? No. Take a simple function that has two 64-bit numbers as input and one output; your sixteen 4Ghz cores would take over 11 billion times the current age of the universe to verify it. You can, instead, do things like symbolic execution... and it turns out, that kind of thing is often a big part of "formally proven correct".
- logicallee 10y agoWhat do fuzzers do in practice? (I am not up on the state of the art)? They try to explore edge cases, but how do they know what is likely to be an edge case? Or how do they try to get coverage of their fuzzing?
- cnvogel 10y agoThey no longer just try out random combinations or cover the input space exhaustively (which is not feasible anyway). Nowadays they use instrumentation in the fuzzed/tested code to have guidance in what direction the input should be modified to get more cases the code covered. Good example: http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/
- caf 10y agoOne common technique (used by eg. AFL) is to instrument the program under test, so it can see when a different codepath has been triggered.