On entend souvent « don’t roll your own crypto ». Mais pourquoi ?
Parce que concevoir et implémenter un protocole cryptographique, c’est très complexe !
Les failles de sécurité peuvent se loger aussi bien dans les primitives cryptographiques (comme le chiffrement ou les signatures) que dans le protocole qui repose sur ces primitives.
Ces failles peuvent se trouver non seulement dans le code, mais aussi dans la spécification du protocole ou de la primitive.

Les méthodes formelles fournissent des outils qui permettent de prouver l’absence de telles failles.
Ces méthodes, si elles sont utilisées principalement par des chercheurs ont des applications bien réelles pour valider et sécuriser les protocoles que vous utilisez quotidiennement.

Nous verrons comment des failles comme Heartbleed [1], le buffer overflow dans SHA-3 [2], ou encore les multiples failles de Matrix [3] auraient pu être évitées grâce aux méthodes formelles, et je partagerai mon expérience avec l’application de ces méthodes sur le futur protocole de messagerie sécurisé MLS [4].

– [1] https://heartbleed.com/
– [2] https://mouha.be/sha-3-buffer-overflow/
– [3] https://nebuchadnezzar-megolm.github.io/
– [4] https://eprint.iacr.org/2022/1732