3 ms·

Wow, that's actually really cool. Thank you so much for such an awesome answer, I learned a lot from your pastebin. So you mentioned that it can handle things

by Exuma 7y ago

Wow, that's actually really cool. Thank you so much for such an awesome answer, I learned a lot from your pastebin. So you mentioned that it can handle things like overflows. Does this include all the things a fuzzer might find? This article says "hacker-proof." Is that hyperbole (which implies 100% certainty in my mind) or is there a margin of error in this type of system. I'm just imagining things how large codebases with lots of maintainers still have bugs found every day from fuzzing. I would imagine if its near 100% that assumes the system that checks it is also free of bugs... quite fun to think about.

docandrew 7y ago
Flow analysis and SMT solvers are mathematically-sound, so if done correctly, a fuzzer would have no luck finding a path through the code where any undefined behavior (or behavior that violates the contracts you've specified) could take place. Getting started with SPARK, you'll see messages like "Can't prove that this variable won't overflow" (usually with corner cases like "when x = 4,294,967,295 and y = -1"). So it kind of makes you realize how error-prone code can be. A statement like "x++" has the assumption baked into it that x isn't going to be INT_MAX. Fuzzers work by manipulating your control flow such that x _will_ be INT_MAX and cause an overflow or other bad stuff. Formal verification exposes all those assumptions and when people complain about slow development, it's because you're basically making the code "fuzzer-proof". "Hacker-proof" is hyperbole, but not as much as some might have you believe. People have pointed out that the specification has to be correct. My code in the pastebin proves every element in the output array is even, but if the code is supposed to produce an array of odd numbers, then obviously that's still a bug, even though it's been "formally verified". I wouldn't use the term "hacker-proof", but I would say "hacker-resistant". FV _can_ eliminate whole classes of vulnerabilities that attackers could otherwise use. A common trope is "well there's still hardware bugs or the spec could be wrong, so why bother?" I mean, sure, a hacker could cut the power to the datacenter, too, but IMO that's not a reason to ignore tools that can make the software we write much more robust. One issue that can crop up is that you can't always prove what you're trying to specify. The state space can grow too big and the solver can't figure it out in a timely fashion, so you have to make assumptions and hope your tests give you enough confidence to deploy the system. This is basically the halting problem - it doesn't say that it's impossible to prove termination (or any other property) of some code, it just says that you can't _always_ prove them. nVidia recently began using SPARK in some of their work, the video does a good job explaining some of the bugs that FV eliminates: https://www.youtube.com/watch?v=DZSSyWlsb28 https://www.youtube.com/watch?v=DZSSyWlsb28
- Exuma 6y ago
  Dude -- awesome. Thank you so much for writing all that, it was extremely fascinating to read. I'll watch the video now... thanks again. And also that makes perfect sense.
touisteur 6y ago
To me fuzzing still helps finding problems the Formal method of choice doesn't cover. Typically my favorite example is stack use or runtime-duration. I can write a parser guaranteed to have no runtime error (bounds, over/underflow, divide by zero) and still make it crash because of stack or heap exhaustion. Or I can find tortuous cases of denial if service. Because the tool doesn't handle (at the moment) stack or heap size, or execution duration. Fuzzing still helps a lot in those cases! Especially if you focus on those kinds of problems.

by Exuma 7y ago

docandrew 7y ago

Flow analysis and SMT solvers are mathematically-sound, so if done correctly, a fuzzer would have no luck finding a path through the code where any undefined behavior (or behavior that violates the contracts you've specified) could take place. Getting started with SPARK, you'll see messages like "Can't prove that this variable won't overflow" (usually with corner cases like "when x = 4,294,967,295 and y = -1"). So it kind of makes you realize how error-prone code can be. A statement like "x++" has the assumption baked into it that x isn't going to be INT_MAX. Fuzzers work by manipulating your control flow such that x _will_ be INT_MAX and cause an overflow or other bad stuff. Formal verification exposes all those assumptions and when people complain about slow development, it's because you're basically making the code "fuzzer-proof". "Hacker-proof" is hyperbole, but not as much as some might have you believe. People have pointed out that the specification has to be correct. My code in the pastebin proves every element in the output array is even, but if the code is supposed to produce an array of odd numbers, then obviously that's still a bug, even though it's been "formally verified". I wouldn't use the term "hacker-proof", but I would say "hacker-resistant". FV _can_ eliminate whole classes of vulnerabilities that attackers could otherwise use. A common trope is "well there's still hardware bugs or the spec could be wrong, so why bother?" I mean, sure, a hacker could cut the power to the datacenter, too, but IMO that's not a reason to ignore tools that can make the software we write much more robust. One issue that can crop up is that you can't always prove what you're trying to specify. The state space can grow too big and the solver can't figure it out in a timely fashion, so you have to make assumptions and hope your tests give you enough confidence to deploy the system. This is basically the halting problem - it doesn't say that it's impossible to prove termination (or any other property) of some code, it just says that you can't _always_ prove them. nVidia recently began using SPARK in some of their work, the video does a good job explaining some of the bugs that FV eliminates: https://www.youtube.com/watch?v=DZSSyWlsb28 https://www.youtube.com/watch?v=DZSSyWlsb28

Exuma 6y ago
Dude -- awesome. Thank you so much for writing all that, it was extremely fascinating to read. I'll watch the video now... thanks again. And also that makes perfect sense.

touisteur 6y ago

To me fuzzing still helps finding problems the Formal method of choice doesn't cover. Typically my favorite example is stack use or runtime-duration. I can write a parser guaranteed to have no runtime error (bounds, over/underflow, divide by zero) and still make it crash because of stack or heap exhaustion. Or I can find tortuous cases of denial if service. Because the tool doesn't handle (at the moment) stack or heap size, or execution duration. Fuzzing still helps a lot in those cases! Especially if you focus on those kinds of problems.