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”

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.

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.

I applaud them for starting with the protocol, because that can be generalized beyond any one specific implementation in principle, even if, in practice, we're somewhat limited to the official Signal apps given their centralized nature. Securing the applications themselves (perhaps starting with their implementations of the protocol, but the rest is also fair game) will inevitably be a bigger task.

I'm actually unclear on whether they just translated the design of the protocol to Lean, or translated the app's implementation of the protocol to Lean.

The wording of the article is a bit too ambiguous to say either way, I think? They just say they "generated" the Lean code; they didn't say what it was being generated from.

From this I think it's a given that they were talking about the implementation, not the specification

> To confirm that AlphaProof Code can tell correct code from buggy code, we reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases, the system produced a machine-checked proof that the buggy version was insecure.

is it just the protocol? Or is it also "the part of signal that implements the protocol", at least, yes it does what it's supposed to, with no weird timing collisions when multithreaded?

Also, I presume there are some unproved baked in assumptions about cryptographic primitives (e.g, but not necessarily, "sha512 has a uniform distribution")