Hacker News Reader

Comment by tachyonbeam | Hacker News Reader

I'm kind of skeptical of formal verification. For instance, it wouldn't have prevented bugs like spectre or meltdown. It can only tell you that your implementation matches some spec, but your spec can still be incomplete or buggy. At the end of the day, there's no substitute for extensive real-world testing.

View on HN

This is such a funny post because formal verification techniques tend to see a lot of success in the hardware world, from lightweight ones to heavy ones, much more so than software, because many behaviors can be bounded over some finite amount of time (or inductively proven over all time, or equivalence checking, etc), and because hardware designs have massive incentives to get it right the first time and not blow a billion dollars on a mistake.

If you write the basic cookie cutter "but but but, it's all just a spec, so we can't ever know anything!!!" it should be a requirement to submit a 5 page essay describing the algorithms/theory behind formal verification techniques, so they can prove they understand them, as opposed to only "understanding" how to make cookie-cutter bait posts.

Ouch. Don’t be so harsh. Your point is valid: specification bugs are definitely important to prevent. But OP question is also valid: what about sub-specification bugs?

No need to roast him.

GGP's post is classic HN middlebrow. Clearly someone who "knows what's best" for HW, but has never been involved in a major HW product, ever.

Serious production HW is formal all over. GGP's opinion is sort of like going to Google's search-engine group and saying that internet connectivity is a bad idea because it'll never fully capture human emotion. It's not even wrong.

My partner did hardware stuff. I couldn't BELEIVE how much time they spent in verification space (and how annoying it seemed and retro the tooling appeared!). Much different than programming where I can iterate 100x per day.

verification is not always formal, though - it's often "fuzz testing" (I have done this).

The most intimidating debugging scenario I've ever heard described was a physical register leak in a renamer.

I mean, strictly speaking that's just ('just') a memory leak, but still, yikes.

It's almost always done to argue for testing, too. But the point of verification as an engineering tool was never to replace testing, but to focus it. (Just like the point of a mathematical proof is not to offer 100% proof of the truth of a statement, but to reduce its truth to the truth of some other statement---usually "ZF holds".)

So you do some formal verification, good. But you still need to: - validate your model; and - validate your assumptions. This would always have to be done, but the fact that GP did not think about it means that, in the case of testing, it's not done. It's just "extensive testing", perhaps with some metric if we're lucky. Never "what are we testing for, and under what circumstances". (Except in places---aerospace, hardware---that welcome formal verification.)

Now, why does the above rant matter? Because GP is advocating the use of testing for a security property. Writing that test means you suspect there's something iffy that can happen with speculation. And if you know something iffy can happen, you can figure out what's not iffy and make that your spec for formal verification. You then get a proof that only the good (secure) behaviour takes place under clear assumptions, instead of getting the guarantee that none of the bad behaviours are exercised by your test suite.

> You then get a proof that only the good (secure) behaviour takes place under clear assumptions, instead of getting the guarantee that none of the bad behaviours are exercised by your test suite.

An important point, and something people often get wrong when they mistakenly believe that they understand the basics of formal methods.

Here's an old quote about Sel4:

> The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.

The and nothing more part is vital. Not only are there no unexpected additional features, there are also no unexpected additional vulnerabilities. More precisely, if there are any vulnerabilities, they must either be in the spec, or be side-channel issues. Formal methods aren't very helpful against side-channel issues.

Code Complete gets into the idea that you want multiple testing methods since they tend to have complementary coverage

Reducing bugs to the spec has the same benefits as Rust reducing memory safety bugs to unsafe blocks

& to your point: Spectre & Meltdown took decades for real world testing to unearth. So now that we know them, it'd be nice to come up with a formalization in the spec to address observable information leaks so that future chips have reduced attack surface in the space of spec implementations

It's hard to prove you're safe from novel threats, but let's not let that stop us from proving we're safe from old tricks

Fair enough.

Spectre and Meltdown were sort of identified in the 90s in a paper by a researcher funded by the... (IIRC) NSA. Make of that what you will.

I'm not sure we're going to see formal proof totally replace standard verification any time soon however when combined with more traditional verification techniques it's very effective. It can find interesting bugs very quickly that other methods may have taken significant cycles to find. As it approaches the problem very differently you get a different set of bugs found from it. It's also great for early bring-up work. With a handful of constraints you can start looking at least some aspects of design behaviour without needing an extensive testbench. When I was working on L1 memory system design at arm I used formal tooling extensively to bring up parts of the memory system before the full testbench was available.

You may start to see formal only verification on smaller/simpler blocks. E.g. imagine some bus adapter, with a decent set of formal properties that specify the bus functionality you may have to do very little work to verify it with formal tools.

There's also the use of SVAs within standard verification. This isn't formal verification but if you've done any formal work you end up with a bunch of new checks you can run in your standard verification flows too, again finding bugs more quickly. You can get nice feedback between the two, develop constraints to enable formal testing, those constraints become assertions in some other verification flow, it finds a violation of the constraint, you realise it needs adapting to cover some extra behaviour and your formal environment is improved (in effect you've found your spec bug).

View it as another tool in the toolbox, one that is becoming every more necessary as hardware designs become ever more complex.

> I'm kind of skeptical of formal verification.

This doesn't stand up. In the software world, both the Sel4 [0] and CompCert [1] projects have surprised researchers unaccustomed to encountering bug-free software. The non-verified alternatives to both systems were always found to be buggy.

For an interesting case-study on the use of formal methods, and their effectiveness, take a look at [2].

> your spec can still be incomplete or buggy

Spec bugs are possible, but empirically they're much less of a problem than ordinary implementation bugs. [2] has good discussion of this topic.

> At the end of the day, there's no substitute for extensive real-world testing.

That's backward. Testing is no substitute for formal methods. Testing is never exhaustive.

I don't think formal methods are often used in the complete absence of testing.

[0] https://www.newscientist.com/article/mg22730392-600-unhackab...

[1] https://compcert.org/motivations.html

[2] https://www.adacore.com/tokeneer

Formal verification catches a lot of bugs, some of which won't be caught by usual testing. It's still valuable even if it doesn't catch all bugs. I just think it as a more efficient way to run exhaustive testing.

This is the hardware equivalent of pretending javascript is fine because having types won't stop all bugs.

While it is true that formal methods, despite being able to prevent Spectre/Meltdown, didn't because someone had to think of the issue before proving it doesn't happen, the goal of formal methods is not to prevent all bad things. It is to prevent some bad things. Would you say that you're skeptical of tests because they haven't prevented many bugs, including Spectre/Meltdown, and therefore we shouldn't test?

The only relevant question is, are formal methods effective -- cost/benefit-wise -- in finding problems. Now there's a wide range of formal methods to the point that speaking about all of them as a single category is often not helpful, but the answer to this question is absolutely yes, in the sense that many formal methods have been found to be a very effective quality-assurance measure in many circumstances.

It's one tool of many. Microsoft used it to catch an error in the design of the memory controller in the XBox360 before launch. They also use it in the design of the consistency levels in CosmosDB which are tied directly to their SLAs. Hardware has a high turn-around time between iterations so being able to understand the design more clearly and catch errors earlier is a great investment.

Reply on news.ycombinator.com