[cadamsdotcom]

Security through obscurity was never a great strategy.. and now it’s not a strategy at all..

Hopefully at the end of this decade, a ton of software practices have been overhauled to eliminate classes of problems. Memory-safe language use is a great start - but it’d be great to see innovation in checking for TOCTOU problems, improper/missing authn & authz, and many others.

This is an engineering problem. It won’t be solved by models that “only do dumb shit 1/10th as often, only 0.01% of the time now not 0.1%!” It won’t be solved by adding more models to do even more double-checking before and after the work. It won’t be solved by hoping humans catch it in review. It isn’t solvable by adding outer loops of any sort - though we may get close. To truly solve this will take serious CS research.

[whimblepop]

Almost never do software companies even attempt to design secure systems. I'm not sure this requires new fundamental research so much as slightly giving a shit.

[user3939382]

Verifying correctness of an implementation is P NP, not serious CS research.

[adrianN]

Most verification is undecidable, lots of it is pspace complete. That doesn’t mean very much in practice since those are worst case bounds. People regularly solve problems that are undecidable for all practical instances that they care about.

[bawolff]

Verifying behaviour of an arbitrary program is uncomputable. However that doesnt mean you can't have proofs of behaviour of specific programs you create.

Personally i have some doubts, a lot of research has gone into the idea without much to show for it, but its a very reasonable research area.

[crote]

I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?