Now is the winter of our disclosure

CNBC has announced that this is “Black October”: according to Chris Krebs, 3% of all critical vulnerabilities ever found have been found in the last month. PHP2Shell was the big one last week, with an appropriately messy release. Details came out on the 20th, GitHub advisories went up early, and a bunch of people took their sites down.

Mostly, though, people didn’t get hacked. Cloudflare had seen millions of exploit attempts, but, as far as I know, we haven’t had any in-the-wild exploitations. Most of the damage has been self-inflicted with people hurriedly taking things off-line, and part of the reason is that these are really quite tricky bugs.

Roughly, my model of software is:

• Someone has an idea of what a program should do.
• They write a program that does that thing.
• A bug indicates a disagreement between the two.

Security is an unusual requirement: you may not have written it down anywhere but “don’t allow people to execute random code from my web service” is probably something you would agree with if asked.

Models are really good at finding differences between a spec/requirement and a piece of software. This feels like a bad moment for software because a lot of these implicit spec disagreements are security flaws. But, it’s a good moment for software for basically all other cases of spec/code mismatch.

Barron et al. at DeepMind recently published a paper describing bugs in cross-entropy and softmax in Jax and PyTorch. These are used approximately… everywhere, so that was surprising. But math gives us a known defined requirement for what these should do. CE’s gradient is q - p, both of which should sum to 1, so the gradient should sum to 0. In softmax, everyone subtracts the max logit for stability, but once the max logit is far enough ahead of the rest, rounding means the gradients don’t quite sum to 0. This causes a phenomenon known as slingshot(ing?), where Adam would lurch about in a surprising way. It’s a pretty edge-case-y bug, which is why it had existed for such a long time in the two frameworks used to build ~all models. But it was a bug!

We are in a potential golden age where anything that can be precisely specified can be systematically searched and tested against. The problem, of course, is that we don’t generally have those precise specs.

Recently, Matt pointed me at an interesting post from the PL group at Brown. A prompt like “write me a regex for dates” is sort of a spec, though not a very detailed one. Their PICK project has an LLM generate several implementations, and then find concrete examples where they disagree. The user then decides what they meant: yes to “10/26/2026”, no to “26/10/2026”, implicitly clarifying they want US-style month-first date ordering. The project isn’t trying to fix the regex, it’s trying to fix the spec.

This general idea, of elucidating increasingly refined specs, works because generating implementations is cheap now. You can envisage applying the same thing to existing software: identify a spec from a piece of software, generate some implementations and get the user’s feedback on outputs that highlight differences between them.

The first part has been tried: Anthropic’s recent red teaming effort did agentic property-testing on some popular packages by inferring properties, writing Hypothesis tests and triaging. But, only about 56% of the identified reports were valid.

You can only get so far inferring the spec from the software. You have to understand the human intent as well, which is exactly what PICK is getting at.

When you do have the right spec, you can leverage the kind of formal verification tools people have been talking about for a while. Michael Daniel, who used to be a cybersecurity coordinator in the Obama administration, suggested that:

We’re going to turn these AI tools on software that hasn’t been deployed yet, so one would hope we start to deploy software that has fewer vulnerabilities to begin with. You burn out all the old stuff, and it makes way for new growth that’s more secure from the beginning.

Which is a good thought! But! We do still have to work out exactly what we actually want everything to do when it grows back.

1. On numpy it found numpy.random.wald sometimes returns negative numbers, which is now patched.