Some context on this article.<p>This article is targeted at proving programs that run on blockchain based virtual machines.<p>These VM's are deterministic to their core. This is quite different the envirnoments that than most programs run in. For example every time code on the EVM runs in production, it is being run in parallel on hundreds to hundreds of thousands of systems, and the outputs/storage writes/events all have to agree exactly after execution, or bad things things happen. The EVM is also single threaded, reasonably well defined, and with multiple different VM implementations in many different languages. So programs here are much easier to verify.<p>In addition, program execution costs are paid per opcode executed, so program sizes range from hundreds of lines to about thirty thousand lines (with the high side of that being considered excessive and insane). It's again quite different than the average desktop software, or even embedded, program size.<p>I have both used fuzzing tools (actually working on reviewing a fuzzing setup today) and formal verification in the past. I agree with the article that currently fuzzing provides a similar level of verification for considerably less effort. Current formal verification systems in the blockchain based virtual machine space are extremely difficult to write good specs for, and extremely easy to write broken specs that don't check what you think they do. On the other hand, good enough specs for fuzzing are fairly intuitive, even if great specs still take a lot of expertise.<p>If I had a math heavy set of code that I wanted to wring the last possible security assurances from, I'd go for formal verification on top of fuzzing. But for most other work, I'd pick fuzzing.<p>(Disclosure, I've been a customer of Trail of Bits, and worked with two of the three authors in the paper)<p>(This isn't to say that form verification will never catch up! I'm thankful for the hard work from the people who have been moving it forward - it's gotten much better over the last two years. One day maybe it will be just as easy.)
A point they're implicitly making is: it's harder to apply formal methods retrospectively. The state of the art in formal verification involves writing the proofs jointly with the code in a language designed for verification, such as Dafny (earlier), F*, or VeRus (emerging).<p>Fuzzing is much easier to add to an existing system - though even there, there's a lot of benefit from designing for testability.
I don't think that fuzzing and formal methods are opposed. First, formal verification is only as good as the specifications and the extraction / equivalence proofs. Likewise, fuzzing by its very nature never reaches full coverage of a code base. However, they are complementary. Adding fuzzing to a formally verified system is a great way to find gaps in the specification or the proofs. Humans write specs and proofs. Humans are fallible. Fuzzing is a great way to explore the health of the specification and implementation.<p>Likewise, building toward a formal specification is a great way to convert errors found by the fuzzer into a class of error, and then build up a means by which that class of error can be eliminated entirely from the code base.<p>The WPA2 protocol -- not its implementation -- was partially verified using formal methods. Unfortunately, there was a flaw in this specification, which led to a poorly crafted state machine. This led to the KRACK attacks. Complementing these specifications with fuzzing could have found these attacks sooner. Researchers have since refined formal modeling of WPA2 to prove that the patches to the KRACK attacks prevent them.<p><a href="https://www.usenix.org/conference/usenixsecurity20/presentation/cremers" rel="nofollow">https://www.usenix.org/conference/usenixsecurity20/presentat...</a><p>These tools are defense in depth for design. None of them are complete on their own.
Formal methods is what happens when you try to do engineering in the traditional sense in the software space. You sit down, design, find a specification, and then build to spec. It's arguably an idealized version, even, because depending on the methods you cannot fail the spec if you succeed in building it.<p>Only a small group of software engineers are interested in this principled approach. Hell many software engineers are scared of recursion.
The spec may be provably perfect, but how to you prove the code perfectly conforms to the spec? I don't think you can.<p>This is why I like end to end tests, UA testing, fuzzing, and property-based tests.
If/when Lean 4 matures more and adds support for formal verification of code, I would like to see it gain high-quality fuzzers as well. Its relatively good speed (hopefully with the new compiler) could make it a good candidate for fusing these two strategies.
int Mid = (high + low) / 2;<p>The above line is easy to formally prove correct. However it is wrong - if high + low is greater than int_max on your system you have a bug.<p>I'm still in favor of formal proofs, but there are limits to what it can do.