7 ms·

Why fuzzing over formal verification?

65 points by rrampage 3y ago

voxl 3y ago
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. Only a small group of software engineers are interested in this principled approach. Hell many software engineers are scared of recursion.
- sabas123 3y ago
  You can also write a formal spec based on a reference. But it will be harder then doing it up front most likely.
- seeknotfind 3y ago
  It's not just that they are afraid. No one has succeeded in building production-level systems at scale purely using "formal methods". There are a variety of ways to measure how a system compares to a spec. For instance, you can measure throughput at various points in a system. However, formal methods are much more detailed, and when they are applied today, it's usually within a limited context as a way to verify or do model checking.
  - colordrops 3y ago
    Right, the tradeoff in time/resources for doing upfront formal verification vs fixing bugs after they are found is almost never worth it. Formal verification isn't even used for most aerospace software.
- quatrefoil 3y ago
  That's a pretty cynical take. I think a more profound problem is that formal specifications for software are fairly intractable. 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...
  - pydry 3y ago
    My experience with formal specifications was that our specification ended up being more complex than the code itself. 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.
    - AnimalMuppet 3y ago
      First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. 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?
      - NovemberWhiskey 3y ago
        >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
        pfdietz 3y ago
        Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
- asplake 3y ago
  There is a sense also of merely moving the problem. If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. On the flip side, type systems bring at least some sense of proof into programming.
  - NovemberWhiskey 3y ago
    >If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. 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.
    - AnimalMuppet 3y ago
      You slightly dodged the question. Is it easier to write a correct specification? But I think the answer is still yes, and still because it's at a higher level of abstraction. There are more details to specify in a program, and there can be bugs in that.
      - NovemberWhiskey 3y ago
        I don't think I did dodge the question. 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.
        staunton 3y ago
        I agree with you but still want to play devil's advocate regarding you argument: > [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.
- odyssey7 3y ago
  Application-level software engineering hasn't been about hand-writing for-loops for a long time, but there's a tendency for people to feel self-satisfied in what's familiar and what they worked hard to master. 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.
  - knome 3y ago
    >can be a tooling step that takes the spec as input It's been said that a sufficiently detailed spec already has a name: a program.
    - odyssey7 3y ago
      Sure, but that's just wordplay. There are genuine, meaningful differences between technologies. Professionals should be able to weigh and consider them in various contexts.
    - someplaceguy 3y ago
      > 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.
- pphysch 3y ago
  > Only a small group of software engineers are interested in this principled approach. 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.
  - thfuran 3y ago
    That the spec can change over time just means you'll change the spec, not that you shouldn't or can't have one.
    - pphysch 3y ago
      In practice, software development methodologies that rely heavily on a complete spec (formal verification, 100% test coverage, pure programming, etc) do not perform well when the spec changes underneath them. It's doable but requires enormous resources and is almost never economical unless you're NASA.
- GuB-42 3y ago
  Traditional engineering is a lot messier than you make it look. 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.
jgalt212 3y ago
The spec may be provably perfect, but how to you prove the code perfectly conforms to the spec? I don't think you can. This is why I like end to end tests, UA testing, fuzzing, and property-based tests.
- NovemberWhiskey 3y ago
  >I don't think you can. 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.
  - AnimalMuppet 3y ago
    You've done it? For how big a program? 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.
    - NovemberWhiskey 3y ago
      Proof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. 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.
- jsenn 3y ago
  Some spec based systems allow you to refine a high-level spec until it’s detailed enough to generate code from, where each refinement can be proved correct [1]. I doubt this is done much, but it is possible. [1] eg https://en.m.wikipedia.org/wiki/B-Method https://en.m.wikipedia.org/wiki/B-Method
dgacmu 3y ago
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). Fuzzing is much easier to add to an existing system - though even there, there's a lot of benefit from designing for testability.
- rurban 3y ago
  Sorry, the state of the art of formal verification is proving C, C++ or Java code directly. Everything else is lost in translation. You just to mark some variables as symbolized and bound the loops. cbmc
  - dgacmu 3y ago
    Not really. Cbmc is really cool but it doesn't lead to the kind of high level proof refinement that lets you say things like "this low level code correctly implements the paxos protocol". 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.
