Why fuzzing over formal verification?
blog.trailofbits.com
blog.trailofbits.com
This article is targeted at proving programs that run on blockchain based virtual machines.
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.
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.
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.
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.
(Disclosure, I've been a customer of Trail of Bits, and worked with two of the three authors in the paper)
(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.)
Fuzzing is much easier to add to an existing system - though even there, there's a lot of benefit from designing for testability.
You just to mark some variables as symbolized and bound the loops.
cbmc
Cmbc is -useful- and lets you check some important safety properties and it's a great tool. But it's not the state of the art in terms of how extensively you can check things with formal verification. It's closer to the state of the art of what you can do with legacy code.
Things like VeRus let you write annotated rust together with proofs that can show higher-level properties such as liveness, mutual exclusion, etc.
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.
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.
https://www.usenix.org/conference/usenixsecurity20/presentat...
These tools are defense in depth for design. None of them are complete on their own.
Only a small group of software engineers are interested in this principled approach. Hell many software engineers are scared of recursion.
For a bridge, you specify that it needs to withstand specific static and dynamic loads, plus several other things like that. Once you have the a handful of formulas sorted out, you can design thousands of bridges the same way; most of the implementation details, such as which color they paint it, don't matter much. I'm not talking out of my butt: I had a car bridge built and still have all the engineering plans. There's a lot of knowledge that goes into making them, but the resulting specification is surprisingly small.
Now try to formally specify a browser. The complexity of the specification will probably rival the complexity of implementation itself. You can break it into small state machines and work with that, but if you prove the correctness of 10,000 state machines, what did you actually prove about the big picture?
If you want to eliminate security issues, what does it even mean that a browser is secure? It runs code from the internet. It reads and writes files. I talks directly to hardware. We have some intuitive sense of what it's supposed and not supposed to do, but now write this down as math...
This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind.
The added complexity of formal verification languages creates an opening for specification bugs to creep in. The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up.
I'm been deeply cynical about formal verification ever since. I'm not even of the opinion that it's "maybe not good for us, but good for building code for rocket ships". I think it might be actually bad at that too.
I'm bullish on more sophisticated type systems and more sophisticated testing, but not formal verification.
Second:
> The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up.
Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?
c.f.
https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
Formal verification doesn't prove that bugs don't exist either, thanks to the aforementioned "bugs in the spec" scenario.
I'm saying that, anecdotally, when I tried it I had more bugs thanks to formal verification because bugs crept into the spec. It was very hard to tell that those bugs were present because the spec was very, very complicated.
I'm not denying that it can catch bugs at all, just that a successful "proof" didn't mean a lack of bugs and that I personally found it to be a relatively inefficient method of catching bugs (or demonstrating their nonexistence).
Well, OK, but the reason you have "bugs" in your specifications is usually that the English-language (or whatever you have) informal requirements documentation is imprecise, ambiguous or contradictory.
At least with a formal specification, you shouldn't have that problem.
Formal specification languages are more likely to have specification bugs despite being precise and unambiguous for the same reason programming languages have bugs despite being precise and unambiguous: they are complicated and extremely expressive languages which means a larger scope for mistakes, misunderstandings and accidental misinterpretation.
Were formal specification languages straightforward and simple the scope for misunderstanding and misinterpretation would decline, but so would the power to "prove" the code is free of bugs.
My primary experience with formal specifications is as part of a literate specification, where you would have a rigorous English-language explanation interspersed with the formal specification (e.g. Z schemata).
A reader can look at the formal specification and the English and decide whether they think they mean the same thing; experience suggests that most engineers or people with STEM-type backgrounds need no more than a few days of training to be able to read Z (even if they can't write it).
The document as a whole can be type-checked, which is a lightweight way to check for the most egregious kinds of errors.
The normal way I get specs is not via a drunk phone call (thank god) but via jira tickets that have been discussed and list concrete examples. I think this is pretty normal for many people.
I received training in Z and I balk at the idea of reading it. Though you dont seem to believe it, I can well believe that the gap between the English language spec and the formal spec is easily desynchronized and infested with bugs.
Specification "by example" is, in my experience, almost guaranteed to result in missed cases or unspecified behaviors in uncommon situations.
Why are you finding difficulty with that? Not having formal verification is an alternative to having a formal verification.
There ought to be a cost/benefit analysis applied to the tool - i.e. does the cost of writing and maintaining the formal specification pay for itself in terms of bugs caught. Does it have the potential to create new kinds of bugs? (I would argue yes).
The common belief is that it does bring value for certain types of code (rocket ships, maybe pacemakers? etc.), however very few people actually use it because for most applications a certain level of bugginess is perfectly fine. As a result, very few people actually have experience with it.
>Specification "by example" is, in my experience, almost guaranteed to result in missed cases or unspecified behaviors in uncommon situations.
Specification by example does mean missed cases, yes, but the missed cases will get caught by manual testers involved in the process of writing the examples, programmers while implementing the code or fuzz testing.
The dysfunctions I tend to see aren't edge case scenarios being missed altogether, but:
* Not involving programmers / testers who would spot the edge cases in the process of writing the examples. This is typically an organizational dysfunction.
* The programmer decides themselves what the correct behavior should be during edge cases without consulting the stakeholders.
* The PO/PM/Developers make poor decisions about overall architecture or intended edge case behavior. A large part of good system design involves constraining the number of inputs to a system so that the number of potential scenarios doesn't explode unmanageably.
The question I think formal verification has to answer is - does it actually bring any value if you are already doing all of those things or is it more of a performative ritual to ward off the bug spirits?
Luckily, a sound proof verification engine is feasible, so you are unlikely to have a "proof error" despite the proof "implementation" being so much larger. But, the fact that the specification is much larger than the implementation means there is more room for specification errors than implementation errors. The reason why you might still want a formal specification even if it is larger is that you can prove it and you can formally reason about the specification, goals, and interactions. It remains to be seen if we can invent a way to consistently make a formal specification simpler than the implementation which would be the holy grail as there would be no downsides.
One cool thing about formal verification is that you can not only prove things about your code, but you can prove things about the specification itself (with some approaches, at least). This includes proving arbitrary properties, proving the presence of bugs, proving the absence of bugs and in some cases, even proving full correctness of the specification.
> I'm bullish on more sophisticated type systems [...] but not formal verification.
I don't know what kind of formal verification framework you used that left you with this conclusion, but the more sophisticated is your type system, the closer you are to doing formal verification.
I've used plenty of type systems, and they have all provided a means to annotate the code and then prove certain properties about the code, but I have never in my life seen a type system which let me define a whole specification as formal verification does.
I have also seen type systems go waaaay overboard. They ended up inhibiting development velocity because they were so intent on forcing the programmer prove of the code properties that actually didn't need to be proven.
In general, I think type systems that try to strongly limit the scope of the properties they are trying to prove and apply a cost/benefit trade off to the value of the proven properties and the costs of the annotation work best.
Just as testing changes the way you structure your software, designing via formal methods changes the code that you produce as well, and it will attract a different set of people than traditional software dev, just as architecture attracts a different set of people than carpentry.
1. https://danq.me/2020/11/11/blink-and-marquee/#:~:text=Invent....
The formal specification for something like Redis is likely much more akin to your car bridge spec. And to continue your analogy, I imagine the specifications for big bridges (Golden Gate, etc) are much more thorough than the ones you built.
On the flip side, type systems bring at least some sense of proof into programming.
That seems like a weird conclusion to me.
You definitely can't write a "correct" program unless you know what you expect it to do. It's easier to write a specification than a program, because a specification is at a higher level of semantic abstraction.
Is it easier to write a correct specification that correct code? Yes, absolutely, because in a specification I can specify outcomes without having to say how they're achieved, and I can specify results that are invariant over time without having to say how they're maintained, etc.
A specification is essentially a bridge between, on the one hand, a higher-level requirements document that's probably imprecise and/or contradictory and/or incomplete and, on the other, code that has to be completely deterministic.
> [It's easier to write specifications than implementations because] in a specification I can specify outcomes without having to say how they're achieved
It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. This way, "correct" isn't a meaningful category, there's only "incorrect in retrospect". This is how most software is made and for most applications I would expect cost-benefit analysis to favor it.
assert(vector.is_empty());
It's even even easier to write a specification that says "if this case, do this; if that case, do that; otherwise, do whatever". Just use your proof language's implication symbol. (this ==> THIS) && (that ==> THAT), done.
Now that LLMs can write for-loops, too, I've hoped that the field will reconsider the activities that it considers to be valuable. The essential complexity is more about what you described: sit down, design, find a specification. The build to spec part, in the 21st century, can be a tooling step that takes the spec as input.
Perhaps the next step for the industry's state of the art in application-level software engineering is mastering formal spec languages, to seriously tailor the scope of work to the essential complexity of mediating between the agile world of human requirements and the formal world of computing systems. But I won't hold my breath--society is inured to software bugs as a fact of life, and programmers are used to being paid to endlessly patch their own mistakes.
It's been said that a sufficiently detailed spec already has a name: a program.
You could create a spec that would specify exactly what a program does, but generally speaking that would have no useful purpose.
For every program that does something, there are multiple ways to implement it. Often, different ways of implementing a program have different performance profiles, which is why many programs become more complex than the most naive way of implementing it.
A spec almost never specifies anything other than the simplest possible way that a program should be implemented (because when creating a spec, performance is irrelevant). This is usually way easier to make sure that it is correct than a spec that would specify exactly how a program should be implemented, including things done for performance.
Furthermore, you don't have to necessarily trust a specification. Specs can also be proven to have certain properties, i.e. they can be formally verified and proven to have absence of (perhaps certain classes of) bugs, and in some cases, can even be proved to have full correctness (yes, the spec itself, not just the program that implements it).
So I don't think it's fair to equate a program to a "sufficiently detailed spec", since most of those details are actually irrelevant (or at least, they should be, and can be proven to be) with regards to the correctness of a program.
Only a small fraction of software applications can be specified up-front. Most software is enterprise software, entertainment software, etc.; software that evolves, where a priori 100% specification is a fool's errand.
Things are out of specs all the time, and engineers have to deal with that all the time. It is even worse because while you can prove a program mathematically correct, reality only has a passing interest in mathematical correctness.
This is why I like end to end tests, UA testing, fuzzing, and property-based tests.
Having done it, I'm pretty sure you can. Why don't you think it can be done?
It requires a programming language (or language subset) with very well-defined semantics, and the use of theorem-proving tools but it's certainly possible.
And, for how many aspects? You can determine the absence of type problems; you can determine the absence of buffer overruns and use-after-free. Can you determine the absence of race conditions? Can you determine that it meets timing constraints with 100% certainty?
There are a huge number of different kinds of things that a specification could specify. I'm pretty sure that we can't formally verify all of them.
The programming language used had no dynamic allocation, so no use-after-free; and it was single-threaded so no race conditions. We did prove that there were no array indexing errors (i.e. buffer overruns). Recursion is also not permitted, so maximum call-stack depth is determined as well.
That is actually the easy part.
From my limited knowledge of formal verification (a university module decades ago and reading the occasional article since) it works very well for individual algorithms or small libraries, where the input ranges and desired outputs can be relatively easy to pin down with some accuracy and precision.
As soon as you are working on something bigger and hairier, even under ideal circumstances the effort to produce the spec becomes exorbitant. And those ideal circumstances include end users (or other stake-holders) who know exactly what they want from the start or at least can be convinced to workshop it (at their cost) until they have bottomed out exactly what they want. More often than not, what happens instead is a PoC is produced, either as wireframes or a fuller prototype, and essentially that PoC and the issues raised against it becomes a partial spec, inconsistencies & holes included. Once you start down that track, getting back towards something formally verifiable is likely harder than starting towards that point in the first place.
IMO formal verification, in an ideal world where you have effectively infinite time for doing things properly properly, or for smaller projects a large but not as infinite time, is the ideal. Unfortunately we don't usually work in an environment like that, so we have to compromise.
The high-water-mark, which is stuff like formal proof of correctness or proof of worst-case runtime, gets a lot of attention; but there are plenty of valuable approaches that are less expensive.
You can do, for example, formal proof of the absence of runtime exceptions (e.g. no bounds check violations), which doesn't require a formal specification and tends to result in a lot of theorems that are easy to prove automatically.
Or you can do data and information flow analysis, which will let you verify that you don't depend on uninitialized values of variables or make sure that your expectations about how different inputs to a program should affect outputs ("hey, why doesn't the weapon release discrete depend on the weight-on-wheels sensor?")
Quite a few design decisions (e.g. focus on classical reasoning support, focus of existing libraries) suggest that software verification of Lean programs isn't seen as a major application. (Of course you can always define a framework and prove stuff about C programs, like the "software foundations" book illustrates in Coq. But that's not really something new and again would need a lot of foundational work and tooling, essentially duplicating what people do with Coq, for no obvious benefit).
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.
I'm still in favor of formal proofs, but there are limits to what it can do.
(I probably got the parenthesis wrong on the original example)