I'm waiting for someone to build an implementation of Tor in a proof-verifiable language.
That would be pretty cool, since anyone could prove source correctness automatically.
That would be pretty cool, since anyone could prove source correctness automatically.
Tor has failed its users because the idea of running a public Tor cloud with volunteer entry, onion, and exit nodes is ludicrous. It means that the entire network is under surveillance all the time, the exact opposite of what you want. There has been widespread confirmation that the data you transfer via the public Tor cloud is being passively surveilled at the endpoints and actively modified when you, for example, download software. This makes it incredibly dangerous to use, likely more dangerous than just using the regular internet.
There are many other problems (like the fact that .onion sites are a dirty hack and likely have many undiscovered weaknesses like the ones CMU found) but nearly all of them are either deployment or architectural issues, not code security issues.
Like you said, Tor has architectural issues. Tor would be fine if it were low-profile, but it's not, and that's a major part of why the architecture is breaking down - it doesn't scale well with increasing users/publicity/nation-state-interest.
For example, side channel attacks. A classic attack on computerized cryptography. I don't know of any proof language that can protect against side channel attacks.
If you look online there are a few lists of tor attacks. The attacks include: snooping on exit relays, application issues, traffic correlation, website fingerprinting, congestion attacks, blocking tor access (declining to extend). Most of these are issues in the design of the tor system, not something I think source code proof systems are capable of preventing.