pfdietz 3y ago
Fuzzing vs. formal methods feels like another example of The Bitter Lesson.
danielvf 3y ago
Some context on this article. 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.)
ykonstant 3y ago
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.
- aSanchezStern 3y ago
  Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in this metatheory without also allowing for program verification. Maybe you're talking about gaining support for formal verification of code not written in Lean? Like, being able to verify C? In that case, it's actually just a library issue. Nothing needs to be changed about the core Lean language, someone just needs to formalize the semantics of the target language semantics in Lean, and then add a verified compiler and verified extraction if you want to make the guarantees extend directly to the compiled assembly. Fuzzers have actually combined well with theorem proving in these kinds of tools in the past; Coq, the proof assistant that heavily inspired Lean and has been in constant use since the mid 80's, has a library QuickChick (based on QuickCheck from the Haskell world) which takes an arbitrary property and generates test inputs to test it, and has very mature support for extending it with new datatypes and invariants.
  - ykonstant 3y ago
    Lean allows formal verification, but it does not make it easy. As staunton remarked, the devs are focusing on classical mathematics, and the ergonomics for verifying code are currently horrible. I do suspect this will change with time, though.
- staunton 3y ago
  Why do you name Lean here as opposed to the other provers? Lean is "the new shiny thing" but my impression is that the community sees its focus in math, not so much software verification. 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).
bluGill 3y ago
int Mid = (high + low) / 2; 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.
- temac 3y ago
  You don't model an unconstrained "int Mid = high + low / 2;" line of e.g. C code with the math equation "Mid = high + low / 2". There are limits but this is a poor example.
  - bluGill 3y ago
    This is a real world example. Code that was proved decades ago and worked has started failing now as computers are able to handle in memory datasets that large. (I probably got the parenthesis wrong on the original example)
- weinzierl 3y ago
  I don't know much about formal verification, but I had expected that it considers the most basic behaviour of the most basic data types we have at the very least. Integer overflow as one of wrap-around, saturation or invalid state (UB in the real world) is a bar so low that I do not know what formal verification that doesn't consider it would be useful for all.
nanolith 3y ago
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. 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/presentation/cremers https://www.usenix.org/conference/usenixsecurity20/presentat... These tools are defense in depth for design. None of them are complete on their own.

65 points by rrampage 3y ago

voxl 3y ago

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. Only a small group of software engineers are interested in this principled approach. Hell many software engineers are scared of recursion.

sabas123 3y ago
You can also write a formal spec based on a reference. But it will be harder then doing it up front most likely.
seeknotfind 3y ago
It's not just that they are afraid. No one has succeeded in building production-level systems at scale purely using "formal methods". There are a variety of ways to measure how a system compares to a spec. For instance, you can measure throughput at various points in a system. However, formal methods are much more detailed, and when they are applied today, it's usually within a limited context as a way to verify or do model checking.
- colordrops 3y ago
  Right, the tradeoff in time/resources for doing upfront formal verification vs fixing bugs after they are found is almost never worth it. Formal verification isn't even used for most aerospace software.
quatrefoil 3y ago
That's a pretty cynical take. I think a more profound problem is that formal specifications for software are fairly intractable. 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...
- pydry 3y ago
  My experience with formal specifications was that our specification ended up being more complex than the code itself. 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.
  - AnimalMuppet 3y ago
    First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. 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?
    - NovemberWhiskey 3y ago
      >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
      - pfdietz 3y ago
        Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
asplake 3y ago
There is a sense also of merely moving the problem. If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. On the flip side, type systems bring at least some sense of proof into programming.
- NovemberWhiskey 3y ago
  >If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. 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.
  - AnimalMuppet 3y ago
    You slightly dodged the question. Is it easier to write a correct specification? But I think the answer is still yes, and still because it's at a higher level of abstraction. There are more details to specify in a program, and there can be bugs in that.
    - NovemberWhiskey 3y ago
      I don't think I did dodge the question. 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.
      - staunton 3y ago
        I agree with you but still want to play devil's advocate regarding you argument: > [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.
odyssey7 3y ago
Application-level software engineering hasn't been about hand-writing for-loops for a long time, but there's a tendency for people to feel self-satisfied in what's familiar and what they worked hard to master. 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.
- knome 3y ago
  >can be a tooling step that takes the spec as input It's been said that a sufficiently detailed spec already has a name: a program.
  - odyssey7 3y ago
    Sure, but that's just wordplay. There are genuine, meaningful differences between technologies. Professionals should be able to weigh and consider them in various contexts.
  - someplaceguy 3y ago
    > 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.
