Hacker News Reader

> Today, we are starting to bridge the gap between pen and paper proofs and computer science: it is called formal verification.

I was involved in formal verification at UC Davis back in 1993, and I'm sure it started before that. And yet we still can't do it effectively all these years later. The language lab was using HOL (higher order logic), us security geeks were using BAN (Burrows-Abadi-Needham logic). BAN logic turned out to have problems and GNY logic was supposed to fix those, but it had problems too... all those logics were failing us in edge cases that we could hardly conceive of. No matter how precise things were specified, no matter how rigorous things were, there were always edge cases that could be pried open to present practical attacks. What I eventually took away from it is that even the smartest humans aren't actually smart enough.

Rogaway was one of the smartest people I ever met. The fact that OCB2, proven secure, had a gaping hole discovered in 2018 doesn't leave me much hope that we'll ever have proveably secure anything.

A related answer that I posted back in 2009 to the question of "How do you fix a bug you can't replicate?"

https://stackoverflow.com/a/1268464/59087

I have absolutely asked users to give me an rr[0] trace of my program when there was an issue. I'm honestly considering shipping it in an embedded (not in the lightweight sense) project at work so that if any problems arise I can easily debug it away from it.

[0]: https://rr-project.org/

In modern world, bugs find you.

I don't find bugs - I write them. ;-)

Meaningful engagement is the key for a successful bug hunt!

Zoinks, mister

How do people find bugs?