3 ms·
You can apply formal methods to code that you cannot in physical reality. If I show you the equation “x == y”, you won’t be able to pick 7 and 8 to make the equ
by anyfoo 6y ago
You can apply formal methods to code that you cannot in physical reality. If I show you the equation “x == y”, you won’t be able to pick 7 and 8 to make the equation true. If I give you a mechanical device that works with beads to answer the same question, you might make it work.
Of course computers are eventually physical reality, too, and things like rowhammer show that you don’t even need traditional “bugs” to escape your mathematical utopia.
But all the bugs talked about here are entirely the fault of the software.
- vntok 6y agoWell one could try to change the meaning of "==" to make the equation true. Think about comparator overloading in supported languages where the x and/or y variables are actually objects, for example.
- anyfoo 6y agoI was talking about algebra, not about C++.
- laumars 6y agoExcept you can artificially alter the value of x or y via numerous different methods of attack via frameworks that supersede the code which has been written the formal methods against.
- anyfoo 6y agoThen you did not do actual formal verification, but something wrong and useless.
- laumars 6y agoFuzz attacks have proven that edge cases are inescapable
- anyfoo 6y agoFuzzing 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.