6 ms·

Automated Symbolic Verification of Telegram's MTProto 2.0

64 points by wyuenho 6y ago

dane-pgp 6y ago
Impressive work, but it leaves open the inevitable question of whether the software that is distributed actually implements the protocol as modelled in the proof. With reproducible builds and a trustworthy build environment, we can hopefully assume that the binary matches the source code, but there isn't yet a proof that the source code doesn't have some unmodelled edge cases (as in the 2017 Key Reinstallation AttaCKs[0] on WPA2). About this threat, the paper says: "Concerning implementation flaws, our formalisation can be used as a reference for the correct implementation of MTProto 2.0 clients (and servers). Tools like Spi2Java or FS2PV can be useful to this end." [0] https://www.krackattacks.com/ https://www.krackattacks.com/
- slondr 6y ago
  The clients are all open source, so you can compile the code on your own machine.
  - 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
kitkat_new 6y ago
well, kind of useless in practice, if the servers know the keys (except for unsynced 1:1...)
- ffpip 6y ago
  Broken crypto ("bunch of randoms have rolled their own crypto", to be precise [0]) is pretty much the only argument HN has against Telegram. They use the same 7 year old russian article [1] to show the said broken crpyto, despite that being written like the month telegram launched on HN. They have fixed all these long ago and even rolled out MTProto 2.0. Nobody wants to break this crypto despite criticizing it. There's a 300K$ cash prize [2]. [0] - https://news.ycombinator.com/item?id=6913632 https://news.ycombinator.com/item?id=6913632 [1] - https://m.habr.com/en/post/206900/ https://m.habr.com/en/post/206900/ [2] - https://telegram.org/faq#q-what-if-my-hacker-friend-says-they-could-decipher-telegram-mes https://telegram.org/faq#q-what-if-my-hacker-friend-says-the...
  - approxim8ion 6y ago
    The bounty isn't as much of an assurance as they would have you believe. Good publicity nonetheless. Relevant article from Moxie Marlinespike: https://archive.vn/SIl9M https://archive.vn/SIl9M A theorized valid attack that was deemed invalid by the fine print in their bounty program: https://web.archive.org/web/20181118154823/https://www.alexrad.me/discourse/a-264-attack-on-telegram-and-why-a-super-villain-doesnt-need-it-to-read-your-telegram-chats.html https://web.archive.org/web/20181118154823/https://www.alexr... These are criticisms of MTproto 1, there is barely any literature about the new version.
    - Anon1096 6y ago
      I think this exact comment sequence with these exact links has been played out on every Hacker News thread about Telegram since its inception.
    - ffpip 6y ago
      Yeah I know it's just publicity. Just like 'Apple will pay 1 million dollars for iphone hack' articles. But Moxie (or any other cryptographer) could use the money for Signal's development. It's a large amount.
j16sdiz 6y ago
[quote] In the light of these results, we can affirm that MTProto 2.0 does not present any logical flaw. Vulnerabilities can arise only from the cryptographic primitives, from implementation flaws (e.g. insufficient checks), from side-channels exfiltration (such as timing or traffic analysis), or from incorrect user behaviour. Hence, these are the aspects which deserve further investigation and particular care in the implementation and use of this protocol. The basic encryption primitive of MTProto 2.0 is assumed to be a perfect authenticated encryption scheme (IND-CCA and INT-CTXT). Although no attack on this scheme is known to date, these properties need to be formally proved in order to deem MTProto 2.0 definitely secure. This proof cannot be done in a symbolic model like ProVerif’s, but it can be achieved in a computational model, using tools like CryptoVerif or EasyCrypt [5, 2], which we leave to future work. However, even in the very unlikely case that a flaw is found in the encryption scheme, the results in this paper would be still valid: the protocol could be used just by replacing the encryption scheme, and no other changes would be required. [/quote] This analysis the protocol, not the cryptographic primitives, which was what get criticized
- BelenusMordred 6y ago
  Apart from choosing RSA over elliptical curves, which primitive in particular is the problem? Otherwise under the hood it's AES256-IGE and SHA256? The key exchange is a strange choice for a modern greenfields project but hardly that noteworthy.
  - amluto 6y ago
    As far as I can tell, AES256-IGE is a made up mode used only by Telegram. That’s far from being a standard choice. I don’t know what authenticated encryption scheme they build on it, but on a very brief look, it doesn’t look authenticated at all. See: https://mgp25.com/AESIGE/ https://mgp25.com/AESIGE/
    - deleted 6y ago
      [deleted]
    - BelenusMordred 6y ago
Canada 6y ago
It's not as if anyone even uses it. It's not even supported in the desktop clients.
- wyuenho 6y ago
  Telegram's MAU is 400 mill last checked [0]. On the desktop, you just can't register, so you can't create an auth_key, but that doesn't mean you can't use the Telegram API over a TLS transport, and encrypt messages using the auth_key created on a phone. [0]: https://www.businessofapps.com/data/telegram-statistics/ https://www.businessofapps.com/data/telegram-statistics/
  - jlelse 6y ago
    Telegram has more than 500 million active users already. https://t.me/durov/142 https://t.me/durov/142
  - Canada 6y ago
    I'm not saying Telegram doesn't have a lot of users, I'm saying that pretty much nobody uses the secret chat feature because it's not supported on all clients and even the clients that do support it can only do 1:1. So it's not very useful.
- lloeki 6y ago
  > It's not even supported in the desktop clients. Secret chat is supported on the macOS native client (there are two clients, the cross-desktop one is electron-based, the native one is in Swift and shares code with the iOS client.
  - Canada 6y ago
    Really? This is the MacOS one version 2.5.1 right? I'm looking and I'm not seeing the option for creating a new secret chat. Is this not the native one? Because the other one had a higher version number and I was running it on Linux for a while.
    - 6y ago

