4 ms·

The clients are all open source, so you can compile the code on your own machine.

by slondr 6y ago

adsharma 6y ago
Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation. This is why it's important to have them in the same code base. I've heard about attempts at inria to implement signal/double ratchet using F-star and verify the correctness. But no such implementation seems to be publicly available. One of the things I'm interested in is to see if it's possible to bring these verification technologies to more mainstream programming languages such as python. https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_signal.py https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_... is something I'd love to verify.
- eitland 6y ago
  > Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation. FWIW, not exactly the same but related: Telegram releases verifiable builds in both Play Store and App Store. AFAIK they are pretty much alone among mainstream IM services to offer this. See: https://core.telegram.org/reproducible-builds https://core.telegram.org/reproducible-builds
  - dbrgn 6y ago
    Threema offers reproducible builds as well, for the Android app: https://threema.ch/en/open-source/reproducible-builds https://threema.ch/en/open-source/reproducible-builds Signal too: https://github.com/signalapp/Signal-Android/blob/master/reproducible-builds/README.md https://github.com/signalapp/Signal-Android/blob/master/repr... Regarding the iOS app store, Telegram writes: > As things stand now, you'll need a jailbroken device, at least 1,5 hours and approximately 90GB of free space to properly set up a virtual machine for the verification process. https://core.telegram.org/reproducible-builds#reproducible-builds-for-ios https://core.telegram.org/reproducible-builds#reproducible-b... It's a manual process within a new VM. I wouldn't be surprised if it frequently breaks without anyone noticing. But at least they're trying, I'm not aware of any better approach. Apple's GUI-focussed approach doesn't make these things easy.
akvadrako 6y ago
Can you really compile them? If you look at the iOS repo, first there is no license associated with the repo. Second, there are lots of people reporting failed builds in the issue tracker without a response. https://github.com/TelegramMessenger/Telegram-iOS https://github.com/TelegramMessenger/Telegram-iOS https://github.com/TelegramMessenger/Telegram-iOS/issues/377 https://github.com/TelegramMessenger/Telegram-iOS/issues/377

The clients are all open source, so you can compile the code on your own machine.

by slondr 6y ago

The clients are all open source, so you can compile the code on your own machine.

Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation. This is why it's important to have them in the same code base. I've heard about attempts at inria to implement signal/double ratchet using F-star and verify the correctness. But no such implementation seems to be publicly available. One of the things I'm interested in is to see if it's possible to bring these verification technologies to more mainstream programming languages such as python. https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_signal.py https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_... is something I'd love to verify.

eitland 6y ago
> Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation. FWIW, not exactly the same but related: Telegram releases verifiable builds in both Play Store and App Store. AFAIK they are pretty much alone among mainstream IM services to offer this. See: https://core.telegram.org/reproducible-builds https://core.telegram.org/reproducible-builds
- dbrgn 6y ago
  Threema offers reproducible builds as well, for the Android app: https://threema.ch/en/open-source/reproducible-builds https://threema.ch/en/open-source/reproducible-builds Signal too: https://github.com/signalapp/Signal-Android/blob/master/reproducible-builds/README.md https://github.com/signalapp/Signal-Android/blob/master/repr... Regarding the iOS app store, Telegram writes: > As things stand now, you'll need a jailbroken device, at least 1,5 hours and approximately 90GB of free space to properly set up a virtual machine for the verification process. https://core.telegram.org/reproducible-builds#reproducible-builds-for-ios https://core.telegram.org/reproducible-builds#reproducible-b... It's a manual process within a new VM. I wouldn't be surprised if it frequently breaks without anyone noticing. But at least they're trying, I'm not aware of any better approach. Apple's GUI-focussed approach doesn't make these things easy.

akvadrako 6y ago

Can you really compile them? If you look at the iOS repo, first there is no license associated with the repo. Second, there are lots of people reporting failed builds in the issue tracker without a response. https://github.com/TelegramMessenger/Telegram-iOS https://github.com/TelegramMessenger/Telegram-iOS https://github.com/TelegramMessenger/Telegram-iOS/issues/377 https://github.com/TelegramMessenger/Telegram-iOS/issues/377