Something seems wrong here. They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?

I can believe that it's possible to get the LLM to write proofs, but I can't believe there were zero bugs in the system they verified. I wonder if they got the theorems wrong, or if they only proved narrow properties of the system.

I've had Claude formally verify crypto and data storage formats. It wrote theorems that looked fine and the formal verification passed but the resulting code contained many, many bugs that other implementations of the same things found with ad hoc testing.

The way the announcement is written, we should expect zero bugs in libsignal moving forward, and I guess time will tell whether that happens or not.

▲

derefr 2 hours ago | parent | next [-]

> they only proved narrow properties of the system.

It's that, yes.

They didn't prove that the code has no bugs; they proved that none of the current bugs (known or unknown) are security-breaking bugs, per their formalized security model.

> First, our researchers collaborated with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every one. From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean, a computer language that mathematically proves the accuracy of code.

The generated Lean code here is just being checked against the "formal mathematical specifications of Signal's security goals", not checked for the low-level properties you might care about as a programmer, e.g. "will it ever leak memory" or "will it ever crash", etc. And in fact, the code is not even being checked for the reachability of non-security-violating protocol failure states, e.g. "could the protocol ever deadlock such that neither side can send messages any more".

It's still perfectly possible for the code to have all of these problems. It's now just known that, as of the commit they did this analysis against, none of those low-level problems, as far as they exist in the codebase, can cause a security-model violation.

Or, to put that another way: the system has been proven to "fail safe" in all its current failure modes, per their specific definition of safety (which is basically "keeping to the security guarantees Signal markets itself to users as having".)

▲

mentalgear 34 minutes ago | parent | next [-]

Note that this is about Signal’s cryptographic protocol, not the Signal App or the surrounding platform OS.

Proofing and securing those is the way larger attack vector and work to come.

▲

legitronics an hour ago | parent | prev [-]

Well I’m not even sure they did that. Not really.

They took signals security goals/aim/target and used models to generate a mathematical model. Which is a bit “hey trust us bro” in 3 ways but they did have human experts fully review 1 path, partially review 1 path, and the last I’m not really sure.

The fully reviewed path was that the aims goals were turned into positive mathematical statements “we will achieve X Y Z” so if we trust the humans that part should be as strong as we achieved X Y Z.

Tons of lean code generated to prove X Y Z correct, a lot of it is entirely self consistent. But then because it’s too much to look at we had the AI judge all of it for problem areas and we had humans look at that 1% of it… okay? That’s great if your magic box can pick out the problem areas but that wasn’t proved.

My last issue is, and please tell me if I’m wrong or missed something, but what says or proves the security goals/models are necessary and sufficient? We aim to do X Y Z. Great. We aim to not do A B C. not sure if I’m quibbling or this is strictly needed but it seems missing (unless it can be captured in entirely in the positive statement) let’s assume it’s included. We did X Y and Z, we did not do A B or C. Okay what’s my prize? Unbreakable crypto?

“Um well no… we know we can have X Y and Z while not having A B and C”

And so if we have X Y Z none of A B C we know the model is good.

“Yeah, probably”

And that the code at some point in time is no better than that?

“Yeah, certainly”

	▲	oggy 22 minutes ago \| parent [-]
		We may be able to say that X Y and Z are necessary since I can show you a concrete attack if you omit one. But we can never be absolutely certain that they're sufficient. Still, we've had something like 30-40 years of research by now looking at how to specify security properties. We certainly didn't get many things right the first time around. For the "basic" stuff, like confidentiality and authenticity we likely have a reasonably good grip on it under some, let's say "reasonable" assumptions. But a lot of research also still goes into developing notions of security with weaker assumptions or more exotic goals.

▲

cortesoft an hour ago | parent | prev | next [-]

This is true for all formal verification systems, though. You can only formally prove that code does what a spec says, you can’t verify that a spec perfectly matches what the code is intended to do.

▲

lubujackson 2 hours ago | parent | prev | next [-]

I guess we need to define what bugs are.

Software doesn't exist in a platonic state like formal mathematics, which at least can be consistent with all other results. Software interacts with the real world and "bugs" can be any number of security weaknesses like emitting useful timing signatures, buffer overflows that depend on the compiler used, weaknesses on certain hardware, etc.

It is great that Google has formalized code to some degree and for software that MUST be hardened, this may be valuable. It may be generally useful, but we need to get a feel for the gaps that inevitably will persist.

▲

SamuelAdams an hour ago | parent | prev | next [-]

This seems like a trivial thing to verify though, point it at a known software version with a CVE, like OpenSSL / Heartbleed, or some of the more recent SSL / PHP / Node / HTTP issues. Then you would expect it to find the Heartbleed vulnerability quite quickly. If it does not, investigate and iterate.

▲

amelius 28 minutes ago | parent | prev | next [-]

> They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?

Well, if it's SSH then I sure hope it has no LLM-discoverable bugs.

▲

fooker an hour ago | parent | prev | next [-]

You'd just move from bugs in code to bugs in the spec.

Real software needs mind blowingly complex specifications and while it's now fairly easy to get an AI generated proof that your code follows the spec, there's not much to help you with bugs in the spec.

AI will happily change the spec for you so the code verifies though, but that doesn't solve the trust issue.

Truly a trusting trust scenario.

▲

lilycarranza990 an hour ago | parent | prev [-]

Hey wanna tryna flip hundreds into thousands??