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.
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.
There is a reason Mythos only found one bug in curl and it wasn't very bad.
Regulation and an ethics/licensing board à la Engineers would probably be a good start. If management knows they can’t tell you to do a bad or sloppy job because no one in your industry worth a damn will… everyone wins.
I just see unintended (but easily imaginable) consequences that don't fix anything.
Especially since the world isn't Dilbert where your boss goes "oh, authz? lol nah, just yolo it" and you go "dangit, alright boss". Instead, security requires eternal vigilance and zero missteps along the thousands a project takes in its lifetime.
I think there's a reason HNers who pitch this idea never give any concrete examples of entailments of their proposal: it doesn't even sound good superficially. e.g. How this actually changes security issues. In fact it just sounds even more convenient to blame engineers.
Yes. People don't seem to understand is that if we build our tools and libraries with models that do random dumb stuff 0.01% of the time, those bugs and leaky abstractions bubble up and grow exponentially into errors and undependable behavior.
People have been doing great research with formal methods, dependent types etc. Disciplining ourselves to truly write and understand code, using the best in math and PL theory (FP and type theory etc) is the only way forward in my opinion. We have to make correctness a value and goal, or else we will keep spinning off into psychosis and the corruption of truth.
Verifying correctness of an implementation is P NP, not serious CS research.
Rust's safety guarantees are also undecidable on an arbitrary program, but Rust still proves them for safe rust code. Why so? Because safe rust code is not an arbitrary program, it is specifically forbidden from doing some things, which becomes a pain in the ass sometimes for a coder, but the result is a subset of programs you can prove safety guarantees for.
The issue is how to design a language that restricts programmers in a way you can prove everything you care for on their programs, and still don't make life of programmers unbearably difficult, because the language allows them nothing.
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.
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.
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.
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?
The specification doesn't have to be.
But yeah, writing specs is usually harder than reviewing the code 4 times :)
It kinda does.
See WPA2 KRACK, you could've had a formally verified WPA2 implementation and it still would've been exploitable because the flaw was the specification itself.
Moving the problem one layer up is the desired outcome because it makes exploitation much more difficult. Your attack surface becomes much smaller.
It might just mean the opposite. Unergonomic and/or slow memory safe languages might not be needed anymore at some point, because LLM can check for reasonable programming patterns and can do some amount of vulnerability checking upfront. But seriously the first point -- as long as you keep to a known set of reasonable patterns (much larger set than the sets accepted by restrictive and cumbersome type systems), memory unsafe languages are actually pretty safe, and the code remains easy to understand, easy to maintain, and performant.
Already today, in my experience, widespread models like Claude 4.6 or 4.8 can quite reliably find some concurrency bugs that are easily missed by humans.
> can reliably find some
Some.
In software & in security, 99% is a failing grade.
So is 99.99%, so is 99.999%, and any other amount less than 100%. It’s not enough to point 5 LLMs at it and it’s not enough to point 500 LLMs at it.
The field needs to seek deterministic & comprehensive solutions to whole problem classes.
Okay, so the whole world is failing and success doesn't exist.
Maybe now you need a better criteria than your previous failure / success_100%_infiniteCost to observe and understand the the world
This logic enables and encourages corruption in all spheres of life. "Things are messed up as they are, so why try so hard to do the right thing?" "Let's be realistic."
The logic allows that to continue because "good" and "better" isn't good enough, only "perfect" is allowed, so instead "nothing" is done
It's not as black and white as you claim. 99% is obviously much better than 0%, and 99.999% would be an exceptional, unheard-of improvement. In most software projects, this would find ALL bugs.
And most "memory safe" languages are not all that memory safe. Or they need escape hooks.
EDIT: To be clear it's not AT ALL black and white. You have drunken too much of the type safety kool-aid.