2 ms·

Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive. I

by anyfoo 6y ago

Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive. In a formally verified program, fuzzing is redundant and useless. Are you going to fuzz the program "x = y+1; return x;", or are you convinced already that it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x), and that it will never access memory out of bounds? Formal verification is exactly that, just usually in less obvious scenarios. Advanced type systems do the same implicitly by making expressions that would violate such properties (or where they cannot be proven) not type check.

Sharlin 6y ago
> x = y+1; return x; Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.
- skissane 6y ago
  > In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
- anyfoo 6y ago
  I did not fail to take that into account: > it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x) And it does not matter, since the point of formal verification is to help taking those issues into account.
  - Sharlin 6y ago
    Pardon me if I'm missing something, but I only see the "natural number" case and the "unsigned" case (the latter of which is indeed well-defined to wrap around to zero in C and C++), but I was talking about the case where x and y have, say, type signed int. Then all bets are off if y happens to equal INT_MAX in some execution, because the compiler is allowed to optimize with the assumption that that literally cannot happen. At least as far as the C standard is concerned. So my point was that in the real world, even such a trivial function may not only yield unexpected results but indeed cause the whole program to have arbitrary, undefined behavior.
laumars 6y ago
My point is that only works if you’re writing the entire software stack. The moment you rely on someone else’s library, whether it’s to read from a file descriptor, a libc wrapper around an OS SYSCALL or whatever, you’re opening up your program to unexpected behaviour. And that’s not even taking into account the slew of very real software bugs that can be introduced from unexpected hardware behavior. Using formal method might prove your applications logic but it doesn’t prove a buffer overflow bug in a library you’ve used, or the OS you’re running on, or the compiler you’ve used from introducing a bug, nor even the hardware itself. Computers these days are sufficiently complex and with enough abstractions that there’s no such thing as a guarantee.
- anyfoo 6y ago
  I wrote this: > Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive.

by anyfoo 6y ago

Sharlin 6y ago

> x = y+1; return x; Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.

skissane 6y ago
> In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
anyfoo 6y ago
I did not fail to take that into account: > it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x) And it does not matter, since the point of formal verification is to help taking those issues into account.
- Sharlin 6y ago
  Pardon me if I'm missing something, but I only see the "natural number" case and the "unsigned" case (the latter of which is indeed well-defined to wrap around to zero in C and C++), but I was talking about the case where x and y have, say, type signed int. Then all bets are off if y happens to equal INT_MAX in some execution, because the compiler is allowed to optimize with the assumption that that literally cannot happen. At least as far as the C standard is concerned. So my point was that in the real world, even such a trivial function may not only yield unexpected results but indeed cause the whole program to have arbitrary, undefined behavior.

laumars 6y ago

My point is that only works if you’re writing the entire software stack. The moment you rely on someone else’s library, whether it’s to read from a file descriptor, a libc wrapper around an OS SYSCALL or whatever, you’re opening up your program to unexpected behaviour. And that’s not even taking into account the slew of very real software bugs that can be introduced from unexpected hardware behavior. Using formal method might prove your applications logic but it doesn’t prove a buffer overflow bug in a library you’ve used, or the OS you’re running on, or the compiler you’ve used from introducing a bug, nor even the hardware itself. Computers these days are sufficiently complex and with enough abstractions that there’s no such thing as a guarantee.

anyfoo 6y ago
I wrote this: > Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive.