Hacker News Reader

Comment by aseipp | Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com