this post was submitted on 09 Aug 2024
200 points (97.6% liked)
Technology
59588 readers
3097 users here now
This is a most excellent place for technology news and articles.
Our Rules
- Follow the lemmy.world rules.
- Only tech related content.
- Be excellent to each another!
- Mod approved content bots can post up to 10 articles per day.
- Threads asking for personal tech support may be deleted.
- Politics threads may be removed.
- No memes allowed as posts, OK to post as comments.
- Only approved bots from the list below, to ask if your bot can be added please contact us.
- Check for duplicates before posting, duplicates may be removed
Approved Bots
founded 1 year ago
MODERATORS
you are viewing a single comment's thread
view the rest of the comments
view the rest of the comments
On that level it usually falls on computer scientists. Formal methods can prove that any implementation is correct, but proving the absence of unintended attacks is a lot harder.
Needham-Schroeder comes to mind as an example from back when I was studying the things.
And not a single one has been able to analyze the encryption in all these years? Fact is, Telegram is the tool the Russian opposition and even Ukrainians use to communicate without Putin being able to infiltrate.
No. It kind of falls on Dijkstra's old statement. "Testing can only prove the presence, not absence of bugs."
You can prove logical correctness of code, but an abstract thing such as "is there an unknown weakness" is a bit harder to prove. The tricky part is coming up with the correct constraints to prove.
Security researchers tend to be on the testing side of things.
A notable example is how DES got its mixers changed between proposal and standardisation. The belief at the time was that the new mixers had some unknown backdoor for the NSA. AFAIK, it has never been proven.