Top
Best
New

Posted by ilreb 4 hours ago

AlphaProof Code(deepmind.google)
358 points | 125 commentspage 4
p-e-w 3 hours ago|
It’s nothing short of amazing that a huge codebase like Signal’s is apparently not only secure in a practical sense, but secure even in a strict formal sense. The people who wrote the Signal code must be engineers of the highest caliber.
Gasp0de 3 hours ago||
This didn't verify the Signal app, only the signal encryption protocol
throawayonthe 2 hours ago||
still a big codebase: https://github.com/signalapp/libsignal
Aboutplants 3 hours ago|||
Yeah quite impressive.
milkshakes 3 hours ago|||
the crypto might be secure; i wouldn't be so sure about the rest of the code.
hoppp 3 hours ago||
And it's never the crypto that breaks, it's usually something else.

E.g : Pegasus spyware don't break whatsapp crypto either

lifeisloving 3 hours ago||
Well the NSA is probably decent at building software. But none of this really matters if the OS isnt secure and the OS is much more complex and less verifiable. Also, why does the government use their own versions of Signal that are more secure, makes you wonder.

Im sure they allow bugs that benefit the NSA.

https://www.malwarebytes.com/blog/bugs/2026/10/signal-bug-co...

Downvote me, but yes I believe that Signal and the EFF are US military programs larping as civilian institutions.

psd1 3 hours ago|||
White-listing contacts would have prevented the gaffe when a journalist was added to a war planning group
SiempreViernes 3 hours ago||
Would it? As I remember the journalist's number was added to an existing contact by some smart feature in iOS, not sure how a whitelist would help there.
booty 3 hours ago|||

    Well the NSA is probably decent at building software. 
Ultimately I'm sure they are but my secondhand understanding from friends is that it's difficult for the US gov't to attract and retain software engineering talent.

It's not just total compensation. Working on classified stuff can be a bit of a career killer, since you can't talk about your past work when looking for a new job.

Plus there's the antipathy toward the current Trump administration, and the general moral unwillingness of many to do defense-related work in general.

Also, last I heard, cannabis use was still a disqualifier for DoD work and/or various security clearances. There are periodic ongoing polygraph tests, not sure about ongoing piss tests. The government is big; I'm sure the exact policies differ from department to department. But this turns a lot of people off.

Of course, every single thing I've said above might also be viewed as a positive by some engineers. Maybe they attract enough "true believers" to more than make up for the other factors.

lifeisloving 2 hours ago||
I would argue that US intelligence, especially on the technical side of things has put emphasis on privatization of these sectors.

US intelligence knows they can't go to policy makers and get funding for billion dollar domestic spy programs. So they stand up private companies and give them smallish grants at the beginning to get them on their feet, i.e Flock, Palantir, Signal Foundation, EFF, cloudflare, oracle. I could go on and on about orgs that their start off the back of US intelligence, whether through direct funding or through their alumni network.

The US Department of Defense has a long tradition of private public partnerships, but the privatization of intelligence has been accelerated in the last decade.

So while the NSA might not be able to attract talented SWEs for gov salaries to work on defense, their vendors that owe them their existence can.

booty 1 hour ago||
That's a great insight!
Computer0 3 hours ago||
I'm pleased to read Signal looks good to our robot mindlords.
dmead 2 hours ago||
did the formal proofs for the haskell compiler stop bugs from happening?
fHr 1 hour ago||
holy shit
yasirkhan001 27 minutes ago||
[flagged]