That's consistent with my experience using them for coding, where even the best models mostly work by being persistently midwit (with infinite knowledge) more than individually brilliant.
Well, the report you're replying to doesn't make me so hopeful: "7349 findings made public, 217 (.5%) fixed"
If we want perfectly secure systems, then perhaps we don’t want universal and general purpose ones.
We cannot automatically and completely verify nontrivial semantic properties of arbitrary programs written in a Turing-complete language (Rice's theorem), but as long as we as humans can intuit correctness arguments for our programs, then formal methods will apply to it. Of course, declarative rather than imperative programming semantics tend to result in simpler correctness arguments, sidestepping reliance on global state and convoluted loop invariants.
I imagine it would be a nightmare to work with.
Maybe the digital equivalent of being locked in a doomsday bunker eating only white rice doesn't produce interesting software experiences.
A computer that isn’t connected to anything (make sure to disable Bluetooth and the microphone) is already safe. I bet eventually we’ll be able to serve static HTML pages safely eventually. Maybe not images. Font selections might have to be pretty restricted. But, at least we’ll have the useful part of the internet back.
Just get rid of the computer at that point.
There is. But it will only be reliable if every transitive dependency of your codebase, all the way down to the hardware level, has been formally verified. Failing that, you have to rely on opaque contracts at the boundaries, and those are just promises that may be mistaken.
The Halting problem, Rice's theorem, etc. only apply if your goal is to automatically deduce properties or their violations for arbitrary programs. If your goal is simply to prove correctness properties for well understood classes of programs in industry, then there are no fundamental obstructions.
They turned frontier models loose on PHP, and the big one they found was based on a previously know logic flaw that was extremely difficult to exploit. Which makes sense: hence the need for frontier models.
And in the wild, while there have been many attempts and a few simple demo successes, the practical impact has seemed to be small, seemingly constrained by the length of the chain and the diversity of PHP configs.
In short, it was indeed a major vulnerability, but not magic (in the Arthur C Clarke sense).
I think ultimately the fear comes down to: do you believe that code can be secured. I recognize that there is probably no objective way to deductively prove it because of the Halting Problem etc. But if one believes code can be constructed to operate to spec, then there must be a limit to the damage an LLM can do, even a very smart one.
I think we are going through a phase where a lot of known triaged code shortcomings will get exposed and hopefully fixed. Sucks while it is happening. But not actually the first round of this type of evolution. And ultimately I think as before, we will come out the other side with more secure and durable technology.