pphysch 3y ago
> Only a small group of software engineers are interested in this principled approach. 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.
- thfuran 3y ago
  That the spec can change over time just means you'll change the spec, not that you shouldn't or can't have one.
  - pphysch 3y ago
    In practice, software development methodologies that rely heavily on a complete spec (formal verification, 100% test coverage, pure programming, etc) do not perform well when the spec changes underneath them. It's doable but requires enormous resources and is almost never economical unless you're NASA.
GuB-42 3y ago
Traditional engineering is a lot messier than you make it look. 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.

jgalt212 3y ago

The spec may be provably perfect, but how to you prove the code perfectly conforms to the spec? I don't think you can. This is why I like end to end tests, UA testing, fuzzing, and property-based tests.

NovemberWhiskey 3y ago
>I don't think you can. 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.
- AnimalMuppet 3y ago
  You've done it? For how big a program? 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.
  - NovemberWhiskey 3y ago
    Proof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. 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.
jsenn 3y ago
Some spec based systems allow you to refine a high-level spec until it’s detailed enough to generate code from, where each refinement can be proved correct [1]. I doubt this is done much, but it is possible. [1] eg https://en.m.wikipedia.org/wiki/B-Method https://en.m.wikipedia.org/wiki/B-Method

dgacmu 3y ago

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). Fuzzing is much easier to add to an existing system - though even there, there's a lot of benefit from designing for testability.

rurban 3y ago
Sorry, the state of the art of formal verification is proving C, C++ or Java code directly. Everything else is lost in translation. You just to mark some variables as symbolized and bound the loops. cbmc
- dgacmu 3y ago
  Not really. Cbmc is really cool but it doesn't lead to the kind of high level proof refinement that lets you say things like "this low level code correctly implements the paxos protocol". 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.

pfdietz 3y ago

Fuzzing vs. formal methods feels like another example of The Bitter Lesson.

danielvf 3y ago

Some context on this article. 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.)

ykonstant 3y ago

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.

aSanchezStern 3y ago
Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in this metatheory without also allowing for program verification. Maybe you're talking about gaining support for formal verification of code not written in Lean? Like, being able to verify C? In that case, it's actually just a library issue. Nothing needs to be changed about the core Lean language, someone just needs to formalize the semantics of the target language semantics in Lean, and then add a verified compiler and verified extraction if you want to make the guarantees extend directly to the compiled assembly. Fuzzers have actually combined well with theorem proving in these kinds of tools in the past; Coq, the proof assistant that heavily inspired Lean and has been in constant use since the mid 80's, has a library QuickChick (based on QuickCheck from the Haskell world) which takes an arbitrary property and generates test inputs to test it, and has very mature support for extending it with new datatypes and invariants.
- ykonstant 3y ago
  Lean allows formal verification, but it does not make it easy. As staunton remarked, the devs are focusing on classical mathematics, and the ergonomics for verifying code are currently horrible. I do suspect this will change with time, though.
staunton 3y ago
Why do you name Lean here as opposed to the other provers? Lean is "the new shiny thing" but my impression is that the community sees its focus in math, not so much software verification. 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).

bluGill 3y ago

int Mid = (high + low) / 2; 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.

temac 3y ago
You don't model an unconstrained "int Mid = high + low / 2;" line of e.g. C code with the math equation "Mid = high + low / 2". There are limits but this is a poor example.
- bluGill 3y ago
  This is a real world example. Code that was proved decades ago and worked has started failing now as computers are able to handle in memory datasets that large. (I probably got the parenthesis wrong on the original example)
weinzierl 3y ago
I don't know much about formal verification, but I had expected that it considers the most basic behaviour of the most basic data types we have at the very least. Integer overflow as one of wrap-around, saturation or invalid state (UB in the real world) is a bar so low that I do not know what formal verification that doesn't consider it would be useful for all.

nanolith 3y ago

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. 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/presentation/cremers https://www.usenix.org/conference/usenixsecurity20/presentat... These tools are defense in depth for design. None of them are complete on their own.