64 points by wyuenho 6y ago

Impressive work, but it leaves open the inevitable question of whether the software that is distributed actually implements the protocol as modelled in the proof. With reproducible builds and a trustworthy build environment, we can hopefully assume that the binary matches the source code, but there isn't yet a proof that the source code doesn't have some unmodelled edge cases (as in the 2017 Key Reinstallation AttaCKs[0] on WPA2). About this threat, the paper says: "Concerning implementation flaws, our formalisation can be used as a reference for the correct implementation of MTProto 2.0 clients (and servers). Tools like Spi2Java or FS2PV can be useful to this end." [0] https://www.krackattacks.com/ https://www.krackattacks.com/

slondr 6y ago
The clients are all open source, so you can compile the code on your own machine.
- 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

kitkat_new 6y ago

well, kind of useless in practice, if the servers know the keys (except for unsynced 1:1...)

ffpip 6y ago
Broken crypto ("bunch of randoms have rolled their own crypto", to be precise [0]) is pretty much the only argument HN has against Telegram. They use the same 7 year old russian article [1] to show the said broken crpyto, despite that being written like the month telegram launched on HN. They have fixed all these long ago and even rolled out MTProto 2.0. Nobody wants to break this crypto despite criticizing it. There's a 300K$ cash prize [2]. [0] - https://news.ycombinator.com/item?id=6913632 https://news.ycombinator.com/item?id=6913632 [1] - https://m.habr.com/en/post/206900/ https://m.habr.com/en/post/206900/ [2] - https://telegram.org/faq#q-what-if-my-hacker-friend-says-they-could-decipher-telegram-mes https://telegram.org/faq#q-what-if-my-hacker-friend-says-the...
- approxim8ion 6y ago
  The bounty isn't as much of an assurance as they would have you believe. Good publicity nonetheless. Relevant article from Moxie Marlinespike: https://archive.vn/SIl9M https://archive.vn/SIl9M A theorized valid attack that was deemed invalid by the fine print in their bounty program: https://web.archive.org/web/20181118154823/https://www.alexrad.me/discourse/a-264-attack-on-telegram-and-why-a-super-villain-doesnt-need-it-to-read-your-telegram-chats.html https://web.archive.org/web/20181118154823/https://www.alexr... These are criticisms of MTproto 1, there is barely any literature about the new version.
  - Anon1096 6y ago
    I think this exact comment sequence with these exact links has been played out on every Hacker News thread about Telegram since its inception.
  - ffpip 6y ago
    Yeah I know it's just publicity. Just like 'Apple will pay 1 million dollars for iphone hack' articles. But Moxie (or any other cryptographer) could use the money for Signal's development. It's a large amount.

j16sdiz 6y ago

[quote] In the light of these results, we can affirm that MTProto 2.0 does not present any logical flaw. Vulnerabilities can arise only from the cryptographic primitives, from implementation flaws (e.g. insufficient checks), from side-channels exfiltration (such as timing or traffic analysis), or from incorrect user behaviour. Hence, these are the aspects which deserve further investigation and particular care in the implementation and use of this protocol. The basic encryption primitive of MTProto 2.0 is assumed to be a perfect authenticated encryption scheme (IND-CCA and INT-CTXT). Although no attack on this scheme is known to date, these properties need to be formally proved in order to deem MTProto 2.0 definitely secure. This proof cannot be done in a symbolic model like ProVerif’s, but it can be achieved in a computational model, using tools like CryptoVerif or EasyCrypt [5, 2], which we leave to future work. However, even in the very unlikely case that a flaw is found in the encryption scheme, the results in this paper would be still valid: the protocol could be used just by replacing the encryption scheme, and no other changes would be required. [/quote] This analysis the protocol, not the cryptographic primitives, which was what get criticized

BelenusMordred 6y ago
Apart from choosing RSA over elliptical curves, which primitive in particular is the problem? Otherwise under the hood it's AES256-IGE and SHA256? The key exchange is a strange choice for a modern greenfields project but hardly that noteworthy.
- amluto 6y ago
  As far as I can tell, AES256-IGE is a made up mode used only by Telegram. That’s far from being a standard choice. I don’t know what authenticated encryption scheme they build on it, but on a very brief look, it doesn’t look authenticated at all. See: https://mgp25.com/AESIGE/ https://mgp25.com/AESIGE/
  - deleted 6y ago
    [deleted]
  - BelenusMordred 6y ago

Canada 6y ago

It's not as if anyone even uses it. It's not even supported in the desktop clients.

wyuenho 6y ago
Telegram's MAU is 400 mill last checked [0]. On the desktop, you just can't register, so you can't create an auth_key, but that doesn't mean you can't use the Telegram API over a TLS transport, and encrypt messages using the auth_key created on a phone. [0]: https://www.businessofapps.com/data/telegram-statistics/ https://www.businessofapps.com/data/telegram-statistics/
- jlelse 6y ago
  Telegram has more than 500 million active users already. https://t.me/durov/142 https://t.me/durov/142
- Canada 6y ago
  I'm not saying Telegram doesn't have a lot of users, I'm saying that pretty much nobody uses the secret chat feature because it's not supported on all clients and even the clients that do support it can only do 1:1. So it's not very useful.
lloeki 6y ago
> It's not even supported in the desktop clients. Secret chat is supported on the macOS native client (there are two clients, the cross-desktop one is electron-based, the native one is in Swift and shares code with the iOS client.
- Canada 6y ago
  Really? This is the MacOS one version 2.5.1 right? I'm looking and I'm not seeing the option for creating a new secret chat. Is this not the native one? Because the other one had a higher version number and I was running it on Linux for a while.
  - 6y ago