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 4 hours ago | parent | next [-]

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.

	▲	inigyou 3 hours ago \| parent [-]
		There is a reason Mythos only found one bug in curl and it wasn't very bad.

▲

user3939382 5 hours ago | parent | prev [-]

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

▲

adrianN 5 hours ago | parent | next [-]

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 5 hours ago | parent | prev [-]

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.

▲

codebje 3 hours ago | parent | next [-]

There's lots of things to show for the research!

Part of what the research shows is that correctness-by-proof has a cost in developer effort.

If there really is a vulnerability-apocalypse due to AI, and it's not just a different flavour of AI hype, the cost of having insecure software will rise to the point that the cost of dealing with insecure or incorrect code at time of creation becomes less than the cost of ignoring it until it blows up.

I doubt it'll rise so much that we'll want to face the cost of behaviour proofs for much code at all, but it's quite possible it'll rise enough that we want to do things like prove that indices are in bounds, at compile time, so vector accesses can skip checks without compromising safety.

▲

crote 3 hours ago | parent | prev [-]

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?

	▲	jopsen an hour ago \| parent [-]
		The specification doesn't have to be. But yeah, writing specs is usually harder than reviewing the code 4 times :)