4 ms·

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

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.

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.